Original-edge routes between arbitrary zonotope vertices without supplied objectives
ProvedHirsch.zonotope_all_endpoint_original_routesFor all natural d and m and any family of m real generators in R^d, any two actual extreme points u and v of the ORIGINAL coefficient segment sum can be joined by a walk of at most m nondegenerate original exposed edges. Every visited point is extreme in the same original body; every consecutive whole closed segment is IsExposed and IsExtreme there. No exposing objectives, regularity, vertex catalogue, Boolean injectivity, face/edge oracle or short route is supplied. The proof derives regular exposing objectives for arbitrary requested extreme points, then reuses the accepted ordered sweep route. Zero, parallel, opposite, repeated and rank-deficient generators, d=0, m=0 and equal endpoints are included. The count m is presented generators, not original H facets. The statement does not provide a polynomial original-facet generator budget, a shortest path, an extracted algorithm or a solution of unrestricted Polynomial Hirsch.
import Mathlib open scoped BigOperators set_option autoImplicit false
theorem Hirsch.zonotope_all_endpoint_original_routes (d m : ℕ) (w : Fin m → (Fin d → ℝ))
(u v : Fin d → ℝ) :
let Z : Set (Fin d → ℝ) := {x | ∃ s : Fin m → ℝ,
(∀ i, 0 ≤ s i ∧ s i ≤ 1) ∧ (∑ i : Fin m, s i • w i) = x}
u ∈ Z.extremePoints ℝ → v ∈ Z.extremePoints ℝ →
∃ L : ℕ, L ≤ m ∧ ∃ p : Fin (L+1) → (Fin d → ℝ),
p 0 = u ∧ p (Fin.last L) = v ∧ (∀ i, p i ∈ Z.extremePoints ℝ) ∧
∀ i : Fin L, p i.castSucc ≠ p i.succ ∧
IsExposed ℝ Z (segment ℝ (p i.castSucc) (p i.succ)) ∧
IsExtreme ℝ Z (segment ℝ (p i.castSucc) (p i.succ)) := by sorry