Regression check for Theorem 1.12

This file isolates the geometric facts needed to pass from the centerpoint theorem for convex flags to the polytope statement. Following the proof in the paper, the flag is built over the working polytope Q = convexHull ℝ (Function.support w), then its output is transported to the minimal containing face of the original polytope P.

The file does not postulate that this support-hull face flag exists. Instead it verifies, without any local sorry, that the explicit construction obligations below suffice. In particular, the Helly bound is derived from the three-case check in FaceFlagHellyBound, rather than stored as a field.

theorem EGZ.mem_affineIntSpan_of_mem {d : ℕ} {S : Set (RealCoord d)} {q : RealCoord d} (hq : q ∈ S) : q ∈ affineIntSpan S

Every member of a set belongs to its affine integer span.

structure EGZ.SupportHullFaceFlagAdapter {d : ℕ} (P : RationalPolytope d) (w : RealCoord d → NNReal) : Type 1

The exact obligations supplied by the canonical face flag of the support hull and by the reduction back to the original polytope.

It is essential that model presents working, not all of P: an unsupported zero-dimensional face of P has no affine lattice generated by the support. The fields outputFace and integral_output_span encode the paper's final passage from a face of working to the minimal containing face of P.

• working : RationalPolytope d

  Rational polytope given by the convex hull of the weighted support.

• working_carrier_eq : self.working.carrier = (convexHull ℝ) (Function.support w)
• working_subset_original : self.working.carrier ⊆ P.carrier
• model : FaceFlagModel self.working

  Face-flag model of the working support polytope.

• laws : FaceFlagCombinationLaws self.model
• supportLift_integral (x : RealCoord d) (_hx : x ∈ Function.support w) (hxQ : x ∈ self.working.carrier) : (self.model.lift x hxQ).IsIntegral
• integralPhysical_rational (q : self.model.flag.Point) (hq : q ∈ self.model.proper) : q.IsIntegral → IsRational (self.model.physical q hq)
• outputFace : { q : self.model.flag.Point // q ∈ self.model.proper } → P.Face

  Face of the original polytope assigned to each proper flag point.

• physical_mem_output_relInterior (q : { q : self.model.flag.Point // q ∈ self.model.proper }) : self.model.physical ↑q ⋯ ∈ (self.outputFace q).relInterior
• integral_output_span (q : { q : self.model.flag.Point // q ∈ self.model.proper }) : (↑q).IsIntegral → self.model.physical ↑q ⋯ ∈ affineIntSpan (Function.support w ∩ (self.outputFace q).carrier)
• topFunctional : (RealCoord d →ᵃ[ℝ] ℝ) → self.model.flag.LinearFunction

  Lift a physical affine functional to a linear function at the top flag node.

• topFunctional_base (xi : RealCoord d →ᵃ[ℝ] ℝ) : (self.topFunctional xi).base = ⊤
• topFunctional_eval (xi : RealCoord d →ᵃ[ℝ] ℝ) (q : { q : self.model.flag.Point // q ∈ self.model.proper }) (hq : (self.topFunctional xi).EvaluableAt ↑q) : (self.topFunctional xi).eval (↑q) hq = xi (self.model.physical ↑q ⋯)

theorem EGZ.SupportHullFaceFlagAdapter.support_mem_working {d : ℕ} {P : RationalPolytope d} {w : RealCoord d → NNReal} (A : SupportHullFaceFlagAdapter P w) : Function.support w ⊆ A.working.carrier

Every support point lies in the working support hull.

theorem EGZ.SupportHullFaceFlagAdapter.support_subset_original {d : ℕ} {P : RationalPolytope d} {w : RealCoord d → NNReal} (A : SupportHullFaceFlagAdapter P w) : Function.support w ⊆ P.carrier

The support-hull reduction retains the original theorem's hypothesis that all weighted points lie in P.

theorem EGZ.SupportHullFaceFlagAdapter.topFunctional_evaluable {d : ℕ} {P : RationalPolytope d} {w : RealCoord d → NNReal} (A : SupportHullFaceFlagAdapter P w) (xi : RealCoord d →ᵃ[ℝ] ℝ) (q : A.model.flag.Point) : (A.topFunctional xi).EvaluableAt q

A top-based flag functional is evaluable at every flag point.

noncomputable def EGZ.canonicalSupportHullFaceFlagAdapter {d : ℕ} (P : RationalPolytope d) (w : RealCoord d → NNReal) (hfinite : (Function.support w).Finite) (hnonzero : w ≠ 0) (hsupport : Function.support w ⊆ P.carrier) (hrational : ∀ q ∈ Function.support w, IsRational q) : SupportHullFaceFlagAdapter P w

The canonical support-hull face flag required in Theorem 1.12.

Its nodes are the faces of convexHull ℝ (Function.support w). A point is based at its least containing face, whose lattice is the affine integer span of the support points on that face. The output face is the least face of the original polytope containing the physical point.

Equations

• One or more equations did not get rendered due to their size.

theorem EGZ.polytopeCenterpointConclusion_of_supportHullFaceFlagAdapter {d : ℕ} (P : RationalPolytope d) (w : RealCoord d → NNReal) (hfinite : (Function.support w).Finite) (hnonzero : w ≠ 0) (G : HollowPolytopeGeometry d) (A : SupportHullFaceFlagAdapter P w) : PolytopeCenterpointConclusion P w

Regression theorem for the proof of Theorem 1.12. Once the support-hull face flag and the independent convex-geometric bundle have been constructed, Corollary 3.14 implies the desired conclusion for the original polytope.

The Helly bound used below is proved by FaceFlagCombinationLaws.hellyConstant_le_hollowPolytopeNumber; it is not an assumption of the adapter.

theorem EGZ.polytopeCenterpointConclusion_of_hollowGeometry {d : ℕ} (P : RationalPolytope d) (w : RealCoord d → NNReal) (hfinite : (Function.support w).Finite) (hnonzero : w ≠ 0) (hsupport : Function.support w ⊆ P.carrier) (hrational : ∀ q ∈ Function.support w, IsRational q) (G : HollowPolytopeGeometry d) : PolytopeCenterpointConclusion P w

The face-flag and centerpoint parts of Theorem 1.12 are unconditional; only boundedness of hollow-polytope vertex counts remains as an input here.

structure EGZ.TheoremOneTwelveSetup (d : ℕ) : Type 1

The two construction theorems still needed to discharge Theorem 1.12 itself. This packages no conclusion about centerpoints: it contains only the global hollow-polytope geometry and the construction of the canonical support-hull face flag from the hypotheses of the theorem.

• hollowGeometry : HollowPolytopeGeometry d
• supportHullFaceFlag (P : RationalPolytope d) (w : RealCoord d → NNReal) : (Function.support w).Finite → w ≠ 0 → Function.support w ⊆ P.carrier → (∀ q ∈ Function.support w, IsRational q) → SupportHullFaceFlagAdapter P w

  Construct a support-hull face-flag adapter for each admissible weighted polytope.

noncomputable def EGZ.TheoremOneTwelveSetup.ofHollowGeometry {d : ℕ} (G : HollowPolytopeGeometry d) : TheoremOneTwelveSetup d

The canonical face model discharges the construction field of TheoremOneTwelveSetup; the setup is therefore equivalent in practice to the independent hollow-polytope boundedness theorem.

Equations

• One or more equations did not get rendered due to their size.

theorem EGZ.polytopeCenterpointConclusion_of_theoremOneTwelveSetup {d : ℕ} (D : TheoremOneTwelveSetup d) (P : RationalPolytope d) (w : RealCoord d → NNReal) (hfinite : (Function.support w).Finite) (hnonzero : w ≠ 0) (hsupport : Function.support w ⊆ P.carrier) (hrational : ∀ q ∈ Function.support w, IsRational q) : PolytopeCenterpointConclusion P w

Exact assembly check against the corrected statement of Theorem 1.12. Once TheoremOneTwelveSetup d is constructed, no further geometric assumptions are needed.