Target-monotone original-edge routes between all moment-polytope vertices
ProvedHirsch.moment_all_endpoint_monotone_routesFor every d<m and injective real node parameters a, form the original mean-centered moment inequalities row_i(x)<=1 in R^d. For ANY two actual extreme points u,v, define the score as the sum of v's tight original rows. Construct a finite natural-indexed route from u to v of length L<choose(m,d), consisting entirely of actual original extreme points. Every step strictly increases that fixed target score, and its entire closed segment is an exposed original edge; strict increase makes the edge nondegenerate. Every original target row already tight at a route point stays tight after the next step. No vertex catalogue, normalized directions, improving-pivot oracle, path or termination bound is supplied. The proof derives target displacement as a nonnegative combination of actual release directions, obtains a target-improving direction that cannot lose a shared target row, and assembles the full route by strict finite ascent using the accepted exact all-vertex catalogue. All dimensions including zero, odd dimensions, arbitrary real spacings, unsorted labels, negative-mean vertices and identical endpoints are retained. The bound can be exponential. This is not a polynomial diameter bound, a shortest or fully nonrevisiting path theorem, or a solution of unrestricted Polynomial Hirsch.
import Mathlib open scoped BigOperators set_option autoImplicit false
theorem Hirsch.moment_all_endpoint_monotone_routes (d m : ℕ) (hm : d < m) (a : Fin m → ℝ)
(ha : Function.Injective a) (u v : Fin d → ℝ) :
let row : (Fin d → ℝ) → Fin m → ℝ := fun x i =>
∑ j : Fin d, (a i ^ (j.val+1) - (∑ z, a z ^ (j.val+1)) / (m : ℝ)) * x j
let P : Set (Fin d → ℝ) := {x | ∀ i, row x i ≤ 1}
let J : Finset (Fin m) := Finset.univ.filter (fun i => row v i = 1)
let score : (Fin d → ℝ) → ℝ := fun x => ∑ i ∈ J, row x i
u ∈ P.extremePoints ℝ → v ∈ P.extremePoints ℝ →
∃ L : ℕ, L < Nat.choose m d ∧ ∃ p : ℕ → (Fin d → ℝ),
p 0 = u ∧ p L = v ∧
(∀ i, i ≤ L → p i ∈ P.extremePoints ℝ) ∧
∀ i, i < L → score (p i) < score (p (i+1)) ∧
IsExposed ℝ P (segment ℝ (p i) (p (i+1))) ∧
∀ j, row (p i) j = 1 → row v j = 1 → row (p (i+1)) j = 1 := by sorry