Original mean-centered moment inequalities form a compact convex body with explicit coordinate bounds
ProvedHirsch.moment_curve_compact_bodyFor any positive half-dimension k, more than 2k distinct real moment parameters on m original labels define their mean-centered dimension-2k inequality set P by all original rows <=1. Prove P compact and convex, with zero in its ordinary ambient interior. For each original row construct a feasible point making it equal to one and every other row strictly less than one. Derive an explicit coordinate box from m times the sums of absolute coefficients of the Lagrange nodal basis. No boundedness, full-rank inverse, vertex catalogue, compactness, feasible support point, or polytope realization is supplied as a premise. The result supplies original-space compact/full-dimensional realization facts; it does not formalize simplicity, a complete facet-lattice identification, asymptotics, or a uniform diameter bound.
import Mathlib open scoped BigOperators
namespace Hirsch
theorem moment_curve_compact_body (k m : ℕ) (hk : 0 < k) (hm : 2 * k < m)
(a : Fin m → ℝ) (ha : Function.Injective a) :
let row : (Fin (2 * k) → ℝ) → Fin m → ℝ := fun x i =>
∑ j : Fin (2 * k),
(a i ^ (j.val + 1) - (∑ l, a l ^ (j.val + 1)) / (m : ℝ)) * x j
let P : Set (Fin (2 * k) → ℝ) := {x | ∀ i : Fin m, row x i ≤ 1}
IsCompact P ∧ Convex ℝ P ∧ (0 : Fin (2 * k) → ℝ) ∈ interior P ∧
(∀ i : Fin m, ∃ x : Fin (2 * k) → ℝ,
x ∈ P ∧ row x i = 1 ∧ ∀ l : Fin m, l ≠ i → row x l < 1) ∧
∀ x ∈ P, ∀ j : Fin (2 * k),
|x j| ≤ (m : ℝ) * ∑ i : Fin m,
|(Lagrange.basis Finset.univ a i).coeff (j.val + 1)| := by sorry
end Hirsch