Construct a mass-preserving square active-row system at every cut vertex
ProvedHirsch.cut_vertex_selected_active_square_systemFor any actual extreme point x of convexHull(S) intersected with m original linear halfspaces in real dimension d, construct a finite positive independent support v_i in S, with n<=d+1 and positive barycentric weights w_i representing x. Select a finite set J of original cuts active at x with exactly n-1 members. The total-mass equation and these selected active-value equations form a square bijective linear system: for EVERY real prescribed mass and EVERY real vector of selected values there exists exactly one real weight vector realizing them. In particular mass one and the original selected right sides uniquely recover w, even among signed alternatives. Neither the support, its weights, selected rows, an inverse, a determinant or a rank oracle is assumed. S need not be finite, closed or compact; support points may individually violate the cuts. The singleton-support case selects no active rows. Existence and exact recovery are proved, not a particular executable row-selection algorithm or a polynomial global catalogue size. This is a finite geometric-algebraic interface, not Polynomial Hirsch.
import Mathlib open scoped BigOperators set_option autoImplicit false
theorem Hirsch.cut_vertex_selected_active_square_system
(m d : ℕ) (S : Set (Fin d → ℝ))
(C : Fin m → (Fin d → ℝ) →ₗ[ℝ] ℝ) (b : Fin m → ℝ)
(x : Fin d → ℝ)
(hx : x ∈ (convexHull ℝ S ∩ {y | ∀ j, C j y ≤ b j}).extremePoints ℝ) :
∃ (n : ℕ) (v : Fin n → Fin d → ℝ) (w : Fin n → ℝ)
(J : Finset {j : Fin m // C j x = b j}),
(∀ i, v i ∈ S) ∧ (∀ i, 0 < w i) ∧ (∑ i, w i) = 1 ∧
(∑ i, w i • v i) = x ∧
LinearIndependent ℝ (fun i => ((1 : ℝ), v i)) ∧
n ≤ d + 1 ∧ J.card + 1 = n ∧
(∀ (mass : ℝ) (values : J → ℝ), ∃! u : Fin n → ℝ,
(∑ i, u i) = mass ∧
∀ j : J, (∑ i, u i * C j.val.val (v i)) = values j) ∧
(∀ u : Fin n → ℝ, (∑ i, u i) = 1 →
(∀ j : J, (∑ i, u i * C j.val.val (v i)) = b j.val.val) → u = w) := by sorry