根多胞体投影定理的无分类证明

Let Φ be a finite reduced crystallographic root system, let P_Φ = conv(Φ) be its root polytope, and let U be a nonzero subspace spanned by roots. Hopkins and Postnikov proved that the orthogonal projection of P_Φ onto U lies in κP_(Φ∩U) for some κ < 2. The published proofs conclude with a case check from the classification of finite root systems. Writing γ_P for the Minkowski functional of P, which measures the least dilation needed to contain a vector, we give a direct proof and the rootwise estimate γ_(P_(Φ∩U))(proj_U α) ≤ 2‖proj_U α‖²/‖α‖² < 2 for α ∈ Φ outside U. After a Weyl-group symmetry moves the projected root into an antidominant chamber, its negative is a nonnegative combination of the vectors dual to the simple roots. After division by half the squared length of the original root, the coefficients are integers. A parabolic orbit average gives a linear upper bound for the gauge, while inverse positivity for an obtuse Gram matrix gives a quadratic lower bound for the norm. Integrality joins the two estimates, and strict contraction under orthogonal projection gives the factor below two. Taking the maximum over the finite root system proves the polytope containment and answers the request for a uniform proof. A complete Lean 4 formalization is publicly available.