Construct an explicit quadratic-generator zonotopal completion of every finite convex hull
ProvedHirsch.finite_hull_pair_segment_completionFor arbitrary natural d, positive n and arbitrary real vectors v_0,...,v_(n-1) in R^d, define Z as the actual sum over all n^2 ordered pairs of closed segments [v_i,v_j], with explicit coefficients in [0,1]. Define Q={q: q+v_i belongs to Z for every original generator i}. Prove Z and Q are compact and convex, Q is nonempty, and Z=conv(v_i)+Q as whole sets. In particular the specified finite convex hull is an actual Minkowski summand of this explicit segment-sum completion. No summand, support equality, rank, independence, full dimension, distinct generators, or generic objective is assumed. The construction includes repeated/interior generators, lower dimensions, d=0 and n=1. The n^2 count is the number of presented segment positions, including diagonal and repeated positions, not the number of irredundant facets or a minimal generator count. No original-edge route or polynomial-in-H-row bound is concluded.
import Mathlib open scoped BigOperators Pointwise set_option autoImplicit false
theorem Hirsch.finite_hull_pair_segment_completion (d n : ℕ) (hn : 0 < n) (v : Fin n → (Fin d → ℝ)) :
let Z : Set (Fin d → ℝ) :=
{z | ∃ t : (Fin n × Fin n) → ℝ,
(∀ e, 0 ≤ t e ∧ t e ≤ 1) ∧
(∑ e : Fin n × Fin n, (t e • v e.1+(1-t e) • v e.2))=z}
let Q : Set (Fin d → ℝ) := {q | ∀ i, q+v i ∈ Z}
IsCompact Z ∧ Convex ℝ Z ∧ IsCompact Q ∧ Convex ℝ Q ∧ Q.Nonempty ∧
Z = {z | ∃ p ∈ convexHull ℝ (Set.range v), ∃ q ∈ Q, p+q=z} ∧
Fintype.card (Fin n × Fin n) = n^2 := by sorry