LeanPool.AsymptoticTrianglePacking.Internal — Module C1 : one nibble round (deterministic

scaffolding)

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

A nibble round takes a set R of "retained" edges (in the probabilistic argument R is a random subset of H, but every structural fact here is deterministic and holds for any R):

• roundMatching R — the retained edges that are isolated, i.e. disjoint from every other retained edge. These form a genuine matching.
• covered R — the vertices used by that matching.
• residual H R — the edges of H that avoid the covered vertices; the hypergraph the next round works on.

Results:

• roundMatching_isMatching — roundMatching R is a matching of the ambient H (when R ⊆ H).
• residual_subset, residual_uniform — the residual hypergraph is a sub-hypergraph of H and stays r-uniform.
• residual_disjoint_covered — every residual edge avoids the covered set (well-formedness of the iteration invariant).

The probabilistic content (expected sizes, concentration) is Layer C2/C3 and consumes Layer B. Definitions (degree, IsUniform, IsMatching, support) come from LeanPool.AsymptoticTrianglePacking.Internal.Basic / LeanPool.AsymptoticTrianglePacking.Internal.Greedy. Must be placeholder-free and axiom-clean [propext, Classical.choice, Quot.sound].

def Hypergraph.roundMatching {V : Type u_1} [DecidableEq V] (R : Finset (Finset V)) : Finset (Finset V)

The matching induced by a retained set R: the retained edges that are disjoint from every other retained edge.

Equations

• Hypergraph.roundMatching R = {e ∈ R | ∀ f ∈ R, f ≠ e → Disjoint e f}

def Hypergraph.covered {V : Type u_1} [DecidableEq V] (R : Finset (Finset V)) : Finset V

The vertices covered by the round's matching.

Equations

• Hypergraph.covered R = Hypergraph.support (Hypergraph.roundMatching R)

def Hypergraph.residual {V : Type u_1} [DecidableEq V] (H R : Finset (Finset V)) : Finset (Finset V)

The residual hypergraph: edges of H that avoid the covered vertices.

Equations

• Hypergraph.residual H R = {e ∈ H | Disjoint e (Hypergraph.covered R)}

@[simp]

theorem Hypergraph.roundMatching_subset {V : Type u_1} [DecidableEq V] (R : Finset (Finset V)) : roundMatching R ⊆ R

theorem Hypergraph.roundMatching_isMatching {V : Type u_1} [DecidableEq V] {H R : Finset (Finset V)} (hRH : R ⊆ H) : IsMatching H (roundMatching R)

C1a — the round's matching is a matching. For R ⊆ H, roundMatching R is a matching of H.

@[simp]

theorem Hypergraph.residual_subset {V : Type u_1} [DecidableEq V] (H R : Finset (Finset V)) : residual H R ⊆ H

theorem Hypergraph.residual_uniform {V : Type u_1} [DecidableEq V] {H : Finset (Finset V)} {r : ℕ} (hr : IsUniform H r) (R : Finset (Finset V)) : IsUniform (residual H R) r

C1b — residual stays r-uniform.

theorem Hypergraph.residual_disjoint_covered {V : Type u_1} [DecidableEq V] {H R : Finset (Finset V)} {e : Finset V} (he : e ∈ residual H R) : Disjoint e (covered R)

C1c — residual edges avoid the covered vertices.