LeanPool.AsymptoticTrianglePacking.Internal — Module C4b-0' : round-matching membership via

conflicts (deterministic bridge)

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

Bridges the round's matching (roundMatching, module C1) with the conflict structure (module C4b-0): an edge is in the round's matching exactly when it is retained and none of its conflicting edges is retained. This is the deterministic identity that lets the survival probability p·(1-p)^{c(e)} (module C4b-1) be attached to actual matching membership.

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

theorem Hypergraph.mem_roundMatching_iff_conflicts {V : Type u_1} [DecidableEq V] {H R : Finset (Finset V)} (hRH : R ⊆ H) {e : Finset V} : e ∈ roundMatching R ↔ e ∈ R ∧ ∀ f ∈ conflicts H e, f ∉ R

C4b-0' — survival iff retained with no retained conflict. For a retained set R ⊆ H, an edge e is in the round's matching iff e ∈ R and none of its conflicting edges lies in R.

LeanPool.AsymptoticTrianglePacking.Internal — covered-whp : expected covered-vertex count per

round

Standalone, Mathlib-only. Turns the expected-matching-size bound (matching_expectation_lower, C4b-2) into a statement about the actual matching-size random variable, and links it to the covered set via |covered| = r · |matching| (the round matching is a matching of an r-uniform hypergraph).

• matchingIndicator / matchingSize — the round matching size as a sum of {0,1} indicators.
• matchingSize_expectation_lower — E[|matching|] ≥ |H| · p·(1-p)^{rΔ}.
• covered_card_eq — |covered R| = r · |roundMatching R|.

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

noncomputable def LeanPool.AsymptoticTrianglePacking.Internal.matchingIndicator {V : Type u_1} [DecidableEq V] {Ω : Type u_2} [MeasureTheory.MeasureSpace Ω] {H : Finset (Finset V)} {p : ℝ} (ρ : BernoulliRetention H p) (e : Finset V) (ω : Ω) : ℝ

Indicator that edge e is in the round's matching at outcome ω.

Equations

• LeanPool.AsymptoticTrianglePacking.Internal.matchingIndicator ρ e ω = if e ∈ Hypergraph.roundMatching (LeanPool.AsymptoticTrianglePacking.Internal.retainedSet H ρ ω) then 1 else 0

theorem LeanPool.AsymptoticTrianglePacking.Internal.covered_card_eq {V : Type u_1} [DecidableEq V] {H R : Finset (Finset V)} {r : ℕ} (hr : Hypergraph.IsUniform H r) (hRH : R ⊆ H) : (Hypergraph.covered R).card = r * (Hypergraph.roundMatching R).card

covered = r·matching. The covered set of a retained set R has r · |roundMatching R| vertices, since the round matching is a matching of the r-uniform hypergraph R... here stated for R ⊆ H with H r-uniform.

theorem LeanPool.AsymptoticTrianglePacking.Internal.matchingEvent_eq {V : Type u_1} [DecidableEq V] {Ω : Type u_2} [MeasureTheory.MeasureSpace Ω] {H : Finset (Finset V)} {p : ℝ} (ρ : BernoulliRetention H p) {e : Finset V} (he : e ∈ H) : {ω : Ω | e ∈ Hypergraph.roundMatching (retainedSet H ρ ω)} = ρ.A e ∩ ⋂ g ∈ Hypergraph.conflicts H e, (ρ.A g)ᶜ

The matching-membership event equals the survival event of Survival.

theorem LeanPool.AsymptoticTrianglePacking.Internal.measurableSet_matchingEvent {V : Type u_1} [DecidableEq V] {Ω : Type u_2} [MeasureTheory.MeasureSpace Ω] {H : Finset (Finset V)} {p : ℝ} (ρ : BernoulliRetention H p) {e : Finset V} (he : e ∈ H) : MeasurableSet {ω : Ω | e ∈ Hypergraph.roundMatching (retainedSet H ρ ω)}

The matching-membership event is measurable.

theorem LeanPool.AsymptoticTrianglePacking.Internal.integral_matchingIndicator {V : Type u_1} [DecidableEq V] {Ω : Type u_2} [MeasureTheory.MeasureSpace Ω] [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] {H : Finset (Finset V)} {p : ℝ} (ρ : BernoulliRetention H p) (hp0 : 0 ≤ p) (hp1 : p ≤ 1) {e : Finset V} (he : e ∈ H) : ∫ (ω : Ω), matchingIndicator ρ e ω = p * (1 - p) ^ (Hypergraph.conflicts H e).card

Integral of the matching indicator: ∫ 1[e matched] = p·(1-p)^{c(e)}.

theorem LeanPool.AsymptoticTrianglePacking.Internal.matchingIndicator_integrable {V : Type u_1} [DecidableEq V] {Ω : Type u_2} [MeasureTheory.MeasureSpace Ω] [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] {H : Finset (Finset V)} {p : ℝ} (ρ : BernoulliRetention H p) {e : Finset V} (he : e ∈ H) : MeasureTheory.Integrable (matchingIndicator ρ e) MeasureTheory.volume

The matching indicator is integrable (bounded and measurable).

theorem LeanPool.AsymptoticTrianglePacking.Internal.matchingSize_expectation_lower {V : Type u_1} [DecidableEq V] {Ω : Type u_2} [MeasureTheory.MeasureSpace Ω] [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] {H : Finset (Finset V)} {p : ℝ} {r Δ : ℕ} (ρ : BernoulliRetention H p) (hp0 : 0 ≤ p) (hp1 : p ≤ 1) (hr : Hypergraph.IsUniform H r) (hΔ : ∀ (x : V), Hypergraph.degree H x ≤ Δ) : ↑H.card * (p * (1 - p) ^ (r * Δ)) ≤ ∫ (ω : Ω), ↑(Hypergraph.roundMatching (retainedSet H ρ ω)).card

covered-whp — expected matching size lower bound. E[|roundMatching|] ≥ |H| · p·(1-p)^{rΔ}. Together with covered_card_eq this gives E[|covered|] ≥ r·|H|·p·(1-p)^{rΔ}: a definite fraction of vertices is covered per round.

theorem LeanPool.AsymptoticTrianglePacking.Internal.integrable_matchingSize {V : Type u_1} [DecidableEq V] {Ω : Type u_2} [MeasureTheory.MeasureSpace Ω] [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] {H : Finset (Finset V)} {p : ℝ} (ρ : BernoulliRetention H p) : MeasureTheory.Integrable (fun (ω : Ω) => ↑(Hypergraph.roundMatching (retainedSet H ρ ω)).card) MeasureTheory.volume

The matching-size random variable is integrable.

theorem LeanPool.AsymptoticTrianglePacking.Internal.exists_large_round_matching {V : Type u_1} [DecidableEq V] {Ω : Type u_2} [MeasureTheory.MeasureSpace Ω] [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] {H : Finset (Finset V)} {p : ℝ} {r Δ : ℕ} (ρ : BernoulliRetention H p) (hp0 : 0 ≤ p) (hp1 : p ≤ 1) (hr : Hypergraph.IsUniform H r) (hΔ : ∀ (x : V), Hypergraph.degree H x ≤ Δ) : ∃ (ω : Ω), ↑H.card * (p * (1 - p) ^ (r * Δ)) ≤ ↑(Hypergraph.roundMatching (retainedSet H ρ ω)).card

D3 (one-round existence) — probabilistic method. There is an outcome whose round matching has at least |H|·p·(1-p)^{rΔ} edges; hence a covered set of ≥ r·|H|·p·(1-p)^{rΔ} vertices. This is the single-round Rödl-nibble lower bound (the iterated (1-β) near-perfect version is the capstone T3).