Reduction of hollow polytopes modulo a prime

This module proves the geometric bridge used by the polynomial method. For every hollow rational polytope, a sufficiently large prime sees its vertices as a p-hollow configuration. The proof uses integral homogenization and uniform saturation of the submodules generated by the vertices of every face.

theorem EGZ.IntCoord.exists_smul_eq_of_mod_eq_zero {p d : ℕ} (x : IntCoord d) (h : mod p x = 0) : ∃ (z : IntCoord d), ↑p • z = x

Lift a coordinatewise zero reduction modulo p to divisibility by p in the integral coordinate module.

theorem EGZ.RationalPolytope.hasPrimeHollowReduction_of_isHollow {d : ℕ} (P : RationalPolytope d) (hP : P.IsHollow) : P.HasPrimeHollowReduction

The vertices of every hollow rational polytope admit a p-hollow reduction for some prime p.

theorem EGZ.hollowReductionBridge (d : ℕ) : HollowReductionBridge d

The unconditional dimensionwise reduction bridge from hollow rational polytopes to prime-field p-hollow configurations.