Uniform chart parameters for support diagrams

These bounds apply before a finite-field representation has been constructed. Only the ranks and integer support boxes enter the coordinate growth function and the prime threshold.

theorem EGZ.convexHull_subset_coordinateBox {n K : ℕ} {S : Set (IntCoord n)} (hS : ∀ z ∈ S, latticeSupNorm z ≤ K) : (convexHull ℝ) (IntCoord.real '' S) ⊆ Set.Icc (fun (x : Fin n) => -↑K) fun (x : Fin n) => ↑K

theorem EGZ.latticeSupNorm_le_of_mem_convexHull {n K : ℕ} {S : Set (IntCoord n)} (hS : ∀ z ∈ S, latticeSupNorm z ≤ K) (q : IntCoord n) (hq : q.real ∈ (convexHull ℝ) (IntCoord.real '' S)) : latticeSupNorm q ≤ K

theorem EGZ.LatticeSupportDiagram.polytope_bound (D : LatticeSupportDiagram) {K : D.Node → ℕ} (hS : ∀ (x : D.Node), ∀ q ∈ D.support x, latticeSupNorm q ≤ K x) (x : D.Node) (q : IntCoord (D.rank x)) (hq : q.real ∈ (D.polytope x).carrier) : latticeSupNorm q ≤ K x

theorem EGZ.exists_uniform_supportChart_parameters (r : ℕ) : ∃ (A : ℕ → ℕ), Monotone A ∧ (∀ (K : ℕ), K ≤ A K) ∧ ∀ (BK : ℕ), ∃ (p₀ : ℕ), 2 ≤ p₀ ∧ ∀ (p : ℕ) [NeZero p] [Fact (Nat.Prime p)], p₀ < p → ∀ (D : LatticeSupportDiagram) (K : D.Node → ℕ), (∀ (x : D.Node), D.rank x ≤ r) → (∀ (x : D.Node), ∀ q ∈ D.support x, latticeSupNorm q ≤ K x) → (∀ (x : D.Node), K x ≤ BK) → ∃ (C : (x : D.Node) → IntegerLatticeChart (D.support x)), (∀ (x : D.Node), Function.Injective ⇑((D.chart C x).modp p)) ∧ (∀ (x : D.Node), ∀ q ∈ (C x).coordinateSupport, IsCenteredLift p q) ∧ (∀ (x : D.Node) (q : IntCoord (C x).rank), latticeSupNorm ((C x).map q) ≤ K x → latticeSupNorm q ≤ A (K x)) ∧ ∀ (x : D.Node) (q : IntCoord (C x).rank), q.real ∈ ((D.chartedFlag C).polytope x).carrier → latticeSupNorm q ≤ A (K x)