One finite cut-image recipe catalogue covers every cut-vertex coordinate
ProvedHirsch.cut_vertex_uniform_coordinate_catalogueLet S be any generating set in real d-dimensional coordinate space, C a finite family of m linear cuts with right-hand side b, Omega a finite set containing the whole m-component cut image of every point of S, and Lambda a finite set containing every coordinate of every point of S. There exists ONE finite scalar set K containing every coordinate of EVERY extreme point of convexHull(S) intersected with those halfspaces. Its cardinality is at most sum from n=0 to min(d+1,m+1) of 2^m times |Omega|^n times |Lambda|^n. Neither cut vertices, positive supports, their weights, an active-row choice, a catalogue, nor catalogue membership are supplied. The proof constructs all finite active-mask, cut-image-tuple and scalar-tuple recipes and decodes one scalar per recipe, using the accepted support-selection/unique-weight theorem to show every actual coordinate is decoded. Inconsistent recipes may output zero; underdetermined recipes may select arbitrary solutions, so K is an overcover, not an exact attained-value list. The empty-support term is harmless padding in the count. The coefficient recipe uses classical choice, not a certified executable solver. The bound is not polynomial in unrestricted cut count and does not establish Polynomial Hirsch.
import Mathlib open scoped BigOperators set_option autoImplicit false
theorem Hirsch.cut_vertex_uniform_coordinate_catalogue
(m d : ℕ) (S : Set (Fin d → ℝ))
(C : Fin m → (Fin d → ℝ) →ₗ[ℝ] ℝ) (b : Fin m → ℝ)
(Ω : Finset (Fin m → ℝ)) (Λ : Finset ℝ)
(hΩ : ∀ v ∈ S, (fun j => C j v) ∈ Ω)
(hΛ : ∀ v ∈ S, ∀ k, v k ∈ Λ) :
∃ K : Finset ℝ,
K.card ≤ ∑ n : Fin (min (d + 1) (m + 1) + 1),
2 ^ m * Ω.card ^ n.val * Λ.card ^ n.val ∧
∀ x : Fin d → ℝ,
x ∈ (convexHull ℝ S ∩ {y | ∀ j, C j y ≤ b j}).extremePoints ℝ →
∀ k, x k ∈ K := by sorry