Inverse Counting Lemma #

This file proves the inverse counting lemma: if two graphons have similar homomorphism densities for all graphs, then they are close in cut distance.

Main results #

Graphon.cutDistance_zero_of_homDensity_eq - Equal hom densities ⟹ cutDistance = 0
Graphon.cutDistance_le_of_homDensity_close - The quantitative inverse counting lemma
Graphon.homDensity_mkStepGraphon_eq_weightedHomSum - Step-graphon hom densities are weighted homomorphism sums (public: specialized by Graphon/SamplingFinite.lean)

Implementation notes #

The counting lemma (in Counting.lean) shows: small cut distance ⟹ similar homomorphism densities

The inverse counting lemma shows the converse: similar homomorphism densities ⟹ small cut distance

Together, these establish that cut distance convergence is equivalent to convergence of all homomorphism densities.

The proof uses:

Algebraic determination for step graphons (MatrixDetermination.lean)
Partition alignment via the Rokhlin cell-alignment core (CutDistance.lean, proved)
Regularity lemma for step approximation
Compactness of graphon space

References #

[L. Lovász, Large Networks and Graph Limits][lovasz2012], Section 10.6

Step graphon inverse counting #

The algebraic core: step graphons on the same partition with equal hom densities for all graphs have cut distance zero. This connects the measure-theoretic homDensity to the finite weightedHomSum and uses matrix_quotient_of_weightedHomSum_eq (the algebraic determination theorem, proved) plus partition alignment (Rokhlin core, proved).

source

theorem Graphon.homDensity_mkStepGraphon_eq_weightedHomSum {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] [StandardBorelSpace α] [MeasureTheory.NullSingletonClass μ] (P : MeasurablePartition α μ) (c : Set α → Set α → ℝ) (hc_symm : ∀ S ∈ P.parts, ∀ T ∈ P.parts, c S T = c T S) (hc_mem : ∀ S ∈ P.parts, ∀ T ∈ P.parts, c S T ∈ Set.Icc 0 1) {k : ℕ} (ι : Fin k → Set α) (hι : ∀ (i : Fin k), ι i ∈ P.parts) (hι_surj : ∀ S ∈ P.parts, ∃ (i : Fin k), ι i = S) (hι_inj : Function.Injective ι) (n : ℕ) (F : SimpleGraph (Fin n)) [DecidableRel F.Adj] :

homDensity F (mkStepGraphon P c hc_symm hc_mem) = weightedHomSum n F (fun (i j : Fin k) => c (ι i) (ι j)) fun (i : Fin k) => (μ (ι i)).toReal

Bridge lemma: For a step graphon mkStepGraphon P c, the homomorphism density homDensity F (mkStepGraphon P c) equals the weighted homomorphism sum weightedHomSum n F c_fin w where:

ι : Fin k → Set α enumerates P.parts
c_fin i j = c (ι i) (ι j) is the coefficient matrix over Fin k
w i = (μ (ι i)).toReal is the cell-measure vector

The proof requires decomposing the pi-integral ∫ x, ∏ e, W(x_{e.1}, x_{e.2}) dμ^n over partition cell products. The integrand is constant on each product ∏ v, ι(σ(v)), and the integral over such a product equals ∏ v, w(σ(v)). Summing over all cell assignments σ : Fin n → Fin k gives weightedHomSum.

Proof: a non-trivial but fully proved integration identity involving Measure.pi and piecewise-constant functions: the pi integral decomposes over partition cell products, on each of which the integrand is constant. Public since the exact finite-sampling formula (Graphon/SamplingFinite.lean, Diaconis–Janson existence half) specializes it to the equipartition.

Main inverse counting lemma #

Headline assembly: equal densities ⟹ cut distance zero #

The assembly below wires simultaneous_regularity → counting bridge → step inverse counting → triangle inequality. Everything is proved except one named parameter-selection lemma (headline_parameter_selection), which isolates the genuine mathematical gap; see its docstring for the circularity analysis.

source

theorem Graphon.cutDistance_zero_of_homDensity_eq {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] [StandardBorelSpace α] [MeasureTheory.NullSingletonClass μ] (U W : Graphon α μ) (h : ∀ (k : ℕ) (F : SimpleGraph (Fin k)) [inst : DecidableRel F.Adj], homDensity F U = homDensity F W) :

U.cutDistance W = 0

Algebraic determination: two graphons with equal homomorphism densities for all finite graphs have cut distance zero (are weakly isomorphic).

FULLY ASSEMBLED (2026-07-06) modulo the single named parameter-selection lemma headline_parameter_selection. For any ε > 0: obtain (δ, δ_step, m) from the selection lemma; apply simultaneous_regularity U W δ to get a partition P within its cardinality bound with both stepifications δ-close in cut norm; the counting bridge stepify_homDensity_transfer converts the EXACT density equality of U, W into 2(m·m)δ < δ_step density closeness of the stepifications; the selection lemma's step ICL gives cutDistance(stepify P U, stepify P W) < ε/3; two triangle inequalities with cutDistance_le_cutNormDiff finish cutDistance U W < ε. Nonnegativity converts ∀ ε > 0, < ε into = 0.

Rests on: headline_parameter_selection (sampling route, proved) and MeasurePreserving.exists_controlled_cell_alignment (Rokhlin core, proved in R2) — fully axiom-clean.

source

theorem Graphon.cutDistance_le_of_homDensity_close {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] [StandardBorelSpace α] [MeasureTheory.NullSingletonClass μ] (ε : ℝ) (hε : ε > 0) :

∃ (δ : ℝ) (_ : δ > 0) (k : ℕ), ∀ (U W : Graphon α μ), (∀ (F : SimpleGraph (Fin k)) [inst : DecidableRel F.Adj], |homDensity F U - homDensity F W| < δ) → U.cutDistance W < ε

The inverse counting lemma: similar homomorphism densities imply small cut distance.

For any ε > 0, there exists δ > 0 and a finite set of graphs F₁,...,Fₖ such that if |t(Fᵢ, U) - t(Fᵢ, W)| < δ for all i, then δ□(U, W) < ε.

source

theorem Graphon.cutDistance_tendsto_iff_homDensity_tendsto {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] [StandardBorelSpace α] [MeasureTheory.NullSingletonClass μ] (W : ℕ → Graphon α μ) (V : Graphon α μ) :

(∀ ε > 0, ∃ (N : ℕ), ∀ n ≥ N, (W n).cutDistance V < ε) ↔ ∀ (k : ℕ) (F : SimpleGraph (Fin k)) [inst : DecidableRel F.Adj], ∀ ε > 0, ∃ (N : ℕ), ∀ n ≥ N, |homDensity F (W n) - homDensity F V| < ε

Corollary: a sequence converges in cut distance iff all homomorphism densities converge.

This is the fundamental characterization of graph limit convergence.