Gap cleanup followed by minimalization

Recharting the reduced gap-cleanup output produces a minimal and reduced decomposition. Its weights, mass, gaps, and node count are unchanged by the coordinate change. Increasing the coordinate bounds only weakens the required inverse-power gap threshold.

theorem EGZ.gapThreshold_antitone_radius {a : ℝ} (ha : 0 ≤ a) {n K B : ℕ} (hn : 0 < n) (hKB : K ≤ B) (d : ℕ) : a / (↑n * (2 * ↑B + 1) ^ d) ≤ a / (↑n * (2 * ↑K + 1) ^ d)

Increasing the box radius decreases the gap threshold.

@[reducible, inline]

noncomputable abbrev EGZ.FlagDecomposition.PrunedWeights.normalized {p d : ℕ} [NeZero p] [Fact (Nat.Prime p)] {f : FpCoord p d → ℕ} {Φ : FlagDecomposition p d f} (D : Φ.PrunedWeights) (hp : Odd p) (C : (x : (D.cleaned hp).flag.Node) → IntegerLatticeChart ((D.cleaned hp).liftedSupport x)) (hmod : ∀ (x : (D.cleaned hp).flag.Node), Function.Injective ⇑((Rechart.chart (D.cleaned hp) C x).modp p)) (hcenter : ∀ (x : (D.cleaned hp).flag.Node), ∀ q ∈ (C x).coordinateSupport, IsCenteredLift p q) : FlagDecomposition p d f

Minimalize the reduced output of gap cleanup.

Equations

• D.normalized hp C hmod hcenter = EGZ.FlagDecomposition.Rechart.decomposition (D.cleaned hp) C hp hmod hcenter

noncomputable def EGZ.FlagDecomposition.PrunedWeights.normalizedNodeEmbedding {p d : ℕ} [NeZero p] [Fact (Nat.Prime p)] {f : FpCoord p d → ℕ} {Φ : FlagDecomposition p d f} (D : Φ.PrunedWeights) (hp : Odd p) (C : (x : (D.cleaned hp).flag.Node) → IntegerLatticeChart ((D.cleaned hp).liftedSupport x)) (hmod : ∀ (x : (D.cleaned hp).flag.Node), Function.Injective ⇑((Rechart.chart (D.cleaned hp) C x).modp p)) (hcenter : ∀ (x : (D.cleaned hp).flag.Node), ∀ q ∈ (C x).coordinateSupport, IsCenteredLift p q) : (D.normalized hp C hmod hcenter).flag.Node ↪ Φ.flag.Node

Embed surviving nodes of the normalized pruning into the original node set.

Equations

• D.normalizedNodeEmbedding hp C hmod hcenter = { toFun := fun (x : (D.normalized hp C hmod hcenter).flag.Node) => ↑↑x, inj' := ⋯ }

@[simp]

theorem EGZ.FlagDecomposition.PrunedWeights.normalized_localWeight {p d : ℕ} [NeZero p] [Fact (Nat.Prime p)] {f : FpCoord p d → ℕ} {Φ : FlagDecomposition p d f} (D : Φ.PrunedWeights) (hp : Odd p) (C : (x : (D.cleaned hp).flag.Node) → IntegerLatticeChart ((D.cleaned hp).liftedSupport x)) (hmod : ∀ (x : (D.cleaned hp).flag.Node), Function.Injective ⇑((Rechart.chart (D.cleaned hp) C x).modp p)) (hcenter : ∀ (x : (D.cleaned hp).flag.Node), ∀ q ∈ (C x).coordinateSupport, IsCenteredLift p q) (x : (D.cleaned hp).flag.Node) : (D.normalized hp C hmod hcenter).localWeight x = D.weight ↑↑x

theorem EGZ.FlagDecomposition.PrunedWeights.normalized_cumulativeWeight {p d : ℕ} [NeZero p] [Fact (Nat.Prime p)] {f : FpCoord p d → ℕ} {Φ : FlagDecomposition p d f} (D : Φ.PrunedWeights) (hp : Odd p) (C : (x : (D.cleaned hp).flag.Node) → IntegerLatticeChart ((D.cleaned hp).liftedSupport x)) (hmod : ∀ (x : (D.cleaned hp).flag.Node), Function.Injective ⇑((Rechart.chart (D.cleaned hp) C x).modp p)) (hcenter : ∀ (x : (D.cleaned hp).flag.Node), ∀ q ∈ (C x).coordinateSupport, IsCenteredLift p q) (x : (D.cleaned hp).flag.Node) : (D.normalized hp C hmod hcenter).cumulativeWeight x = D.cumulative ↑↑x

theorem EGZ.FlagDecomposition.PrunedWeights.normalized_localWeight_le {p d : ℕ} [NeZero p] [Fact (Nat.Prime p)] {f : FpCoord p d → ℕ} {Φ : FlagDecomposition p d f} (D : Φ.PrunedWeights) (hp : Odd p) (C : (x : (D.cleaned hp).flag.Node) → IntegerLatticeChart ((D.cleaned hp).liftedSupport x)) (hmod : ∀ (x : (D.cleaned hp).flag.Node), Function.Injective ⇑((Rechart.chart (D.cleaned hp) C x).modp p)) (hcenter : ∀ (x : (D.cleaned hp).flag.Node), ∀ q ∈ (C x).coordinateSupport, IsCenteredLift p q) (x : (D.cleaned hp).flag.Node) (v : FpCoord p d) : (D.normalized hp C hmod hcenter).localWeight x v ≤ Φ.localWeight (↑↑x) v

theorem EGZ.FlagDecomposition.PrunedWeights.normalized_cumulativeWeight_le {p d : ℕ} [NeZero p] [Fact (Nat.Prime p)] {f : FpCoord p d → ℕ} {Φ : FlagDecomposition p d f} (D : Φ.PrunedWeights) (hp : Odd p) (C : (x : (D.cleaned hp).flag.Node) → IntegerLatticeChart ((D.cleaned hp).liftedSupport x)) (hmod : ∀ (x : (D.cleaned hp).flag.Node), Function.Injective ⇑((Rechart.chart (D.cleaned hp) C x).modp p)) (hcenter : ∀ (x : (D.cleaned hp).flag.Node), ∀ q ∈ (C x).coordinateSupport, IsCenteredLift p q) (x : (D.cleaned hp).flag.Node) (v : FpCoord p d) : (D.normalized hp C hmod hcenter).cumulativeWeight x v ≤ Φ.cumulativeWeight (↑↑x) v

theorem EGZ.FlagDecomposition.PrunedWeights.normalized_retainedWeight {p d : ℕ} [NeZero p] [Fact (Nat.Prime p)] {f : FpCoord p d → ℕ} {Φ : FlagDecomposition p d f} (D : Φ.PrunedWeights) (hp : Odd p) (C : (x : (D.cleaned hp).flag.Node) → IntegerLatticeChart ((D.cleaned hp).liftedSupport x)) (hmod : ∀ (x : (D.cleaned hp).flag.Node), Function.Injective ⇑((Rechart.chart (D.cleaned hp) C x).modp p)) (hcenter : ∀ (x : (D.cleaned hp).flag.Node), ∀ q ∈ (C x).coordinateSupport, IsCenteredLift p q) : (D.normalized hp C hmod hcenter).retainedWeight = FlagDecompositionRaw.retainedWeight D.weight

theorem EGZ.FlagDecomposition.PrunedWeights.normalized_retainedWeight_le {p d : ℕ} [NeZero p] [Fact (Nat.Prime p)] {f : FpCoord p d → ℕ} {Φ : FlagDecomposition p d f} (D : Φ.PrunedWeights) (hp : Odd p) (C : (x : (D.cleaned hp).flag.Node) → IntegerLatticeChart ((D.cleaned hp).liftedSupport x)) (hmod : ∀ (x : (D.cleaned hp).flag.Node), Function.Injective ⇑((Rechart.chart (D.cleaned hp) C x).modp p)) (hcenter : ∀ (x : (D.cleaned hp).flag.Node), ∀ q ∈ (C x).coordinateSupport, IsCenteredLift p q) (v : FpCoord p d) : (D.normalized hp C hmod hcenter).retainedWeight v ≤ Φ.retainedWeight v

@[simp]

theorem EGZ.FlagDecomposition.PrunedWeights.normalized_retainedMass {p d : ℕ} [NeZero p] [Fact (Nat.Prime p)] {f : FpCoord p d → ℕ} {Φ : FlagDecomposition p d f} (D : Φ.PrunedWeights) (hp : Odd p) (C : (x : (D.cleaned hp).flag.Node) → IntegerLatticeChart ((D.cleaned hp).liftedSupport x)) (hmod : ∀ (x : (D.cleaned hp).flag.Node), Function.Injective ⇑((Rechart.chart (D.cleaned hp) C x).modp p)) (hcenter : ∀ (x : (D.cleaned hp).flag.Node), ∀ q ∈ (C x).coordinateSupport, IsCenteredLift p q) : (D.normalized hp C hmod hcenter).retainedMass = (D.cleaned hp).retainedMass

@[simp]

theorem EGZ.FlagDecomposition.PrunedWeights.normalized_gap {p d : ℕ} [NeZero p] [Fact (Nat.Prime p)] {f : FpCoord p d → ℕ} {Φ : FlagDecomposition p d f} (D : Φ.PrunedWeights) (hp : Odd p) (C : (x : (D.cleaned hp).flag.Node) → IntegerLatticeChart ((D.cleaned hp).liftedSupport x)) (hmod : ∀ (x : (D.cleaned hp).flag.Node), Function.Injective ⇑((Rechart.chart (D.cleaned hp) C x).modp p)) (hcenter : ∀ (x : (D.cleaned hp).flag.Node), ∀ q ∈ (C x).coordinateSupport, IsCenteredLift p q) (x : (D.cleaned hp).flag.Node) : (D.normalized hp C hmod hcenter).gap x = (D.cleaned hp).gap x

theorem EGZ.FlagDecomposition.PrunedWeights.normalized_hat {p d : ℕ} [NeZero p] [Fact (Nat.Prime p)] {f : FpCoord p d → ℕ} {Φ : FlagDecomposition p d f} (D : Φ.PrunedWeights) (hp : Odd p) (C : (x : (D.cleaned hp).flag.Node) → IntegerLatticeChart ((D.cleaned hp).liftedSupport x)) (hmod : ∀ (x : (D.cleaned hp).flag.Node), Function.Injective ⇑((Rechart.chart (D.cleaned hp) C x).modp p)) (hcenter : ∀ (x : (D.cleaned hp).flag.Node), ∀ q ∈ (C x).coordinateSupport, IsCenteredLift p q) (x : (D.cleaned hp).flag.Node) (q : IntCoord (C x).rank) : (D.normalized hp C hmod hcenter).hat x q = D.hat (↑↑x) ((C x).map q)

theorem EGZ.FlagDecomposition.PrunedWeights.normalized_localLift {p d : ℕ} [NeZero p] [Fact (Nat.Prime p)] {f : FpCoord p d → ℕ} {Φ : FlagDecomposition p d f} (D : Φ.PrunedWeights) (hp : Odd p) (C : (x : (D.cleaned hp).flag.Node) → IntegerLatticeChart ((D.cleaned hp).liftedSupport x)) (hmod : ∀ (x : (D.cleaned hp).flag.Node), Function.Injective ⇑((Rechart.chart (D.cleaned hp) C x).modp p)) (hcenter : ∀ (x : (D.cleaned hp).flag.Node), ∀ q ∈ (C x).coordinateSupport, IsCenteredLift p q) (x : (D.cleaned hp).flag.Node) (q : IntCoord (C x).rank) : (D.normalized hp C hmod hcenter).localLift x q = D.localLift (↑↑x) ((C x).map q)

theorem EGZ.FlagDecomposition.PrunedWeights.normalized_isMinimal {p d : ℕ} [NeZero p] [Fact (Nat.Prime p)] {f : FpCoord p d → ℕ} {Φ : FlagDecomposition p d f} (D : Φ.PrunedWeights) (hp : Odd p) (C : (x : (D.cleaned hp).flag.Node) → IntegerLatticeChart ((D.cleaned hp).liftedSupport x)) (hmod : ∀ (x : (D.cleaned hp).flag.Node), Function.Injective ⇑((Rechart.chart (D.cleaned hp) C x).modp p)) (hcenter : ∀ (x : (D.cleaned hp).flag.Node), ∀ q ∈ (C x).coordinateSupport, IsCenteredLift p q) : (D.normalized hp C hmod hcenter).IsMinimal

theorem EGZ.FlagDecomposition.PrunedWeights.normalized_isReduced {p d : ℕ} [NeZero p] [Fact (Nat.Prime p)] {f : FpCoord p d → ℕ} {Φ : FlagDecomposition p d f} (D : Φ.PrunedWeights) (hp : Odd p) (C : (x : (D.cleaned hp).flag.Node) → IntegerLatticeChart ((D.cleaned hp).liftedSupport x)) (hmod : ∀ (x : (D.cleaned hp).flag.Node), Function.Injective ⇑((Rechart.chart (D.cleaned hp) C x).modp p)) (hcenter : ∀ (x : (D.cleaned hp).flag.Node), ∀ q ∈ (C x).coordinateSupport, IsCenteredLift p q) : (D.normalized hp C hmod hcenter).IsReduced

theorem EGZ.FlagDecomposition.PrunedWeights.normalized_card_eq {p d : ℕ} [NeZero p] [Fact (Nat.Prime p)] {f : FpCoord p d → ℕ} {Φ : FlagDecomposition p d f} (D : Φ.PrunedWeights) (hp : Odd p) (C : (x : (D.cleaned hp).flag.Node) → IntegerLatticeChart ((D.cleaned hp).liftedSupport x)) (hmod : ∀ (x : (D.cleaned hp).flag.Node), Function.Injective ⇑((Rechart.chart (D.cleaned hp) C x).modp p)) (hcenter : ∀ (x : (D.cleaned hp).flag.Node), ∀ q ∈ (C x).coordinateSupport, IsCenteredLift p q) : Fintype.card (D.normalized hp C hmod hcenter).flag.Node = Fintype.card (D.cleaned hp).flag.Node

theorem EGZ.FlagDecomposition.PrunedWeights.normalized_card_le {p d : ℕ} [NeZero p] [Fact (Nat.Prime p)] {f : FpCoord p d → ℕ} {Φ : FlagDecomposition p d f} (D : Φ.PrunedWeights) (hp : Odd p) (C : (x : (D.cleaned hp).flag.Node) → IntegerLatticeChart ((D.cleaned hp).liftedSupport x)) (hmod : ∀ (x : (D.cleaned hp).flag.Node), Function.Injective ⇑((Rechart.chart (D.cleaned hp) C x).modp p)) (hcenter : ∀ (x : (D.cleaned hp).flag.Node), ∀ q ∈ (C x).coordinateSupport, IsCenteredLift p q) : Fintype.card (D.normalized hp C hmod hcenter).flag.Node ≤ Fintype.card Φ.flag.Node

theorem EGZ.FlagDecomposition.PrunedWeights.normalized_isKBounded {p d : ℕ} [NeZero p] [Fact (Nat.Prime p)] {f : FpCoord p d → ℕ} {Φ : FlagDecomposition p d f} (D : Φ.PrunedWeights) (hp : Odd p) (C : (x : (D.cleaned hp).flag.Node) → IntegerLatticeChart ((D.cleaned hp).liftedSupport x)) (hmod : ∀ (x : (D.cleaned hp).flag.Node), Function.Injective ⇑((Rechart.chart (D.cleaned hp) C x).modp p)) (hcenter : ∀ (x : (D.cleaned hp).flag.Node), ∀ q ∈ (C x).coordinateSupport, IsCenteredLift p q) {K : Φ.flag.Node → ℕ} {B : (D.cleaned hp).flag.Node → ℕ} (hK : Φ.IsKBounded K) (hC : ∀ (x : (D.cleaned hp).flag.Node) (q : IntCoord (C x).rank), latticeSupNorm ((C x).map q) ≤ K ↑↑x → latticeSupNorm q ≤ B x) : (D.normalized hp C hmod hcenter).IsKBounded B

theorem EGZ.FlagDecomposition.PrunedWeights.normalized_retainedMass_loss_le {p d : ℕ} [NeZero p] [Fact (Nat.Prime p)] {f : FpCoord p d → ℕ} {Φ : FlagDecomposition p d f} (D : Φ.PrunedWeights) (hp : Odd p) (C : (x : (D.cleaned hp).flag.Node) → IntegerLatticeChart ((D.cleaned hp).liftedSupport x)) (hmod : ∀ (x : (D.cleaned hp).flag.Node), Function.Injective ⇑((Rechart.chart (D.cleaned hp) C x).modp p)) (hcenter : ∀ (x : (D.cleaned hp).flag.Node), ∀ q ∈ (C x).coordinateSupport, IsCenteredLift p q) {α : ℝ} (hmass : (1 - α) * ↑Φ.retainedMass ≤ ↑(D.cleaned hp).retainedMass) : ↑Φ.retainedMass - ↑(D.normalized hp C hmod hcenter).retainedMass ≤ α * ↑Φ.retainedMass

The coordinate change preserves the already established mass-loss bound.

theorem EGZ.FlagDecomposition.PrunedWeights.normalized_gap_bound {p d : ℕ} [NeZero p] [Fact (Nat.Prime p)] {f : FpCoord p d → ℕ} {Φ : FlagDecomposition p d f} (D : Φ.PrunedWeights) (hp : Odd p) (C : (x : (D.cleaned hp).flag.Node) → IntegerLatticeChart ((D.cleaned hp).liftedSupport x)) (hmod : ∀ (x : (D.cleaned hp).flag.Node), Function.Injective ⇑((Rechart.chart (D.cleaned hp) C x).modp p)) (hcenter : ∀ (x : (D.cleaned hp).flag.Node), ∀ q ∈ (C x).coordinateSupport, IsCenteredLift p q) {K : Φ.flag.Node → ℕ} {B : (D.cleaned hp).flag.Node → ℕ} {α : ℝ} (hα : 0 ≤ α) (hKB : ∀ (x : (D.cleaned hp).flag.Node), K ↑↑x ≤ B x) (hgap : ∀ (x : (D.cleaned hp).flag.Node), α * ↑Φ.retainedMass / (↑(Fintype.card Φ.flag.Node) * (2 * ↑(K ↑↑x) + 1) ^ d) ≤ ↑((D.cleaned hp).gap x)) (x : (D.cleaned hp).flag.Node) : α * ↑Φ.retainedMass / (↑(Fintype.card Φ.flag.Node) * (2 * ↑(B x) + 1) ^ d) ≤ ↑((D.normalized hp C hmod hcenter).gap x)

A gap bound in the old coordinates remains valid at larger coordinate bounds after recharting. The denominator uses the old node count.

noncomputable def EGZ.FlagDecomposition.PrunedWeights.normalizedSubdivisionMap {p d : ℕ} [NeZero p] [Fact (Nat.Prime p)] {f : FpCoord p d → ℕ} {Φ : FlagDecomposition p d f} (D : Φ.PrunedWeights) (hp : Odd p) (C : (x : (D.cleaned hp).flag.Node) → IntegerLatticeChart ((D.cleaned hp).liftedSupport x)) (hmod : ∀ (x : (D.cleaned hp).flag.Node), Function.Injective ⇑((Rechart.chart (D.cleaned hp) C x).modp p)) (hcenter : ∀ (x : (D.cleaned hp).flag.Node), ∀ q ∈ (C x).coordinateSupport, IsCenteredLift p q) : Φ.SubdivisionMap (D.normalized hp C hmod hcenter)

The subdivision map obtained by cleaning and normalizing the pruned weights.

Equations

• D.normalizedSubdivisionMap hp C hmod hcenter = (D.cleanedSubdivisionMap hp).comp (EGZ.FlagDecomposition.Rechart.subdivisionMap (D.cleaned hp) C hp hmod hcenter)

@[simp]

theorem EGZ.FlagDecomposition.PrunedWeights.normalizedSubdivisionMap_node {p d : ℕ} [NeZero p] [Fact (Nat.Prime p)] {f : FpCoord p d → ℕ} {Φ : FlagDecomposition p d f} (D : Φ.PrunedWeights) (hp : Odd p) (C : (x : (D.cleaned hp).flag.Node) → IntegerLatticeChart ((D.cleaned hp).liftedSupport x)) (hmod : ∀ (x : (D.cleaned hp).flag.Node), Function.Injective ⇑((Rechart.chart (D.cleaned hp) C x).modp p)) (hcenter : ∀ (x : (D.cleaned hp).flag.Node), ∀ q ∈ (C x).coordinateSupport, IsCenteredLift p q) (x : (D.cleaned hp).flag.Node) : (D.normalizedSubdivisionMap hp C hmod hcenter).node x = ↑↑x

theorem EGZ.FlagDecomposition.PrunedWeights.normalized_isRealizedFace {p d : ℕ} [NeZero p] [Fact (Nat.Prime p)] {f : FpCoord p d → ℕ} {Φ : FlagDecomposition p d f} (D : Φ.PrunedWeights) (hp : Odd p) (C : (x : (D.cleaned hp).flag.Node) → IntegerLatticeChart ((D.cleaned hp).liftedSupport x)) (hmod : ∀ (x : (D.cleaned hp).flag.Node), Function.Injective ⇑((Rechart.chart (D.cleaned hp) C x).modp p)) (hcenter : ∀ (x : (D.cleaned hp).flag.Node), ∀ q ∈ (C x).coordinateSupport, IsCenteredLift p q) (x : (D.cleaned hp).flag.Node) (Γ : (Φ.flag.polytope ↑↑x).Face) (hne : (((D.normalized hp C hmod hcenter).flag.polytope x).carrier ∩ ⇑((D.normalizedSubdivisionMap hp C hmod hcenter).fibre x) ⁻¹' Γ.carrier).Nonempty) (hΓ : Φ.IsRealizedFace (↑↑x) Γ) : (D.normalized hp C hmod hcenter).IsRealizedFace x ((D.normalizedSubdivisionMap hp C hmod hcenter).face x Γ hne)

theorem EGZ.FlagDecomposition.PrunedWeights.normalized_isCompleteElement {p d : ℕ} [NeZero p] [Fact (Nat.Prime p)] {f : FpCoord p d → ℕ} {Φ : FlagDecomposition p d f} (D : Φ.PrunedWeights) (hp : Odd p) (C : (x : (D.cleaned hp).flag.Node) → IntegerLatticeChart ((D.cleaned hp).liftedSupport x)) (hmod : ∀ (x : (D.cleaned hp).flag.Node), Function.Injective ⇑((Rechart.chart (D.cleaned hp) C x).modp p)) (hcenter : ∀ (x : (D.cleaned hp).flag.Node), ∀ q ∈ (C x).coordinateSupport, IsCenteredLift p q) {x : (D.cleaned hp).flag.Node} {t : ℕ} {ε δ α : ℝ} (hε : 0 < ε) (hα : 0 ≤ α) (hlarge : Φ.IsLargeElement ε ↑↑x) (hcomplete : Φ.IsCompleteElement (↑↑x) t δ) (hloss : ↑Φ.retainedMass - ↑(D.normalized hp C hmod hcenter).retainedMass ≤ α * ↑Φ.retainedMass) : (D.normalized hp C hmod hcenter).IsCompleteElement x t (δ - α / ε)

theorem EGZ.normalized_gap_cleanup_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) → ∀ (α : ℝ), 0 ≤ α → α < 1 → ∃ (D : Φ.PrunedWeights) (hp : Odd p) (C : (x : (D.cleaned hp).flag.Node) → IntegerLatticeChart ((D.cleaned hp).liftedSupport x)) (hmod : ∀ (x : (D.cleaned hp).flag.Node), Function.Injective ⇑((FlagDecomposition.Rechart.chart (D.cleaned hp) C x).modp p)) (hcenter : ∀ (x : (D.cleaned hp).flag.Node), ∀ q ∈ (C x).coordinateSupport, IsCenteredLift p q), let Ψ := D.normalized hp C hmod hcenter; (∀ (x : Φ.flag.Node) (v : FpCoord p d), D.weight x v = 0 ∨ D.weight x v = Φ.localWeight x v) ∧ Ψ.IsMinimal ∧ Ψ.IsReduced ∧ (Ψ.IsKBounded fun (x : Ψ.flag.Node) => A (K ↑↑x)) ∧ Fintype.card Ψ.flag.Node ≤ Fintype.card Φ.flag.Node ∧ ↑Φ.retainedMass - ↑Ψ.retainedMass ≤ α * ↑Φ.retainedMass ∧ ∀ (x : Ψ.flag.Node), α * ↑Φ.retainedMass / (↑(Fintype.card Φ.flag.Node) * (2 * ↑(A (K ↑↑x)) + 1) ^ d) ≤ ↑(Ψ.gap x)

Uniform normalized gap cleanup. The coordinate growth function depends only on dimension, and the prime threshold only on the old uniform bound. The resulting operation is both minimal and reduced.