Quadratic original-edge routes with at most three exceptional target rows
ProvedHirsch.three_exception_quadratic_original_routesFor a finite real family C in ambient dimension d whose convex hull equals the original m halfspaces, actual extreme endpoints u,v, and at most three exceptional original row labels B, assume every target-tight row outside B has its boundary value and at most one other value on all actual vertices. Construct a route through actual original extreme points of length at most (m-d)+m*m. Every consecutive pair is distinct, its entire segment is IsExtreme in the original halfspace body, and every acquired target row stays tight. Residual dimension, nonzero-restriction slice bounds, incidence counts and the actual route are derived; no graph, basis, residual rank, small catalogue or cheap route is supplied. Exact H/hull equality and the outside-B two-level condition are explicit structural assumptions. Redundant rows/generators, nonsimple/lower-dimensional hulls, dimension zero, coincident endpoints, empty B and non-target exceptions are included. This is not a uniform Polynomial Hirsch theorem, shortestness, all-facet nonrevisiting or an efficient H-to-V claim.
import Mathlib open scoped BigOperators set_option autoImplicit false
theorem Hirsch.three_exception_quadratic_original_routes (d m : ℕ) (C : Finset (Fin d → ℝ))
(A : Fin m → (Fin d → ℝ) →ₗ[ℝ] ℝ) (b : Fin m → ℝ)
(hP : convexHull ℝ (C : Set (Fin d → ℝ))={x | ∀ i, A i x ≤ b i})
(B : Finset (Fin m)) (hB : B.card ≤ 3) (u v : Fin d → ℝ)
(hu : u ∈ ({x | ∀ i, A i x ≤ b i} : Set (Fin d → ℝ)).extremePoints ℝ)
(hv : v ∈ ({x | ∀ i, A i x ≤ b i} : Set (Fin d → ℝ)).extremePoints ℝ)
(htwo : ∀ i, i ∉ B → A i v=b i → ∃ lo : ℝ,
∀ x ∈ ({x | ∀ j, A j x ≤ b j} : Set (Fin d → ℝ)).extremePoints ℝ,
A i x=lo ∨ A i x=b i) :
∃ L : ℕ, L ≤ (m-d)+m*m ∧
∃ p : Fin (L+1) → (Fin d → ℝ), p 0=u ∧ p (Fin.last L)=v ∧
(∀ t, p t ∈ ({x | ∀ i, A i x ≤ b i} : Set (Fin d → ℝ)).extremePoints ℝ) ∧
∀ t : Fin L, p t.castSucc ≠ p t.succ ∧
IsExtreme ℝ {x : Fin d → ℝ | ∀ i, A i x ≤ b i}
(segment ℝ (p t.castSucc) (p t.succ)) ∧
(∀ i, A i v=b i → A i (p t.castSucc)=b i → A i (p t.succ)=b i) := by sorry