The minimal decomposition lemma

A bounded flag decomposition can be expressed in its support-generated lattice coordinates for every sufficiently large prime. The new decomposition has the same nodes and local weights, is minimal, and preserves gaps, reducedness, element completeness, and realized faces under chart pullback. The coordinate growth function depends only on dimension, and the prime threshold depends only on dimension and the original uniform box bound.

theorem EGZ.minimalization_lemma (d : ℕ) : ∃ (A : ℕ → ℕ), Monotone A ∧ (∀ (K : ℕ), K ≤ A K) ∧ ∀ (BK : ℕ), ∃ (p₀ : ℕ), 2 ≤ p₀ ∧ ∀ (p : ℕ) [inst : NeZero p] [inst_1 : 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)) (hp : Odd p) (hinj : ∀ (x : Φ.flag.Node), Function.Injective ⇑((FlagDecomposition.Rechart.chart Φ C x).modp p)) (hcenter : ∀ (x : Φ.flag.Node), ∀ q ∈ (C x).coordinateSupport, IsCenteredLift p q), let Ψ := FlagDecomposition.Rechart.decomposition Φ C hp hinj hcenter; Ψ.IsMinimal ∧ (Ψ.IsKBounded fun (x : Ψ.flag.Node) => A (K x)) ∧ (∀ (x : Ψ.flag.Node), Ψ.localWeight x = Φ.localWeight x) ∧ (∀ (x : Ψ.flag.Node), Ψ.cumulativeWeight x = Φ.cumulativeWeight x) ∧ Ψ.retainedWeight = Φ.retainedWeight ∧ Ψ.retainedMass = Φ.retainedMass ∧ (∀ (x : Ψ.flag.Node), Ψ.gap x = Φ.gap x) ∧ (∀ (x : Ψ.flag.Node) (q : IntCoord (Ψ.flag.rank x)), Ψ.hat x q = Φ.hat x ((C x).map q)) ∧ (∀ (x : Ψ.flag.Node) (q : IntCoord (Ψ.flag.rank x)), Ψ.localLift x q = Φ.localLift x ((C x).map q)) ∧ (Ψ.IsReduced ↔ Φ.IsReduced) ∧ (∀ (x : Φ.flag.Node) (t : ℕ) (δ : ℝ), Φ.IsCompleteElement x t δ → Ψ.IsCompleteElement x t δ) ∧ ∀ (x : Φ.flag.Node) (Γ : (Φ.flag.polytope x).Face), Φ.IsRealizedFace x Γ → Ψ.IsRealizedFace x ((FlagDecomposition.Rechart.subdivisionMap Φ C hp hinj hcenter).face x Γ ⋯)

Uniform form of the paper's minimal decomposition lemma. The output is the actual recharted decomposition, so its node poset is definitionally the original node poset. Local and cumulative lifted weights are identified by the chart maps; retained mass and every node gap are unchanged.