Uniform parameters for minimal lattice coordinates

The coordinate growth function depends only on the ambient dimension. A single prime threshold depending on that dimension and the old uniform box bound makes all chosen chart reductions injective and all new supports centered, simultaneously for every input decomposition.

theorem EGZ.FlagDecomposition.IsKBounded.liftedSupport_bound {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} {Φ : FlagDecomposition p d f} {K : Φ.flag.Node → ℕ} (hΦ : Φ.IsKBounded K) (x : Φ.flag.Node) (z : IntCoord (Φ.flag.rank x)) (hz : z ∈ Φ.liftedSupport x) : latticeSupNorm z ≤ K x

Boundedness on the polytope bounds every lifted support generator.

theorem EGZ.exists_uniform_rechart_parameters (d : ℕ) : ∃ (A : ℕ → ℕ), Monotone A ∧ (∀ (K : ℕ), K ≤ A K) ∧ ∀ (BK : ℕ), ∃ (p₀ : ℕ), 2 ≤ p₀ ∧ ∀ (p : ℕ) [inst : NeZero p] [Fact (Nat.Prime p)], p₀ < p → ∀ (f : FpCoord p d → ℕ) (Φ : FlagDecomposition p d f) (K : Φ.flag.Node → ℕ), Φ.IsKBounded K → (∀ (x : Φ.flag.Node), K x ≤ BK) → ∃ (C : (x : Φ.flag.Node) → IntegerLatticeChart (Φ.liftedSupport x)), (∀ (x : Φ.flag.Node), Function.Injective ⇑((FlagDecomposition.Rechart.chart Φ C x).modp p)) ∧ (∀ (x : Φ.flag.Node), ∀ q ∈ (C x).coordinateSupport, IsCenteredLift p q) ∧ (∀ (x : Φ.flag.Node) (q : IntCoord (C x).rank), latticeSupNorm ((C x).map q) ≤ K x → latticeSupNorm q ≤ A (K x)) ∧ ∀ (x : Φ.flag.Node) (q : IntCoord (C x).rank), q.real ∈ (FlagDecomposition.Rechart.polytope Φ C x).carrier → latticeSupNorm q ≤ A (K x)

Uniform choices for replacing all node lattices with their generated coordinate lattices. The prime threshold is chosen before the prime, input weight, decomposition, and nodewise bounds.