A Classification-Free Proof of the Root-Polytope Projection Theorem

Let Phi be a finite reduced crystallographic root system, let its root polytope be the convex hull of Phi, and let U be a nonzero subspace spanned by roots. Hopkins and Postnikov proved that the orthogonal projection of the root polytope onto U lies in kappa times the root polytope of Phi intersect U for some kappa below two; the published proofs conclude with a classification check. This paper gives a direct proof and an explicit rootwise estimate. A subsystem Weyl symmetry moves each projected root into an antidominant chamber. Parabolic orbit averaging gives a linear gauge bound, inverse positivity for an obtuse Gram matrix gives a quadratic norm bound, and crystallographic integrality joins them. Strict contraction under orthogonal projection yields the factor below two. Taking the maximum over the finite root system proves the full polytope containment. A complete Lean 4 formalization is provided.