1 Graphons

This project formalizes the theory of graphons — limits of dense graph sequences — in Lean 4 using Mathlib, following Lovász  [ Lov12 ] .

A graphon is a symmetric measurable function \(W : [0,1]^2 \to [0,1]\) (more generally, on an arbitrary probability space). Graphons arise as the natural limit objects for convergent sequences of dense graphs.

1.1 Proof Status

The advertised program is fully proved (2026-07-10): no live sorry remains, and every headline theorem verifies with the standard axioms only (propext, Classical.choice, Quot.sound). The three items formerly tracked here were each resolved:

1. Rokhlin / measure-isomorphism input: the original exists_common_extension stub was shown unprovable as stated and replaced by four corrected cores, all proved from the atomless standard-Borel measure-isomorphism theorem, built from scratch in Graphon/MeasureIso.lean (mod-0 isomorphism with \(([0,1],\lambda )\) plus a mod-0-to-everywhere upgrade); the final overlay core is proved in Graphon/Overlay.lean. Used by: cut distance triangle inequality, partition alignment, compactness.

2. Algebraic determination for \(k \ge 2\) (matrix_quotient_of_weightedHomSum_eq): proved 2026-07-06 via the twin-free bijection and the cross-matrix super transfer (Graphon/CrossSuper.lean).

3. Determination theorem (cutDistance_zero_of_homDensity_eq): proved, via the First Sampling Lemma (proved 2026-07-08, Graphon/SamplingLemma.lean) and the \(K\)-independent quantitative inverse counting lemma.

The repository contains zero sorry/admit proof placeholders (enforced by the CI census with an empty allowlist since issue #19 closed); the formerly-retained refuted-conjecture stubs were deleted, with their refutation documentation kept as prose.

1.2 Main Results

The formalization establishes:

• Cut distance pseudometric. Cut distance is a pseudometric: non-negativity, symmetry (Proposition 7), and the triangle inequality (Theorem 8).

• Frieze–Kannan weak regularity lemma. Every graphon admits a step approximation of bounded complexity (Theorem 20), following Frieze–Kannan  [ FK99 ] and Lovász  [ Lov12 , Corollary 9.13 ] .

• Counting lemma. Small cut distance implies similar homomorphism densities (Theorem 22).

• Compactness. The cut-distance quotient modulo weak isomorphism is a compact metric space; concretely, the graphon pseudometric space is totally bounded (Theorem 23) and complete (Theorem 24).

• Inverse counting lemma. For any \(\varepsilon {\gt} 0\), finitely many test graphs control cut distance up to \(\varepsilon \) (Theorem 27), following Lovász  [ Lov12 , Lemma 10.32 ] .

• Convergence equivalence. Cut distance convergence is equivalent to convergence of all homomorphism densities (Theorem 61).

1.3 Graphon Definition

A graphon on a probability space \((\alpha , \mu )\) is a symmetric measurable function taking values in \([0,1]\) a.e., following Lovász  [ Lov12 , Definition 7.1 ] .

2 Cut Distance

The cut distance is the fundamental pseudometric on graphon space, measuring how close two graphons are after optimal rearrangement of the underlying probability space. The development follows Lovász  [ Lov12 , Chapter 8 ] and Borgs–Chayes–Lovász–Sós–Vesztergombi  [ BCL\(^{+}\)08 ] .

2.1 Cut Norm

The cut norm of the difference of two graphons, defined as the supremum of \(|\int _{S \times T} (U - W)|\) over measurable sets \(S, T\).

2.2 Pullback

The pullback of a graphon under a measure-preserving map, fundamental to the definition of cut distance. Following Lovász  [ Lov12 , Section 8.2 ] .

2.3 Cut Distance Definition

The cut distance between two graphons, defined as the infimum of \(\| U^\varphi - W^\psi \| _\square \) over measure-preserving maps \(\varphi , \psi \). This two-sided formulation avoids the need for invertibility (Lovász  [ Lov12 , Section 8.2 ] ).

2.4 Metric Properties

Cut distance is a pseudometric on graphon space (Lovász  [ Lov12 , Theorem 8.13, Corollary 8.14 ] ).

The triangle inequality couples the measure-preserving witnesses via the (fully proved) Rokhlin cores exists_common_coupling_maps and cutNormDiff_pullback_le, both consequences of the atomless standard-Borel measure-isomorphism theorem (Graphon/MeasureIso.lean). Status: fully proved, standard axioms only.

Pullback by a measure-preserving bijection preserves cut distance (Lovász  [ Lov12 , Section 8.2 ] ).

2.5 The Measure-Isomorphism Theorem and the Rokhlin Cores

The measure-theoretic engine behind the pseudometric and compactness theory is the classical fact that every atomless standard Borel probability space is measure-preservingly isomorphic mod 0 to \(([0,1],\lambda )\), built from scratch in Graphon/MeasureIso.lean via the probability integral transform and a quantile inverse.

A mod-0 isomorphism upgrades to an everywhere-defined measure-preserving measurable equivalence by patching the defect sets through uncountable Borel null reservoirs (a compact Cantor scheme provides the reservoirs).

Four consumer-shaped corollaries — the Rokhlin cores — carry all of the graphon program’s alignment needs. Any two measure-preserving maps admit a common coupling by measure-preserving maps:

Pullback along a single measure-preserving map contracts the cut norm:

Equal-measure measurable cell families can be aligned by a measure-preserving bijection (almost everywhere):

Finally, the overlay theorem: on an atomless space the cut distance — an infimum over pairs of maps — is achieved up to any \(\varepsilon \) by a single measure-preserving bijection, leaving the second graphon bare. The proof realizes the coupling matrix of two step approximations exactly, by prescribed-mass carving and two controlled cell alignments.

3 Partitions and Step Graphons

Step graphons — graphons that are constant on rectangles of a partition — are the finite-dimensional building blocks of graphon theory.

3.1 Measurable Partitions

A finite partition of the probability space into measurable sets that cover almost everywhere.

3.2 Stepification

The stepification \(W_P\) of a graphon \(W\) with respect to a partition \(P\) replaces \(W\) on each rectangle \(S \times T\) by its average (Lovász  [ Lov12 , Section 9.2 ] ).

3.3 Step Graphons from Coefficients

A step graphon built from explicit coefficients on a partition.

4 Regularity

The Frieze–Kannan weak regularity lemma for graphons: every graphon can be approximated by a step graphon of bounded complexity. Following Frieze–Kannan  [ FK99 ] and Lovász  [ Lov12 , Corollary 9.13 ] .

4.1 Energy Increment

The energy increment lemma: if a partition \(P\) does not approximate \(W\) well, then a refinement \(Q\) has strictly higher energy (Lovász  [ Lov12 , Lemma 9.11 ] ).

4.2 Regularity Lemma

The regularity lemma: for any \(\varepsilon {\gt} 0\), every graphon admits a partition \(P\) with at most \(\mathrm{regularityBound}(\varepsilon )\) parts such that \(\| W - W_P\| _\square \le \varepsilon \).

5 Homomorphism Densities and the Counting Lemma

Homomorphism densities encode the local structure of a graphon. The counting lemma shows that small cut distance implies similar homomorphism densities. Following Lovász  [ Lov12 , Chapter 5 and Section 10.1 ] .

5.1 Homomorphism Density

For a finite graph \(F\) and a graphon \(W\), the homomorphism density \(t(F, W) = \int \prod _{uv \in E(F)} W(x_u, x_v) \, d\mu ^{V(F)}\) (Lovász  [ Lov12 , Equation (5.29) ] ).

5.2 Counting Lemma

The counting lemma: \(|t(F, U) - t(F, W)| \le |E(F)| \cdot \| U - W\| _\square \) (Lovász  [ Lov12 , Lemma 10.23 ] ).

6 Compactness

The cut-distance quotient modulo weak isomorphism is a compact metric space (Lovász  [ Lov12 , Theorem 9.23 ] ). Concretely, we prove total boundedness (via the regularity lemma and grid quantization) and completeness (via a direct limit construction from rapidly converging subsequences) of the graphon pseudometric space.

6.1 Total Boundedness

For any \(\varepsilon {\gt} 0\), there exists a finite \(\varepsilon \)-net in cut distance. The construction uses the regularity lemma to approximate any graphon by a step graphon, then quantizes coefficients to a grid (Lovász  [ Lov12 , Section 9.3 ] ).

6.2 Completeness

Every Cauchy sequence in cut distance has a limit graphon. The proof extracts a rapidly converging subsequence, builds the limit graphon via Radon–Nikodym, and shows the full sequence converges (Lovász  [ Lov12 , Section 9.3 ] ).

6.3 The Graphon Space

The proved pseudometric theory packages into a bundled state space: the metric separation quotient of graphons under cut distance — equivalently, graphons modulo weak isomorphism — is a compact Polish standard-Borel metric space, the natural home for graphon-valued random elements.

7 Inverse Counting Lemma and Convergence

The inverse counting lemma is the converse of the counting lemma: if all homomorphism densities are similar, then the graphons are close in cut distance. Together with the counting lemma, this gives the fundamental convergence equivalence (Lovász  [ Lov12 , Section 10.6 and Theorem 11.5 ] ).

7.1 Inverse Counting Lemma

For any \(\varepsilon {\gt} 0\), there exist \(\delta {\gt} 0\) and a finite family of test graphs such that \(\delta \)-close homomorphism densities imply \(\varepsilon \)-close cut distance (Lovász  [ Lov12 , Lemma 10.32 ] ). Status: fully proved — partition alignment via the proved Rokhlin cell-alignment core, the step-graphon core via the proved algebraic determination theorem, and the parameter selection via the proved First Sampling Lemma.

7.2 The First Sampling Lemma and Determination

The parameter selection behind the quantitative inverse counting lemma is supplied by the First Sampling Lemma (Lovász  [ Lov12 , Lemma 10.16 ] ): one sample size works for every graphon on the space simultaneously.

Together these give the determination theorem: equal homomorphism densities for all finite simple graphs force cut distance zero.

The finite sample laws carry the same information: two graphons have equal sample laws at every size exactly when they are weakly isomorphic.

The sample laws package into continuous point-separating coordinates on the graphon space, embedding it as a compact closed subset of the product of finite graph-law simplices.

7.3 The Finite Density Triangle

For finite graphs, the three classical labeled subgraph densities — the homomorphism density \(t\), normalized by all \(n^k\) vertex maps, and the injective and induced densities \(t_{\mathrm{inj}}\), \(t_{\mathrm{ind}}\), normalized by the \(n^{\underline{k}}\) injective maps — are related by the zeta and Möbius identities (Lovász  [ Lov12 , § 5.2.3, (5.19)–(5.20) ] ) and the collision (birthday) comparison \(|t - t_{\mathrm{inj}}| \le k^2/n\) — a coarser corollary of Lovász (5.21), whose stated bound is \(\binom {k}{2}/n\); the formalized ordered-pair union bound gives \(k^2\). All three statements are unconditional: for hosts smaller than the pattern both injective densities vanish by convention. On the equipartition step graphon of a host the analytic homomorphism density is exactly \(t\) and the sampling mass exactly the normalized pullback count, so the comparison transfers to the sampling formulas.

7.4 The Graphon-Mixture Representation

Exchangeable graph laws — families of finite graph laws consistent under every injection of labels — are exactly the mixtures of graphon sample laws (Diaconis–Janson  [ DJ08 , Theorem 5.3 ] ). Mixing over a probability measure on the graphon space is injective: the hom-density coordinates span a point-separating subalgebra of the bounded continuous functions, so the mixing measure is determined by its integrals against them, which are marginal quantities.

Conversely, every exchangeable law arises: the empirical mixing measures (the law of the graphon class of an \(n\)-vertex sample) admit a Prokhorov subsequential limit by compactness, and a quantitative collision estimate — injective vertex maps contribute exact marginal masses by consistency, non-injective ones at most a \(k^2/n\) proportion — identifies the limit’s marginals.

Together:

In fact the empirical mixing measures converge along the whole sequence: subsequential limits are unique by the representation theorem, and a unique cluster point in the compact metrizable space of mixing measures forces weak convergence to the representing measure.

The extreme points of the correspondence are characterized by dissociation (Diaconis–Janson  [ DJ08 , Theorem 5.5 ] ): upper events on disjoint vertex blocks are independent exactly when the mixing measure is a Dirac — equivalently, when the law samples a single fixed graphon.

7.5 The Infinite Exchangeable Graph Law

The consistent finite marginals extend uniquely to a probability law on simple graphs with vertex set \(\mathbb {N}\): the space of such graphs is a compact metrizable zero-dimensional Polish space (an arbitrary Boolean assignment on off-diagonal pairs), so a Prokhorov subsequential limit of padded finite laws provides the extension, and finite-restriction measure extensionality gives uniqueness — a specialized Kolmogorov extension with no general projective-limit machinery.

The infinite law is invariant under every relabeling of \(\mathbb {N}\) (finite images lie in initial segments, where injection consistency applies), and conversely the finite restrictions of any relabeling-invariant law are consistent, giving the equivalence of the finite and infinite formulations — layers 1–2 of the Aldous–Hoover realization.

Composed with the graphon-mixture representation, this gives the infinite form of the correspondence: every exchangeable probability law on infinite graphs is represented by a unique probability measure on graphon space — the distributional form of Aldous–Hoover.

The canonical infinite law of a graphon class embeds the compact graphon space homeomorphically onto a closed set of probability laws on infinite graphs — the infinite analogue of the finite coordinate embedding.

The canonical infinite law of a fixed graphon is realized by an explicit sampler: independent uniform vertex positions and one independent uniform per unordered edge, compared against the graphon value — the classical \(W\)-random infinite graph.

The abstract equivalence has a genuine probabilistic meaning: the represented infinite law of a mixing measure is the barycenter of the canonical fiber laws, as a kernel/bind mixture.

The explicit sampler’s empirical graphons converge to the class of the sampled graphon in probability (the almost-sure strengthening — the manuscript’s Proposition 11.32 — awaits the quantitative sampling layer).

For a fixed simple graph \(F\) on \(q\) vertices, the homomorphism density of the sampled graph concentrates exponentially around \(t(F,W)\): an eventual fixed-\(F\) Corollary-10.4-style tail \(2\exp (-\varepsilon ^2 k/(2q^2))\), valid once \(2q^2 \le \varepsilon k\). This is the summable fixed-\(F\) ingredient that Borel–Cantelli upgrades to almost-sure convergence.

In fact the convergence is almost sure (the manuscript’s Proposition 11.32): the exponential hom-density concentration of the sample makes every coordinate converge almost surely by Borel–Cantelli, and the convergence equivalence upgrades the countable intersection to cut-distance convergence pathwise.

For a general exchangeable law, the empirical graphons converge almost surely to a universal measurable limit random variable, whose law is exactly the representing measure — the pathwise face of the correspondence.

In the dissociated/extreme case (classically equivalent to ergodic; the formal equivalence is future work) the functional Aldous–Hoover representation needs no measurable selection: extremality fixes a single graphon class, one raw representative realizes it through the explicit sampler, and conversely every such law is dissociated.

The empirical limit is unchanged by deleting finitely many initial vertices, so it is measurable with respect to the vertex-tail \(\sigma \)-algebra — the key input for the tail formulations of the extremality theorem.

Consequently a law whose vertex-tail \(\sigma \)-algebra is trivial has a Dirac representing measure, hence is dissociated — and restriction independence (the initial restriction independent of the tail) implies vertex-tail triviality, giving two arcs of the Diaconis–Janson five-way extremality theorem.

Conversely, a dissociated law is restriction independent: the two-block joint mass factors by a two-variable Möbius inversion of the upper-mass dissociation criterion, and finite tail windows exhaust the tail. All five formulations are therefore equivalent — the Diaconis–Janson five-way extremality theorem.

Adjoining the finite-permutation action gives the ergodic-decomposition form: a law is ergodic under the finitely supported relabelings of \(\mathbb {N}\) (every permutation-invariant event has measure \(0\) or \(1\)) exactly when it is extreme. Restriction independence forces ergodicity by an approximate-independence estimate — approximate an invariant event by an initial cylinder, push it onto a disjoint tail block, and compare — while ergodicity forces vertex-tail triviality because every vertex-tail event is invariant. The empirical limit \(\mathrm{limitGraphon}\) thus generates the invariant \(\sigma \)-algebra modulo null sets.

Because every permutation-invariant event is null or conull in each sampled fiber and the empirical limit converges almost surely there, an invariant event coincides, modulo a null set, with a preimage under \(\mathrm{limitGraphon}\) of a Borel classifier on graphon space — so \(\mathrm{limitGraphon}\) generates the invariant \(\sigma \)-algebra up to null sets.

7.6 The Generic Relational and Directed Exchangeable-Law Equivalences

The finite/infinite exchangeable-law correspondence is not special to simple graphs. For an arbitrary multi-sorted relational signature with finitely many sorts and countably many relation symbols, the structure space is again a compact zero-dimensional Polish space (an arbitrary Boolean assignment on relational coordinates), so the same Prokhorov extension and finite-restriction extensionality identify the size-vector-indexed families of consistent probability marginals with the probability laws on the infinite structure space invariant under every sortwise relabeling of \(\mathbb {N}\) — the generic Aldous–Hoover–Kallenberg finite-marginal \(\leftrightarrow \) infinite-law layer.

Directed graphs are the one-sort, single-binary-relation, ordered-argument, diagonal-permitted case. Because the signature is finite, a finite directed law over \(\mathrm{Fin}\, k\) is a genuine probability mass function on \(\mathrm{Digraph}(\mathrm{Fin}\, k)\), and the carrier equivalence with the relational structure (which carries all the measurable structure — Mathlib’s \(\mathrm{Digraph}\) gets none) commutes with \(\mathrm{comap}\)/restriction. Transporting the \(\mathrm{PMF}\) marginals across it and composing with the generic equivalence yields the directed finite/infinite exchangeable-law equivalence. (This is the projective-law equivalence; the directed representation theorem, a mixture over digraphons, comes later.)

7.7 The Relational Extremality Equivalence

For an exchangeable law on the infinite structure space of a finite-sort relational signature, five characterizations of extremality coincide: exact finite-event block factorization (dissociation), independence of every initial block from its complementary tail, triviality of the vertex-tail \(\sigma \)-algebra, ergodicity under the finitely supported sortwise relabelings, and genuine extreme-point membership in the simplex of invariant probability laws. The proof is representation-free: the tail arrow is closed by an \(L^1\) Lévy downward theorem (conditional expectations along a decreasing filtration), and the ergodic–extreme equivalence is the classical invariant-simplex characterization ported to the relabeling group. The Dirac-mixing description of the extreme laws is a later corollary of the representation layer.

7.8 Digraphons and Directed Sampling

The measure-theoretic limit object for directed graphs (Cai–Ackerman–Freer  [ CAF16 , § 2.3–2.4 ] ) is not a single asymmetric kernel: reciprocal edges may be dependent, so a digraphon assigns to each ordered pair of latent positions a probability vector over the four reciprocal-edge states, with a transpose symmetry, plus a loop coordinate. Sampling draws i.i.d. latent positions, one uniform per unordered pair, and reads both directed edges off a single categorical draw; the exact finite-event probability is a product of one loop indicator per vertex and one simplex mass per unordered pair, stated over an arbitrary injective labeling so that consistency and exchangeability are immediate. The sampler realizes, on the infinite digraph space, exactly the infinite exchangeable law of its finite marginals, and the sampled law is dissociated.

The classical special families are digraphons: an ordinary graphon embeds with its reciprocal edges fully correlated, and its digraph sample is the undirected \(W\)-random graph ( [ CAF16 , § 3.2.1 ] ); a tournament kernel with \(A(x,y)+A(y,x)=1\) samples an almost-sure tournament ( [ CAF16 , § 3.2.2 ] ); and an asymmetric kernel draws the two directions of each pair independently ( [ CAF16 , § 3.1 ] ).

7.9 Convergence Equivalence

A sequence of graphons converges in cut distance if and only if all homomorphism densities converge (Lovász  [ Lov12 , Theorem 11.5 ] ).