LeanPool.AsymptoticTrianglePacking.Internal — Module A4 : near-regularity and codegree-bounded

predicates

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

Content:

• NearlyRegular H d μ — every vertex degree lies in [(1-μ)d, (1+μ)d].
• CodegreeBounded H C — every pair has codegree ≤ C.
• sum_degree_bounds — the degree sum is squeezed into [(1-μ)d·|V|, (1+μ)d·|V|]. Combined with the handshake ∑ deg = r|H| (module A2) this pins |H| to (1±μ)·|V|·d/r, the estimate the nibble round consumes.

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

def Hypergraph.NearlyRegular {V : Type u_1} [DecidableEq V] (H : Finset (Finset V)) (d μ : ℝ) : Prop

H is (1 ± μ)-nearly d-regular: every degree lies in [(1-μ)d, (1+μ)d].

Equations

• Hypergraph.NearlyRegular H d μ = ∀ (v : V), (1 - μ) * d ≤ ↑(Hypergraph.degree H v) ∧ ↑(Hypergraph.degree H v) ≤ (1 + μ) * d

def Hypergraph.CodegreeBounded {V : Type u_1} [DecidableEq V] (H : Finset (Finset V)) (C : ℝ) : Prop

H has codegree bounded by C: every distinct pair lies in at most C edges.

Equations

• Hypergraph.CodegreeBounded H C = ∀ (x y : V), x ≠ y → ↑(Hypergraph.codegree H x y) ≤ C

theorem Hypergraph.sum_degree_bounds {V : Type u_1} [DecidableEq V] [Fintype V] {H : Finset (Finset V)} {d μ : ℝ} (hReg : NearlyRegular H d μ) : (1 - μ) * d * ↑(Fintype.card V) ≤ ∑ v : V, ↑(degree H v) ∧ ∑ v : V, ↑(degree H v) ≤ (1 + μ) * d * ↑(Fintype.card V)

A4 — degree-sum squeeze. If H is (1±μ)-nearly d-regular on a finite vertex type, then ∑_v degree v lies in [(1-μ)d·|V|, (1+μ)d·|V|].

Near-regular hypergraph nibble interface

The interface records the finite matching statement established by the nibble construction: near-regular, low-codegree uniform hypergraphs have near-perfect matchings.

Definitions come from LeanPool.AsymptoticTrianglePacking.Internal.Basic (IsUniform, IsMatching) and LeanPool.AsymptoticTrianglePacking.Internal.Regular (NearlyRegular, CodegreeBounded).

def LeanPool.AsymptoticTrianglePacking.Internal.NibbleTheorem : Prop

T3 interface — the nibble theorem. For r ≥ 2 and any target β > 0, there is a near-regularity/codegree tolerance μ > 0 such that every r-uniform hypergraph on a finite vertex set that is (1±μ)-nearly d-regular with codegree ≤ μd has a matching covering at least a (1-β) fraction of the maximum possible (|V|/r).

Equations

• One or more equations did not get rendered due to their size.

LeanPool.AsymptoticTrianglePacking.Internal — near-regularity for the majority of vertices, and

the adapted nibble interface

This file introduces the majority notion NearlyRegularMost H d μ η: regularity outside an exceptional set of at most an η-fraction of the vertices. It also records the matching interfaces that consume this hypothesis.

• NearlyRegularMost — near-d-regular outside an exceptional set of size ≤ η|V|.
• NearlyRegular.nearlyRegularMost — strict regularity is the η-majority notion with empty Exc.
• NibbleTheoremMost — the T3 interface consuming NearlyRegularMost.
• NibbleTheoremMost.nibbleTheorem — the majority interface is a strengthening: it implies the strict NibbleTheorem (so discharging it suffices for the whole Layer E chain).

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

def Hypergraph.NearlyRegularMost {V : Type u_1} [Fintype V] [DecidableEq V] (H : Finset (Finset V)) (d μ η : ℝ) : Prop

Majority near-regularity. H is (1±μ)-nearly d-regular outside an exceptional set of vertices of size at most η·|V|. Recovers NearlyRegular when the exceptional set is empty.

Equations

• Hypergraph.NearlyRegularMost H d μ η = ∃ (Exc : Finset V), ↑Exc.card ≤ η * ↑(Fintype.card V) ∧ ∀ v ∉ Exc, (1 - μ) * d ≤ ↑(Hypergraph.degree H v) ∧ ↑(Hypergraph.degree H v) ≤ (1 + μ) * d

theorem Hypergraph.NearlyRegular.nearlyRegularMost {V : Type u_1} [Fintype V] [DecidableEq V] {H : Finset (Finset V)} {d μ η : ℝ} (hη : 0 ≤ η) (h : NearlyRegular H d μ) : NearlyRegularMost H d μ η

Strict near-regularity is majority near-regularity with an empty exceptional set (any η ≥ 0).

def LeanPool.AsymptoticTrianglePacking.Internal.NibbleTheoremMost : Prop

T3 interface (majority form). For r ≥ 2 and target β > 0, there are tolerances μ, η > 0 such that every r-uniform hypergraph that is (1±μ)-nearly d-regular OUTSIDE an η-fraction exceptional set, with codegree ≤ μd, has a matching covering ≥ (1-β)·(|V|/r). The nibble absorbs the small exceptional set into the target slack β.

Equations

• One or more equations did not get rendered due to their size.

def LeanPool.AsymptoticTrianglePacking.Internal.NibbleTheoremMostCeil : Prop

T3 interface with global degree ceiling. This is the form consumed by the corrected Freedman assembly: in addition to majority near-regularity and codegree boundedness, every vertex has degree at most (1+μ)d.

Equations

• One or more equations did not get rendered due to their size.

def LeanPool.AsymptoticTrianglePacking.Internal.NibbleTheoremMostCeilSized : Prop

T3 interface with global ceiling and polynomial size control. The Freedman parameter selection needs a uniform way to make the all-vertices bad-event probability small. The abstract hypergraph hypotheses do not bound |V| in terms of the regular degree scale d; the triangle hypergraph application does. This interface records that missing input explicitly.

Equations

• One or more equations did not get rendered due to their size.

theorem LeanPool.AsymptoticTrianglePacking.Internal.NibbleTheoremMost.nibbleTheorem (h : NibbleTheoremMost) : NibbleTheorem

The majority interface implies the strict one. Since strict NearlyRegular is a special case of NearlyRegularMost (empty exceptional set), NibbleTheoremMost implies NibbleTheorem — so discharging the majority form suffices for the entire Layer E chain that consumes NibbleTheorem.