LeanPool.AsymptoticTrianglePacking.Internal — Module D1 : iteration of nibble rounds

(deterministic scaffolding)

Standalone, Mathlib-only. Foundation for the Rödl-nibble project.

Given a per-round retention strategy R (a function assigning to the current hypergraph the set of retained edges), nibbleIter R H k runs k rounds starting from H, returning the pair (accumulated matching, current residual hypergraph). Each round adds the round's matching and passes to the residual (edges avoiding the covered vertices).

Deterministic invariants proved here (they hold for any strategy R):

• nibbleResidual_subset — the residual after k rounds is a sub-hypergraph of H.
• nibbleResidual_uniform — the residual stays r-uniform.

The probabilistic per-round shrinkage of the uncovered set (C4b-2 / C4) and the final assembly of the accumulated matching (D2 / D3) build on top of this scaffolding.

Definitions come from LeanPool.AsymptoticTrianglePacking.Internal.Basic / LeanPool.AsymptoticTrianglePacking.Internal.Round. Must be placeholder-free and axiom-clean [propext, Classical.choice, Quot.sound].

def Hypergraph.nibbleIter {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 under retention strategy R, returning (accumulated matching, current residual).

Equations

• Hypergraph.nibbleIter R H = Hypergraph.nibbleIterSeq (fun (x : ℕ) => R) H

theorem Hypergraph.nibbleIterSeq_const {V : Type u_1} [DecidableEq V] (R : Finset (Finset V) → Finset (Finset V)) (H : Finset (Finset V)) (k : ℕ) : nibbleIterSeq (fun (x : ℕ) => R) H k = nibbleIter R H k

The constant strategy sequence is the fixed-strategy iteration.

def Hypergraph.nibbleResidual {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.

Equations

• Hypergraph.nibbleResidual R H k = (Hypergraph.nibbleIter R H k).2

def Hypergraph.nibbleMatching {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.

Equations

• Hypergraph.nibbleMatching R H k = (Hypergraph.nibbleIter R H k).1

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

D1a — the residual is a sub-hypergraph of H.

theorem Hypergraph.nibbleResidual_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 (nibbleResidual R H k) r

D1b — the residual stays r-uniform.

LeanPool.AsymptoticTrianglePacking.Internal — D3 assembly : the accumulated matching is a matching

Standalone, Mathlib-only. The accumulated matching after k nibble rounds (nibbleMatching, D1) is a genuine matching of H. The key is a cross-round invariant: the residual hypergraph after k rounds is disjoint from the support of the accumulated matching (each round only matches edges that avoid all previously covered vertices). Hence the round matchings have pairwise-disjoint supports and their union is a matching — the assembly step of T3.

Definitions from LeanPool.AsymptoticTrianglePacking.Internal.Basic / LeanPool.AsymptoticTrianglePacking.Internal.Greedy / LeanPool.AsymptoticTrianglePacking.Internal.Round / LeanPool.AsymptoticTrianglePacking.Internal.Iteration. Must be placeholder-free and axiom-clean [propext, Classical.choice, Quot.sound].

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

D3a — accumulated matching stays inside H.

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

D3b — cross-round invariant. Every edge of the residual after k rounds is disjoint from the support of the accumulated matching.

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

D3 — the accumulated matching is a matching of H.