LeanPool.AsymptoticTrianglePacking.Internal — round-dependent iteration of nibble rounds

Standalone, Mathlib-only. LeanPool.AsymptoticTrianglePacking.Internal.Iteration iterates ONE fixed retention strategy R. The obstruction LeanPool.AsymptoticTrianglePacking.Internal.total_gain_le shows that a fixed strategy — in particular a fixed retention probability p — can never cover more than a (1-μ)d/(rΔ) ≤ 1/r fraction of the vertex set, no matter how many rounds are run: with p fixed, the residual degree decays like (1-rΔp)^k and so does the per-round covering fraction, whose total is a convergent geometric series.

The nibble therefore has to re-tune its retention probability from round to round (p_k ≈ x / (r·d_k), tracking the shrinking residual degree d_k). This file provides the corresponding deterministic scaffolding: iteration along a sequence R : ℕ → strategy of retention strategies. Its round-to-round invariants are the common core specialized by LeanPool.AsymptoticTrianglePacking.Internal.Iteration and LeanPool.AsymptoticTrianglePacking.Internal.Assemble.

• nibbleIterSeq, nibbleResidualSeq, nibbleMatchingSeq — the sequence-indexed iteration.
• nibbleResidualSeq_subset, nibbleResidualSeq_uniform — residual invariants.
• nibbleResidualSeq_disjoint_support, nibbleMatchingSeq_isMatching — the assembly invariants. The fixed-strategy iteration is recovered by specializing this sequence in LeanPool.AsymptoticTrianglePacking.Internal.Iteration.

Must be placeholder-free and axiom-clean [propext, Classical.choice, Quot.sound].

def Hypergraph.nibbleIterSeq {V : Type u_1} [DecidableEq V] (R : ℕ → Finset (Finset V) → Finset (Finset V)) (H : Finset (Finset V)) : ℕ → Finset (Finset V) × Finset (Finset V)

Run k nibble rounds from H, using the strategy R i in round i; returns (accumulated matching, current residual).

Equations

• One or more equations did not get rendered due to their size.
• Hypergraph.nibbleIterSeq R H 0 = (∅, H)

def Hypergraph.nibbleResidualSeq {V : Type u_1} [DecidableEq V] (R : ℕ → Finset (Finset V) → Finset (Finset V)) (H : Finset (Finset V)) (k : ℕ) : Finset (Finset V)

The residual hypergraph after k rounds of a strategy sequence.

Equations

• Hypergraph.nibbleResidualSeq R H k = (Hypergraph.nibbleIterSeq R H k).2

def Hypergraph.nibbleMatchingSeq {V : Type u_1} [DecidableEq V] (R : ℕ → Finset (Finset V) → Finset (Finset V)) (H : Finset (Finset V)) (k : ℕ) : Finset (Finset V)

The matching accumulated over k rounds of a strategy sequence.

Equations

• Hypergraph.nibbleMatchingSeq R H k = (Hypergraph.nibbleIterSeq R H k).1

theorem Hypergraph.nibbleResidualSeq_subset {V : Type u_1} [DecidableEq V] (R : ℕ → Finset (Finset V) → Finset (Finset V)) (H : Finset (Finset V)) (k : ℕ) : nibbleResidualSeq R H k ⊆ H

The residual after k rounds is a sub-hypergraph of H.

theorem Hypergraph.nibbleResidualSeq_uniform {V : Type u_1} [DecidableEq V] {H : Finset (Finset V)} {r : ℕ} (hr : IsUniform H r) (R : ℕ → Finset (Finset V) → Finset (Finset V)) (k : ℕ) : IsUniform (nibbleResidualSeq R H k) r

The residual stays r-uniform.

theorem Hypergraph.nibbleMatchingSeq_subset {V : Type u_1} [DecidableEq V] {R : ℕ → Finset (Finset V) → Finset (Finset V)} (hR : ∀ (k : ℕ) (H' : Finset (Finset V)), R k H' ⊆ H') (H : Finset (Finset V)) (k : ℕ) : nibbleMatchingSeq R H k ⊆ H

The accumulated matching stays inside H.

theorem Hypergraph.nibbleResidualSeq_disjoint_support {V : Type u_1} [DecidableEq V] {R : ℕ → Finset (Finset V) → Finset (Finset V)} (H : Finset (Finset V)) (k : ℕ) (e : Finset V) : e ∈ nibbleResidualSeq R H k → Disjoint e (support (nibbleMatchingSeq R H k))

Cross-round invariant: every edge of the residual after k rounds avoids everything covered so far.

theorem Hypergraph.nibbleMatchingSeq_isMatching {V : Type u_1} [DecidableEq V] {R : ℕ → Finset (Finset V) → Finset (Finset V)} (hR : ∀ (k : ℕ) (H' : Finset (Finset V)), R k H' ⊆ H') (H : Finset (Finset V)) (k : ℕ) : IsMatching H (nibbleMatchingSeq R H k)

The accumulated matching is a matching of H.

theorem Hypergraph.nibbleMatchingSeq_support_card_succ {V : Type u_1} [DecidableEq V] {R : ℕ → Finset (Finset V) → Finset (Finset V)} (hR : ∀ (k : ℕ) (H' : Finset (Finset V)), R k H' ⊆ H') (H : Finset (Finset V)) (k : ℕ) : (support (nibbleMatchingSeq R H (k + 1))).card = (support (nibbleMatchingSeq R H k)).card + (support (roundMatching (R k (nibbleResidualSeq R H k)))).card

New vertices covered in round k add exactly to the accumulated covered count.