Alternating moment labels form explicit minimal incompatible original-row families
ProvedHirsch.moment_curve_ordered_minimal_nonfacesFor any injective real moment-parameter map a on m original labels, a half-dimension k and a map b selecting 2k+3 parameters in strictly increasing order, let N consist of the k+1 odd-ranked selected labels. In the original 2k-dimensional mean-centered moment inequality system (averaged over all m labels), prove that N has cardinality k+1, no feasible point makes all N rows tight, and every proper subset T of N has a feasible witness making exactly the rows in T tight. The barycentric signs, incompatibility, and proper-face feasibility are derived, not assumed. This assembles the ordered-sign and minimality bridge using the accepted small-face and barycentric proof bodies; it does not count the complete odd-label catalogue, assert a general diameter bound, or solve Polynomial Hirsch.
import Mathlib open scoped BigOperators
namespace Hirsch
theorem moment_curve_ordered_minimal_nonfaces (k m : ℕ) (a : Fin m → ℝ) (ha : Function.Injective a)
(b : Fin (2 * k + 3) → Fin m) (hab : StrictMono (fun j => a (b j))) :
let N : Finset (Fin m) := Finset.univ.image
(fun j : Fin (k + 1) => b ⟨2 * j.val + 1, by have hj := j.isLt; omega⟩)
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
N.card = k + 1 ∧
(¬ ∃ x : Fin (2 * k) → ℝ,
(∀ i : Fin m, row x i ≤ 1) ∧ ∀ i ∈ N, row x i = 1) ∧
∀ T : Finset (Fin m), T ⊂ N →
∃ x : Fin (2 * k) → ℝ,
(∀ i : Fin m, row x i ≤ 1) ∧
∀ i : Fin m, row x i = 1 ↔ i ∈ T := by sorry
end Hirsch