Add roadmap: Dense graph limits and graphons (Lovász LNGL Part 3)

[cameronfreer]

Summary

Adds a roadmap for a Tau Ceti library entry on dense graph limits and graphons, after Part 3 of Lovász, Large Networks and Graph Limits (LNGL). The spine is Graphon → homDensity → cutNorm → cutDist → GraphonSpace → counting → regularity → compactness → separation → convergence, culminating in the equivalence of cut-distance convergence with convergence of all homomorphism densities. It connects graphons and cut distance to Mathlib's existing finite-graph ecosystem (Szemerédi regularity, partition / equitabilise infrastructure, triangle counting/removal, Turán, the binomial random graph G(V,p), measurable simple graphs) rather than rebuilding it.

Two prior Lean formalizations are pinned migration sources (API warnings and proof routes, not the mathematical specification): math-commons/graphons (strict-function carrier, coupling cutDist, sorry-free modulo four audited classical axioms) and cameronfreer/graphon (AEEqFun carrier, measure-preserving-map cutDist, no custom axioms with concentrated sorrys). The roadmap is the intended sorry-free / axiom-free synthesis both can upstream into.

The roadmap follows the existing TauCetiRoadmap format:

• narrative README.md (conventions, layer plan, consumed-Mathlib inventory, acceptance gates, provenance, references)
• Suggested.lean with compiled sorry-signatures
• root README.md index entry
• root TauCetiRoadmap.lean import

Suggested.lean pins the prototype types as sorry-signatures that build green against the pinned Mathlib (lake build, verified locally; sorry is allowed in this human-owned roadmap library). Several structural predicates (IsCoupling; the Layer-8 IsIsoInvariant / IsMultiplicative / IsNormalized / IsReflectionPositive) are defined outright; theorem-scale endpoints remain sorry-targets. It fixes the load-bearing choices so contributors don't oscillate. The cut norm acts on kernels (so a difference U − W is well-typed), with a concrete set form cutNormSet and a signed-form factor sandwich. cutDist is coupling-primary and cross-carrier, with its triangle inequality — hence the GraphonSpace metric quotient — on arbitrary probability carriers (Janson, Graphons, cut norm and distance, Lemma 6.5). The constant-graphon and sampling targets share the unitInterval convention with SimpleGraph.binomialRandom. The Layer-6a separation is carrier-free in both directions (Janson, Thm 8.10) — the forward via the coupling counting lemma, the hard converse pinned cross-carrier with no standard-Borel / atomless hypotheses and the same-carrier forms as specializations — over SimpleGraph (Fin n). Layer 2 is block-average based: Frieze–Kannan weak regularity consumes equitabilise / Finpartition infrastructure and builds the analytic graphon energy ‖E[W|P⊗P]‖² as the L² norm of the block-average step graphon (Mathlib's finite Finpartition.energy is a proof template, not an input), with Szemerédi's strong lemma a related comparison point. And the injective sampling density t₀ is normalized by the falling factorial (n)_k (Nat.descFactorial), never Nat.choose.

Roadmap shape

The roadmap organizes the development into ten layers (0–9):

0. finite-graph and measure scaffolding
1. core objects and basic API — the symmetric-kernel ℝ-module, Graphon, homDensity, cutNorm (with the set form and the signed/factor-sandwich forms), the coupling-primary cross-carrier cutDist with its arbitrary-carrier triangle inequality (Janson, Lemma 6.5), and the GraphonSpace quotient — a genuine metric quotient over any probability carrier, no standard-Borel hypothesis (with GraphonSpaceI and a MetricSpace instance whose distance computes as cutDist)
2. counting (with the coupling-form counting_lemma_coupling and the homDensityOnSpace descent), Frieze–Kannan weak regularity (weak_regularity_frieze_kannan) built on the block-average stepGraphonAvg and its energy Pythagoras, and total boundedness
3. the AE / AEEqFun view, with the named invariance lemmas and the L⁰→strict representative bridge
4. completeness and compactness — the Lovász–Szegedy compactness theorem (CompactSpace / CompleteSpace GraphonSpaceI)
5. agreement of the coupling and measure-preserving-map cut distances over standard Borel carriers, atoms allowed (cutDistPullback + cutDist_eq_cutDistPullback, via the measure-preserving map from (I, volume) onto any standard Borel probability space — Janson, Thm A.9)
6. separation / inverse counting — carrier-free in both directions (Janson, Thm 8.10): the forward via the coupling counting lemma, the hard converse the analytic summit, pinned cross-carrier with the same-carrier form its specialization and the proof route owned by the representation-on-[0,1] reduction (exists_graphon_unitInterval_cutDist_eq_zero; Janson, Thm 7.1) — and the convergence equivalence (tendsto_graphonSpace_iff_forall_homDensity), with quotient-level graphonSpace_ext_homDensity
7. applications and validation — finite-graph compatibility (finiteGraphGraphon, 0 < m), Goodman, Mantel, Sidorenko-C₄, and computed-value gates (t(K₂,W_{K₄})=3/4, t(K₃,W_{C₅})=0)
8. quantum graphs and reflection positivity — injectively labeled graphs with label-retaining gluing (LabeledGraph.glue : LabeledGraph k → LabeledGraph k → LabeledGraph k, so gluing iterates and the gluing algebra is expressible; forgetLabels for the underlying unlabeled graph), finite connection matrices with Matrix.PosSemidef, and Lovász–Szegedy representability as the four-condition iff IsIsoInvariant / IsMultiplicative / IsNormalized / IsReflectionPositive over the canonical (I, volume) carrier (Lovász–Szegedy, Limits of dense graph sequences, Thm 2.2), with the [0,1] range a derived corollary (graphParam_mem_Icc_of_representability_axioms), never a hypothesis
9. sampling and exchangeable arrays — sampleGraph, the injective density t₀ with the hom-vs-injective closeness and unbiasedness anchors, and the Aldous–Hoover representation

It also records the five pinned design conventions (carrier, cut-distance, finite-graph, carrier-generality, and vocabulary / object-kind choices) — with the rationale for the two load-bearing ones (coupling-primary cutDist, the strict carrier) inlined in the roadmap itself — the entry-point-checked consumed-Mathlib inventory, the reusable infrastructure to build (the (I, volume) transport targets: the measure-preserving map from (I, volume) onto any standard Borel probability space, whose target may have atoms; the atomless mod-null equivalence; and the representation-on-[0,1] reduction; plus dyadic martingale L¹-convergence lemmas), the acceptance gates, and a reviewer checklist.

Files changed

README.md                                     (root index entry, #14)
TauCetiRoadmap.lean                           (root import)
TauCetiRoadmap/DenseGraphLimits/README.md
TauCetiRoadmap/DenseGraphLimits/Suggested.lean

Verification

• lake build green; expected sorry warnings only.

Authorship

Authored by Michael R. Douglas and Cameron Freer, with the assistance of GPT Pro, Claude Code (Opus 4.8 and Fable 5), Codex (GPT 5.5 and 5.6 Sol), Gemini, lean4-skills, and lean-lsp-mcp.

[kim-em]

🤖 Codex says:

Thanks—the five earlier review threads are addressed in the current head, and I have resolved them. I think three specification gaps remain before approval:

1. The Aldous–Hoover endpoint needs an explicit dependency and a graphon-specific target. The Exchangeability roadmap already assigns exchangeable arrays and Aldous–Hoover to its Layer 8, describing it as a substantial tower with its own prerequisites. This roadmap currently names the same development without citing that dependency. Please make DenseGraphLimits consume Exchangeability Layer 8, then pin what this roadmap builds on top of it: the bridge between graphon sampling and symmetric jointly exchangeable Bernoulli arrays or infinite exchangeable random graphs.

2. Layer 9 does not pin the joint sampling architecture needed for its almost-sure claims. sampleGraph W n gives a marginal law for each n; an almost-sure convergence statement across n needs all the samples represented on one probability space, or it must instead be stated through per-n concentration bounds from which such a coupling and Borel–Cantelli argument are constructed. Please pin the intended object and theorem shapes, distinguish almost-sure convergence from convergence in probability or distribution, and name the concentration route. The weak-convergence stack currently cited does not by itself supply that specification. This can naturally be resolved together with the exchangeable-graph bridge above.

3. Layer 8 still jumps from the reflection-positivity predicates to the full representability theorem. Layer 8a defines labeled graphs, gluing, connection matrices, and the four structural predicates, but saying the gluing algebra’s laws are “expressible” does not make their theory a target. Please pin a concrete intermediate proof spine. For example, the cited Lovász–Szegedy route passes from connection-matrix positivity to positivity of the finite fully-labelled matrices, through the Möbius transform f† ≥ 0, then constructs random finite graph laws and uses concentration/Borel–Cantelli to obtain a convergent graph sequence before producing its graphon representation. A quantum-graph or moment-algebra route would instead need its own basic algebra and intermediate results pinned. Whichever route is intended, its dependencies—including any use of Layer 9—need to appear in the roadmap’s ordering rather than being hidden inside the headline theorem.

[cameronfreer]

🤖 Fable 5 (directed by Cameron and reviewed by GPT 5.6 Sol) says:

Thanks — the three gaps are addressed across the six new commits (plus a merge of main), with one deliberate deviation on gap 1 explained below. (Independently useful context: cameronfreer/graphon has advanced substantially and is now sorry-free with no custom axioms; the provenance section is refreshed and pinned at commit 6eccca5, which supplies proved routes for the Layer-9 stack and part of the Layer-8 algebraic substrate.)

1. The Aldous–Hoover endpoint — pinned, but decoupled rather than made a dependency. Layer 9 now ends at a fully pinned graph-level target: ExchangeableGraphLaw (consistent finite marginals under every label injection), sampleExchangeableLaw with the anchor upperMass_sampleExchangeableLaw : P(F ≤ G(k,W)) = t(F,W), IsDissociated with the extremality target exists_graphon_of_isDissociated, the infinite form + compactness extension, and the summit graphonMixtureLawEquiv : ProbabilityMeasure GraphonSpaceI ≃ InfiniteExchangeableGraphLaw — uniqueness explicitly on the graphon quotient, never among raw kernel representatives. The correspondence is pinned beyond its Dirac fibers: alongside the Dirac anchor, the general mixture-coordinate law graphonMixtureLawEquiv_upperMass gives, for every mixing measure P, upperMass F = ∫ t(F,·) dP on the quotient — upper masses determine each finite marginal by Möbius inversion, so an arbitrary permuting Equiv cannot satisfy it (the precedent is the library's infiniteMixtureLawEquiv_law_map_restrictFin). The roadmap names this the Diaconis–Janson graphon-mixture representation (a graph-level Aldous–Hoover consequence), deliberately not "Aldous–Hoover". The reason we did not make DenseGraphLimits consume Exchangeability Layer 8: the prior formalization proves the graph-level correspondence (infiniteMixtureLawEquiv, InfiniteRepresentation.lean) by compactness extension plus the mixture representation, with no array-level input — a dependency edge would overstate the proof dependency. Instead the array-level theory is declared independent parallel work, joined by the bridge you asked for, recorded as a documented future interface — proposed identifier graphLawArrayLawEquiv, equating exchangeable graph laws with symmetric, irreflexive, jointly exchangeable Boolean-array laws — prose-only until the Exchangeability roadmap's array API exists (per the roadmap guide's rule for conditions that cannot yet be stated). Diaconis–Janson (2008) added to References.

2. Joint sampling architecture — pinned. infiniteSampleLaw W is the law of the infinite W-random graph on one probability space (i.i.d. positions + one uniform per pair; Mathlib's MeasurableSpace (SimpleGraph V) covers V = ℕ), with infiniteSampleLaw_map_restrictFin identifying every G(n,W) as a restriction of this single object, and infiniteSampleLaw_eq_extension identifying the explicit sampler with the compactness extension of the sampling marginals — which certifies the sampler's exchangeability and welds the sampling, graph-law, and mixture subsections into one architecture. The two convergence modes are now distinct pinned theorems with distinct named routes: in probability (sampleGraph_cutDist_tendsto_inProbability, LNGL 10.16, on the marginals, via the two-stage point-sampling/Azuma + rounding/union-bound decomposition) and almost surely (infiniteSampleLaw_ae_tendsto_cutDist, on the joint space, via the per-coordinate concentration bound sampleGraph_injHomDensity_concentration — LNGL Prop 11.32 shape, summable tails — Borel–Cantelli per fixed F, countable intersection, and the Layer-6b convergence equivalence). Neither proof consumes the other, and the weak-convergence stack previously cited here is no longer load-bearing for these targets.

3. The Layer-8b spine — pinned as a chain of named targets, and the dependency on Layer 9 is now explicit in the ordering. The route: reflection positivity → graphParamMobius_nonneg (f† ≥ 0, via PSD fully-labelled blocks and the Möbius congruence) and graphParamMobius_sum_eq_one (∑ f† = 1) → the random graph law paramExchangeableLaw (L_f) → paramExchangeableLaw_upperMass (upperMass L_f = f) → isDissociated_paramExchangeableLaw → Layer 9's exists_graphon_of_isDissociated gives L_f = sampleExchangeableLaw W → the sampling anchor closes f F = t(F,W). Note the precise scope of the Layer-9 dependency: the spine consumes the graph-law representation/extremality infrastructure only, not the graphon-sampling concentration theorems — while the spine runs, no representing graphon exists yet, so the classical random-graphs-plus-convergent-subsequence route would additionally need an f†-specific variance or simultaneous-selection lemma; the extremality route needs none. The Ordering section now reads Layer 8a → Layer 9's graph-law layer → Layer 8b.

lake build is green on the new head (Suggested.lean imports only Mathlib; the new declarations are the pins listed above, with graphParamMobius, upperMass, IsDissociated, restrictFin, and the structures ExchangeableGraphLaw and InfiniteExchangeableGraphLaw given real bodies).

Directed by Cameron Freer, written by Fable 5 high, reviewed by GPT 5.6 Sol xhigh.

[cameronfreer]

Thanks—the five earlier review threads are addressed in the current head, and I have resolved them. I think three specification gaps remain before approval:

Thanks for this review. As noted in the longer reply, my cameronfreer/graphon repo is now farther along, and it contains a lot of new relevant details.

Also I think it makes more sense for this roadmap to target the graphon-specific variant of Aldous-Hoover, while the jointly (or separately) exchangeable array versions could be later extensions to the Exchangeability roadmap and eventually meet up with this one somehow.

The other two points were more straightforward.