Uniform parameters for complete-element refinements

The coordinate growth function is selected using only the ambient dimension. Iterating a growth step gives all slab widths and a prime threshold uniform over the input decomposition, its local masses, and the selected anchor.

theorem EGZ.exists_uniform_completePreparation_charts (d : ℕ) (g : ℕ → ℕ) : ∃ (A : ℕ → ℕ), Monotone A ∧ (∀ (K : ℕ), K ≤ A K) ∧ ∀ (K : ℕ), ∃ (p₀ : ℕ), 2 ≤ p₀ ∧ ∀ (p : ℕ) [inst : NeZero p] [inst_1 : Fact (Nat.Prime p)], p₀ < p → ∃ (hp : Odd p), ∀ (f : FpCoord p d → ℕ) (Φ : FlagDecomposition p d f) (anchor : Φ.flag.Node) (δ : ℝ) (hδ : 0 ≤ δ) (hsmall : 3 ^ (d + 1) * δ < 1) (D : Φ.CompletePreparation anchor (refinementWidth A g K) δ), (Φ.IsKBounded fun (x : Φ.flag.Node) => K) → (∀ (i : Fin D.count), 2 * refinementWidth A g K (↑i + 1) < p) ∧ ∃ (C : (x : (D.diagram hp hδ hsmall).Node) → IntegerLatticeChart ((D.diagram hp hδ hsmall).support x)), (∀ (x : (D.diagram hp hδ hsmall).Node), Function.Injective ⇑(((D.diagram hp hδ hsmall).chart C x).modp p)) ∧ (∀ (x : (D.diagram hp hδ hsmall).Node), ∀ q ∈ (C x).coordinateSupport, IsCenteredLift p q) ∧ ∀ (x : (D.diagram hp hδ hsmall).Node) (q : IntCoord (C x).rank), q.real ∈ (((D.diagram hp hδ hsmall).chartedFlag C).polytope x).carrier → latticeSupNorm q ≤ A (refinementWidth A g K D.count)

All possible maximal thin-direction preparations share one prime threshold. The chart bound uses their actual number of selected directions.

theorem EGZ.complete_refinement_lemma (d : ℕ) (g : ℕ → ℕ) (hg : Monotone g) : ∃ (B : ℕ → ℕ), Monotone B ∧ (∀ (K : ℕ), K ≤ B K) ∧ ∀ (K : ℕ), ∃ (p₀ : ℕ), 2 ≤ p₀ ∧ ∀ (p : ℕ) [inst : NeZero p] [inst_1 : Fact (Nat.Prime p)], p₀ < p → ∀ (f : FpCoord p d → ℕ) (Φ : FlagDecomposition p d f) (anchor : Φ.flag.Node) (δ : ℝ) (hδ : 0 ≤ δ) (hsmall : 3 ^ (d + 1) * δ < 1), (Φ.IsKBounded fun (x : Φ.flag.Node) => K) → ∃ (hp : Odd p) (t : ℕ → ℕ) (D : Φ.CompletePreparation anchor t δ) (C : (x : (D.diagram hp hδ hsmall).Node) → IntegerLatticeChart ((D.diagram hp hδ hsmall).support x)) (hmod : ∀ (x : (D.diagram hp hδ hsmall).Node), Function.Injective ⇑((IntegralAffineMap.ofIntAffineMap (C x).map).modp p)) (hcenter : ∀ (x : (D.diagram hp hδ hsmall).Node), ∀ q ∈ (C x).coordinateSupport, IsCenteredLift p q) (b : ℕ), let Ψ := D.refined hp hδ hsmall C hmod hcenter; have S := D.refinedSubdivisionMap hp hδ hsmall C hmod hcenter; K ≤ b ∧ b ≤ B K ∧ Monotone t ∧ t 0 = K ∧ g b ≤ t (D.count + 1) ∧ Ψ.IsMinimal ∧ (Ψ.IsKBounded fun (x : Ψ.flag.Node) => b) ∧ (Antitone fun (x : Ψ.flag.Node) => b) ∧ ↑Φ.retainedMass - ↑Ψ.retainedMass ≤ 3 ^ (d + 1) * δ * ↑(natMass (Φ.cumulativeWeight anchor)) ∧ Fintype.card Ψ.flag.Node ≤ 2 * Fintype.card Φ.flag.Node ∧ Ψ.IsCompleteElement (D.lowerAnchor hp hδ hsmall) (g b) δ ∧ D.completeNode hp hδ hsmall C hmod hcenter ≤ D.lowerAnchor hp hδ hsmall ∧ Ψ.IsReducedElement (D.completeNode hp hδ hsmall C hmod hcenter) ∧ Ψ.IsCompleteElement (D.completeNode hp hδ hsmall C hmod hcenter) (g b) δ ∧ Ψ.cumulativeWeight (D.completeNode hp hδ hsmall C hmod hcenter) = Ψ.cumulativeWeight (D.lowerAnchor hp hδ hsmall) ∧ ¬Ψ.IsReducedElement (D.upperAnchor hp hδ hsmall) ∧ S.node (D.lowerAnchor hp hδ hsmall) = anchor ∧ S.node (D.upperAnchor hp hδ hsmall) = anchor ∧ ∀ (x : Ψ.flag.Node) (Γ : (Φ.flag.polytope (S.node x)).Face) (hne : ((Ψ.flag.polytope x).carrier ∩ ⇑⋯ ⁻¹' Γ.carrier).Nonempty), Φ.IsRealizedFace (S.node x) Γ → Ψ.IsRealizedFace x (S.face x Γ hne)

A uniform complete-element refinement, retaining its concrete direction preparation and lattice charts. The output radius is bounded by one monotone function of the original radius; its reduced complete node and non-reduced upper anchor are explicit nodes of the constructed two-layer flag.