Regression checks for Proposition 7.1

The proof of Proposition 7.1 has two algebraic inputs which are independent of the long flag-decomposition argument:

• a family longer than hollowConstant p d has a nontrivial zero combination of total weight p;
• an integer-coordinate affine average whose numerator vanishes modulo p is again an integer point.

Keeping these as standalone, proved lemmas prevents the later flag interface from hiding either step in an axiom.

The affine cancellation used by the representation

theorem EGZ.exists_nontrivial_zero_combination_of_hollowConstant_lt {p d n : ℕ} (hp : Nat.Prime p) (hn : hollowConstant p d < n) (v : Fin n → FpVec p d) : ∃ (α : Fin n → ℕ), ∑ i : Fin n, α i = p ∧ ∑ i : Fin n, α i • v i = 0 ∧ ∀ (i : Fin n), α i < p

If a family is longer than the extremal p-hollow length, it admits a zero combination of total weight p in which every coefficient is strictly less than p.

This is the exact operational consequence of n > 𝔴(𝔽_p^d) used in Proposition 7.1.

theorem EGZ.isIntegral_weighted_average_of_mod_eq_zero {p n : ℕ} {I : Type u_1} [Fintype I] (hp : 0 < p) (α : I → ℕ) (z : I → IntCoord n) (hmod : ∑ i : I, α i • IntCoord.mod p (z i) = 0) : IsIntegral (∑ i : I, (↑(α i) / ↑p) • (z i).real)

Coordinate form of the affine-lattice calculation in equation zero of the proof of Proposition 7.1.

The vectors z i are coordinates relative to an affine lattice origin. Vanishing of the integer numerator modulo p says precisely that its normalized real sum has integer coordinates. In Proposition 7.1 the additional equality ∑ α = p makes this normalized sum an affine combination, but it is not needed for the divisibility calculation itself.

The representation-level barycenter calculation

theorem EGZ.FpRepresentation.convexCombination_isIntegral_of_zero_sum {p d n : ℕ} (hp : Nat.Prime p) {F : ConvexFlag} (R : FpRepresentation p d F) (points : Fin n → F.Point) (z : (i : Fin n) → IntCoord (F.rank (points i).base)) (hz : ∀ (i : Fin n), (z i).real = (points i).val) (v : Fin n → FpCoord p d) (hvspace : ∀ (i : Fin n), v i ∈ R.space (points i).base) (hvmap : ∀ (i : Fin n), (R.map (points i).base) (v i) = IntCoord.mod p (z i)) (α : Fin n → ℕ) (hαsum : ∑ i : Fin n, α i = p) (hαzero : ∑ i : Fin n, α i • v i = 0) (result : F.Point) (hcomb : ConvexFlag.ConvexCombination points (fun (i : Fin n) => ↑(α i) / ↑p) result) : result.IsIntegral

Regression form of equation comb2 followed by equation zero in the proof of Proposition 7.1.

Each integral flag point is lifted to the representing affine subspace over ZMod p. A zero combination of those lifts, with total natural weight p, gives an integral convex-combination result. The proof checks both places where affine (rather than linear) coordinates matter: compatibility with the transition map, and cancellation of the translation term because the coefficient sum is zero in ZMod p.

theorem EGZ.FpRepresentation.hellyIndependent_card_le_hollowConstant {p d n : ℕ} (hp : Nat.Prime p) {F : ConvexFlag} (R : FpRepresentation p d F) {Omega : F.ProperPointSet} {points : Fin n → F.Point} (hind : ConvexFlag.HellyIndependent Omega points) : n ≤ hollowConstant p d

The cardinality contradiction at the heart of Proposition 7.1.

This version deliberately assumes only an FpRepresentation; none of the minimality, reducedness, completeness, mass, or face conditions of a flag decomposition enter the proof.

theorem EGZ.FpRepresentation.hellyConstant_le_hollowConstant {p d : ℕ} (hp : Nat.Prime p) {F : ConvexFlag} (R : FpRepresentation p d F) (Omega : F.ProperPointSet) : ConvexFlag.hellyConstant Omega ≤ hollowConstant p d

Proposition 7.1 at the level of an arbitrary representation.

theorem EGZ.FlagDecomposition.propositionSevenOne {p d : ℕ} [NeZero p] (hp : Nat.Prime p) {f : FpCoord p d → ℕ} (Phi : FlagDecomposition p d f) : ConvexFlag.hellyConstant Phi.properPoints ≤ hollowConstant p d

Proposition 7.1 (lbound) for the proper-point set of a flag decomposition. The proof factors through the representation-only result above, recording precisely which part of the Section 4 structure it uses.