Support polytopes stay in the centered box

Every lifted support point is centered by definition. The centered real box is convex, so the whole support polytope lies in it. In particular, integer transitions of nonzero local lifts are centered without any additional coordinate bound or large-modulus hypothesis.

theorem EGZ.FlagDecomposition.polytope_subset_centeredBox {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (x : Φ.flag.Node) : (Φ.flag.polytope x).carrier ⊆ Set.Icc (fun (x : Fin (Φ.flag.rank x)) => -↑((p - 1) / 2)) fun (x : Fin (Φ.flag.rank x)) => ↑((p - 1) / 2)

The real support polytope is contained in the centered coordinate box.

theorem EGZ.FlagDecomposition.isCenteredLift_of_mem_polytope {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (x : Φ.flag.Node) (q : IntCoord (Φ.flag.rank x)) (hq : q.real ∈ (Φ.flag.polytope x).carrier) : IsCenteredLift p q

Every integer point of a decomposition polytope is already centered.

theorem EGZ.FlagDecomposition.isCenteredLift_transition_of_mem_polytope {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) {y x : Φ.flag.Node} (h : y ≤ x) (q : IntCoord (Φ.flag.rank y)) (hq : q.real ∈ (Φ.flag.polytope y).carrier) : IsCenteredLift p ((Φ.flag.transition h).integer q)

Centeredness is preserved by a flag transition on integer polytope points.

theorem EGZ.FlagDecomposition.isCenteredLift_transition_of_localLift {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) {y x : Φ.flag.Node} (h : y ≤ x) (q : IntCoord (Φ.flag.rank y)) (hq : Φ.localLift y q ≠ 0) : IsCenteredLift p ((Φ.flag.transition h).integer q)

Transitions of nonzero local lifts stay centered automatically.