Finite gap cleanup

The numerical core of the gap cleanup lemma removes an entire fibre whenever its positive mass is at most its threshold. Each fibre can be charged only once: after deletion its mass remains zero. Strong induction on the remaining finite set of fibres proves termination and the total mass bound together.

theorem EGZ.exists_gap_pruning {α : Type u_1} {β : Type u_2} [Fintype α] (s : Finset β) (fibre : β → Set α) (threshold : β → ℝ) (hnonneg : ∀ b ∈ s, 0 ≤ threshold b) (w : α → ℕ) : ∃ (w' : α → ℕ), (∀ (a : α), w' a = 0 ∨ w' a = w a) ∧ w' ≤ w ∧ (∀ b ∈ s, natMassOn w' (fibre b) = 0 ∨ threshold b < ↑(natMassOn w' (fibre b))) ∧ ↑(natMass w) - ↑(natMass w') ≤ ∑ b ∈ s, threshold b

Simultaneous gap cleanup for any finite family of sets of atoms. The resulting weight is obtained only by deleting atoms, all surviving fibre masses exceed their thresholds, and the loss is at most the sum of thresholds. No disjointness assumption on the sets is needed.

theorem EGZ.FlagDecompositionRaw.cumulativeWeight_mono {p d : ℕ} {F : ConvexFlag} {pieces pieces' : F.Node → FpCoord p d → ℕ} (hle : ∀ (x : F.Node) (v : FpCoord p d), pieces' x v ≤ pieces x v) (x : F.Node) (v : FpCoord p d) : cumulativeWeight pieces' x v ≤ cumulativeWeight pieces x v

theorem EGZ.FlagDecompositionRaw.hat_mono {p d : ℕ} [NeZero p] {F : ConvexFlag} (R : FpRepresentation p d F) {pieces pieces' : F.Node → FpCoord p d → ℕ} (hle : ∀ (x : F.Node) (v : FpCoord p d), pieces' x v ≤ pieces x v) (x : F.Node) (q : IntCoord (F.rank x)) : hat R pieces' x q ≤ hat R pieces x q

def EGZ.FlagDecompositionRaw.cumulativeFibre {p d : ℕ} {F : ConvexFlag} (R : FpRepresentation p d F) (x : F.Node) (q : IntCoord (F.rank x)) : Set (F.Node × FpCoord p d)

The atoms in a cumulative coordinate fibre. Atoms remember their local node, so overlapping ambient supports do not cause double counting.

Equations

• EGZ.FlagDecompositionRaw.cumulativeFibre R x q = {a : F.Node × EGZ.FpCoord p d | a.1 ≤ x ∧ (R.map x) a.2 = EGZ.IntCoord.mod p q}

theorem EGZ.FlagDecompositionRaw.hat_eq_natMassOn {p d : ℕ} [NeZero p] {F : ConvexFlag} (R : FpRepresentation p d F) (pieces : F.Node → FpCoord p d → ℕ) (x : F.Node) (q : IntCoord (F.rank x)) (hq : IsCenteredLift p q) : hat R pieces x q = natMassOn (fun (a : F.Node × FpCoord p d) => pieces a.1 a.2) (cumulativeFibre R x q)

theorem EGZ.FlagDecompositionRaw.natMass_retainedWeight {p d : ℕ} [NeZero p] {F : ConvexFlag} (pieces : F.Node → FpCoord p d → ℕ) : natMass (retainedWeight pieces) = natMass fun (a : F.Node × FpCoord p d) => pieces a.1 a.2

theorem EGZ.FlagDecomposition.gap_pos {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (x : Φ.flag.Node) : 0 < Φ.gap x

theorem EGZ.FlagDecomposition.gap_le_hat {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (x : Φ.flag.Node) (q : IntCoord (Φ.flag.rank x)) (hq : Φ.hat x q ≠ 0) : Φ.gap x ≤ Φ.hat x q

theorem EGZ.FlagDecomposition.card_liftedSupport_le {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) {K : Φ.flag.Node → ℕ} (hK : Φ.IsKBounded K) (x : Φ.flag.Node) : (Φ.liftedSupport x).card ≤ (2 * K x + 1) ^ Φ.flag.rank x

A coordinate bound controls the number of positive cumulative fibres, uniformly in the prime.

theorem EGZ.FlagDecomposition.card_liftedSupport_le_pow_dim {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} [Fact (Nat.Prime p)] (Φ : FlagDecomposition p d f) {K : Φ.flag.Node → ℕ} (hK : Φ.IsKBounded K) (x : Φ.flag.Node) : (Φ.liftedSupport x).card ≤ (2 * K x + 1) ^ d

theorem EGZ.FlagDecomposition.exists_gap_pruned_localWeight {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (threshold : Φ.flag.Node → ℝ) (hnonneg : ∀ (x : Φ.flag.Node), 0 ≤ threshold x) : ∃ (pieces : Φ.flag.Node → FpCoord p d → ℕ), (∀ (x : Φ.flag.Node) (v : FpCoord p d), pieces x v = 0 ∨ pieces x v = Φ.localWeight x v) ∧ (∀ (x : Φ.flag.Node) (v : FpCoord p d), pieces x v ≤ Φ.localWeight x v) ∧ (∀ (x : Φ.flag.Node) (q : IntCoord (Φ.flag.rank x)), FlagDecompositionRaw.hat Φ.representation pieces x q = 0 ∨ threshold x < ↑(FlagDecompositionRaw.hat Φ.representation pieces x q)) ∧ ↑Φ.retainedMass - ↑(natMass (FlagDecompositionRaw.retainedWeight pieces)) ≤ ∑ x : Φ.flag.Node, ↑(Φ.liftedSupport x).card * threshold x

Gap cleanup of all local atoms, before rebuilding the active polytopes. Its loss bound counts only the original lifted supports. The theorem applies to arbitrary node thresholds and preserves the original value of every surviving local atom.

theorem EGZ.FlagDecomposition.exists_bounded_gap_pruning {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} [Fact (Nat.Prime p)] (Φ : FlagDecomposition p d f) {K : Φ.flag.Node → ℕ} (hK : Φ.IsKBounded K) {α : ℝ} (hα : 0 ≤ α) : ∃ (pieces : Φ.flag.Node → FpCoord p d → ℕ), (∀ (x : Φ.flag.Node) (v : FpCoord p d), pieces x v = 0 ∨ pieces x v = Φ.localWeight x v) ∧ (∀ (x : Φ.flag.Node) (v : FpCoord p d), pieces x v ≤ Φ.localWeight x v) ∧ (∀ (x : Φ.flag.Node) (q : IntCoord (Φ.flag.rank x)), FlagDecompositionRaw.hat Φ.representation pieces x q ≠ 0 → α * ↑Φ.retainedMass / (↑(Fintype.card Φ.flag.Node) * (2 * ↑(K x) + 1) ^ d) < ↑(FlagDecompositionRaw.hat Φ.representation pieces x q)) ∧ (1 - α) * ↑Φ.retainedMass ≤ ↑(natMass (FlagDecompositionRaw.retainedWeight pieces))

The numerical conclusion of the gap cleanup lemma with the paper's uniform threshold. Rebuilding the reduced active flag is a separate geometric operation; this theorem supplies its local weights and complete loss estimate.