The face-flag Helly bound used in Theorem 1.12

This file is an intentionally stronger regression check than merely storing the inequality hellyConstant Ω ≤ hollowPolytopeNumber d in a face-flag adapter. It separates the proof in the paper into three cases (a repeated physical point, failure of convex position, and the hollow-polytope case), and proves that the resulting physical certificate contradicts Helly independence.

The two face/lattice facts used by the reduction are stated independently of Helly constants:

• physical affine combinations lift to flag convex combinations; and
• an affine-integer-span certificate on the positive support makes the lift integral.

The canonical face model in EGZ.ConvexFlag.FaceModel now proves both facts. This file also proves that a nonvertex intrinsic integer point of a finite convex hull admits the required nontrivial positive-support representation.

The polytope in this file is the working polytope convexHull ℝ (Function.support w) from the first paragraph of the proof of Theorem 1.12, not necessarily the polytope in the theorem statement. This distinction is essential: an unsupported zero-dimensional face has no affine lattice generated by the support.

structure EGZ.PhysicalNontrivialCombination {d n : ℕ} (P : RationalPolytope d) (points : Fin n → RealCoord d) : Type

A physical convex combination with no coefficient equal to one.

• result : RealCoord d

  Point represented by the convex combination.

• result_mem : self.result ∈ P.carrier
• weight : Fin n → ℝ

  Nonnegative coefficients of the convex combination.

• nonnegative (i : Fin n) : 0 ≤ self.weight i
• sum_eq_one : ∑ i : Fin n, self.weight i = 1
• barycenter : self.result = ∑ i : Fin n, self.weight i • points i
• nontrivial (i : Fin n) : self.weight i ≠ 1

def EGZ.PhysicalNontrivialCombination.activeSet {d n : ℕ} {P : RationalPolytope d} {points : Fin n → RealCoord d} (c : PhysicalNontrivialCombination P points) : Set (RealCoord d)

The physical points occurring with strictly positive coefficient.

Equations

• c.activeSet = points '' {i : Fin n | 0 < c.weight i}

def EGZ.PhysicalNontrivialCombination.IsActiveSpanIntegral {d n : ℕ} {P : RationalPolytope d} {points : Fin n → RealCoord d} (c : PhysicalNontrivialCombination P points) : Prop

The certificate produced in the hollow-polytope case: the result is in the affine integer span of the points used with positive coefficient.

Equations

• c.IsActiveSpanIntegral = (c.result ∈ EGZ.affineIntSpan c.activeSet)

theorem EGZ.FiniteHullModel.nonvertex_intrinsic_combination {d n : ℕ} {points : Fin n → RealCoord d} (H : FiniteHullModel points) (q : RealCoord d) (hqmem : q ∈ H.polytope.carrier) (hqintrinsic : H.polytope.IsIntrinsicInteger q) (hqnotvertex : q ∉ H.polytope.vertexSet) : ∃ (c : PhysicalNontrivialCombination H.polytope points), c.result = q ∧ c.IsActiveSpanIntegral

A nonvertex intrinsic integer point of a finite convex hull has a nontrivial convex representation whose positive support certifies its affine integer span.

The construction first averages all indexed vertices on the minimal face. If that centroid is not the given point, relative-interior extension writes the point strictly between the centroid and another point of the face. A convex representation of the latter point then completes the desired representation while retaining every face vertex with positive weight.

structure EGZ.HollowPolytopeGeometry (d : ℕ) : Prop

Pure convex/lattice geometry needed for the hollow-polytope case.

The finite rational hull, its vertex identification, and the positive-support nonvertex representation are now unconditional. The remaining field is the boundedness property required by the sSup definition of L(d).

• hollowCounts_bddAbove : BddAbove {n : ℕ | AdmitsHollowPolytopeVertexCount d n}

theorem EGZ.HollowPolytopeGeometry.hollowCard_le {d : ℕ} (G : HollowPolytopeGeometry d) (Q : RationalPolytope d) (hQ : Q.IsHollow) : Q.vertexSet.ncard ≤ hollowPolytopeNumber d

Boundedness makes the sSup definition of L(d) an actual upper bound. Without this hypothesis, sSup of an unbounded set of naturals is zero, so this step cannot be recovered from the bare definition.

theorem EGZ.HollowPolytopeGeometry.hollowCase {d n : ℕ} (G : HollowPolytopeGeometry d) (points : Fin n → RealCoord d) (hinjective : Function.Injective points) (hrational : ∀ (i : Fin n), IsRational (points i)) (hconvex : IsInConvexPosition points) (hlarge : hollowPolytopeNumber d < n) : ∃ (H : FiniteHullModel points) (c : PhysicalNontrivialCombination H.polytope points), c.IsActiveSpanIntegral

The paper's hollow-polytope branch, derived from the explicit geometric obligations above.

theorem EGZ.FaceFlagCombinationLaws.of_not_convexPosition {d n : ℕ} {P : RationalPolytope d} {A : FaceFlagModel P} (laws : FaceFlagCombinationLaws A) (points : Fin n → A.flag.Point) (hproper : ∀ (i : Fin n), points i ∈ A.proper) (hintegral : ∀ (i : Fin n), (points i).IsIntegral) (hnotconvex : ¬IsInConvexPosition fun (i : Fin n) => A.physical (points i) ⋯) : ∃ (weight : Fin n → ℝ) (result : A.flag.Point), ConvexFlag.ConvexCombination points weight result ∧ result.IsIntegral ∧ ∀ (i : Fin n), weight i ≠ 1

Failure of convex position already supplies the nontrivial integral combination from the second case in the paper.

theorem EGZ.FaceFlagCombinationLaws.of_physical_duplicate {d n : ℕ} {P : RationalPolytope d} {A : FaceFlagModel P} (laws : FaceFlagCombinationLaws A) (points : Fin n → A.flag.Point) (hproper : ∀ (i : Fin n), points i ∈ A.proper) (hintegral : ∀ (i : Fin n), (points i).IsIntegral) {i j : Fin n} (hij : i ≠ j) (hphysical : A.physical (points i) ⋯ = A.physical (points j) ⋯) : ∃ (weight : Fin n → ℝ) (result : A.flag.Point), ConvexFlag.ConvexCombination points weight result ∧ result.IsIntegral ∧ ∀ (k : Fin n), weight k ≠ 1

A repeated physical point supplies the half-half combination from the first case in the paper.

theorem EGZ.FaceFlagCombinationLaws.of_hollowCase {d n : ℕ} {P : RationalPolytope d} {A : FaceFlagModel P} (laws : FaceFlagCombinationLaws A) (points : Fin n → A.flag.Point) (hproper : ∀ (i : Fin n), points i ∈ A.proper) (hintegral : ∀ (i : Fin n), (points i).IsIntegral) (c : PhysicalNontrivialCombination P fun (i : Fin n) => A.physical (points i) ⋯) (hcspan : c.IsActiveSpanIntegral) : ∃ (weight : Fin n → ℝ) (result : A.flag.Point), ConvexFlag.ConvexCombination points weight result ∧ result.IsIntegral ∧ ∀ (i : Fin n), weight i ≠ 1

The hollow-polytope case lifts the intrinsic integer certificate through the face-lattice compatibility law.

theorem EGZ.FaceFlagCombinationLaws.exists_nontrivial_integral_combination_of_large {d n : ℕ} {P : RationalPolytope d} {A : FaceFlagModel P} (laws : FaceFlagCombinationLaws A) (G : HollowPolytopeGeometry d) (points : Fin n → A.flag.Point) (hproper : ∀ (i : Fin n), points i ∈ A.proper) (hintegral : ∀ (i : Fin n), (points i).IsIntegral) (hrational : ∀ (i : Fin n), IsRational (A.physical (points i) ⋯)) (hlarge : hollowPolytopeNumber d < n) : ∃ (weight : Fin n → ℝ) (result : A.flag.Point), ConvexFlag.ConvexCombination points weight result ∧ result.IsIntegral ∧ ∀ (i : Fin n), weight i ≠ 1

Full three-case reduction for a family larger than L(d).

theorem EGZ.FaceFlagCombinationLaws.hellyConstant_le_hollowPolytopeNumber {d : ℕ} {P : RationalPolytope d} {A : FaceFlagModel P} (laws : FaceFlagCombinationLaws A) (G : HollowPolytopeGeometry d) (hrational : ∀ (q : A.flag.Point) (hq : q ∈ A.proper), q.IsIntegral → IsRational (A.physical q hq)) : ConvexFlag.hellyConstant A.proper ≤ hollowPolytopeNumber d

The desired face-flag bound, with no wholesale helly_bound hypothesis. It follows by applying the three-case reduction to a hypothetical Helly-independent family of excessive size.