Graphon.lean

/-
Copyright (c) 2026 Cameron Freer. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Cameron Freer
-/

import Graphon.PermutationExtension
import Graphon.RelationalSignature
import Graphon.RelationalStructure
import Graphon.RelationalTopology
import Graphon.RelPoolGeometry
import Graphon.RelStationaryExtension
import Graphon.RelExtensionLift
import Graphon.RelExchangeableLaw
import Graphon.RelInfiniteLaw
import Graphon.RelLawEquivalence
import Graphon.RelRestrictionBlocks
import Graphon.RelRestrictionIndependence
import Graphon.RelInvariantAction
import Graphon.RelErgodicLinks
import Graphon.RelErgodicExtreme
import Graphon.RelExtremality
import Graphon.RelEqualityPattern
import Graphon.RelKernelEvaluator
import Graphon.RelKernelSampler
import Graphon.KernelRandomization
import Graphon.ForMathlib.BooleanMobius
import Graphon.ForMathlib.CompProdComap
import Graphon.ForMathlib.CondExpComap
import Graphon.ForMathlib.CouplingGluing
import Graphon.ForMathlib.CountableFactorLift
import Graphon.ForMathlib.CondExpRepresentable
import Graphon.ForMathlib.CondIndepRefine
import Graphon.ForMathlib.CondIndepSup
import Graphon.ForMathlib.RelativeFactorCoupling
import Graphon.ForMathlib.UnitIntervalMap
import Graphon.UniformFactorCoupling
import Graphon.RelRankOneTransfer
import Graphon.RelRankOneCoupling
import Graphon.RelRankOneRecovery
import Graphon.RelRankOneScreening
import Graphon.RelRankOneRepresentation
import Graphon.RelRankCoding
import Graphon.RelRankRepresentation
import Graphon.RelRankInjectionInvariance
import Graphon.RelLatentGeometry
import Graphon.RelObservationGeometry
import Graphon.RelPooledLatents
import Graphon.RelPooledExtension
import Graphon.RelPooledAcceptance
import Graphon.RelAustinPolling
import Graphon.RelAustinEnriched
import Graphon.RelRankSuccessorContract
import Graphon.DigraphCoordSupport
import Graphon.RelBipartiteRegression
import Graphon.RelIidEdgeRegression
import Graphon.RelSingletonPeel
import Graphon.RelFixingAlgebra
import Graphon.RelRankAlgebra
import Graphon.RelLowerFactor
import Graphon.RelRankSuccessor
import Graphon.RelRankLatents
import Graphon.RelRankOneCondIndep
import Graphon.RelPollingInfrastructure
import Graphon.RelFixingCondIndep
import Graphon.SeparableFactor
import Graphon.RelCoherentBasis
import Graphon.RelFactorLaws
import Graphon.RelStepKernel
import Graphon.RelBasisSyntax
import Graphon.RelBasisSaturation
import Graphon.DigraphMaps
import Graphon.InfiniteDigraph
import Graphon.SimpleGraphDigraphBridge
import Graphon.InfiniteDigraphLaw
import Graphon.ExchangeableLawBlueprint
import Graphon.Digraphon
import Graphon.SamplerSources
import Graphon.DigraphSampler
import Graphon.DigraphonConstructors
import Graphon.DigraphSamplerFamilies
import Graphon.Basic
import Graphon.Step
import Graphon.HomDensity
import Graphon.Pullback
import Graphon.Operations
import Graphon.Operator
import Graphon.CutNorm
import Graphon.CutDistance
import Graphon.CutNormPullback
import Graphon.StepCostTransport
import Graphon.FiniteFactorApproximation
import Graphon.CouplingTriangle
import Graphon.LevyDownward
import Graphon.MeasureIso
import Graphon.Approximation
import Graphon.Counting
import Graphon.Regularity
import Graphon.RegularityFinpartition
import Graphon.Overlay
import Graphon.Compactness
import Graphon.GraphonSpace
import Graphon.InfiniteGraph
import Graphon.Sampling
import Graphon.CaiGovorov
import Graphon.Lovasz
import Graphon.CrossSuper
import Graphon.SimpleRank
import Graphon.CycleKrylov
import Graphon.MatrixDetermination
import Graphon.SamplingICL
import Graphon.SamplingConcentration
import Graphon.SamplingRounding
import Graphon.SamplingPointwise
import Graphon.SamplingLemma
import Graphon.SamplingLaw
import Graphon.SamplingExamples
import Graphon.SamplingDetermination
import Graphon.SamplingCoordinates
import Graphon.ExchangeableGraphLaw
import Graphon.MixtureConvergence
import Graphon.HomDensityAlgebra
import Graphon.MixtureCoordinates
import Graphon.MixtureUniqueness
import Graphon.InverseCounting
import Graphon.InjectionCounting
import Graphon.SamplingFinite
import Graphon.SubgraphDensities
import Graphon.SubgraphDensityCopyBridge
import Graphon.SubgraphDensityBridges
import Graphon.SubgraphDensityBlueprint
import Graphon.MixtureExistence
import Graphon.MixtureRepresentation
import Graphon.MixtureExtremality
import Graphon.InfiniteLaw
import Graphon.InfiniteExchangeability
import Graphon.InfiniteRepresentation
import Graphon.MixtureKernel
import Graphon.InfiniteSamplingConvergence
import Graphon.McDiarmid
import Graphon.SampleExposure
import Graphon.AlmostSureSampling
import Graphon.LimitGraphon
import Graphon.InfiniteSampleLaw
import Graphon.EmpiricalGraphon
import Graphon.InfiniteExtremality
import Graphon.InfiniteSampler
import Graphon.DissociatedSampler
import Graphon.VertexTail
import Graphon.InvariantAction
import Graphon.RestrictionIndependence
import Graphon.RestrictionIndependenceReverse
import Graphon.ErgodicDecomposition
import Graphon.Convergence

/-!
# Graphons in Lean 4

A formalization of graphons — the theory of limits of dense graph sequences —
in Lean 4 using Mathlib.

## Stable core

* `Graphon.Basic` — Graphon definition, symmetry, boundedness
* `Graphon.Pullback` — Pullback under measure-preserving maps
* `Graphon.Step` — Measurable partitions, step functions
* `Graphon.HomDensity` — Homomorphism density definition
* `Graphon.CutNorm` — Cut norm, graphon integrability
* `Graphon.Approximation` — Rectangle averages, cut norm approximation
* `Graphon.CutDistance` — Cut distance, pseudometric properties, three of the four Rokhlin cores
* `Graphon.LevyDownward` — **Lévy's downward theorem, L¹ version** (Mathlib-upstream candidate, #24): orthogonal projections along an antitone sequence of subspaces converge to the projection onto the infimum; the `Lᵖ`-subspace of an infimum σ-algebra is the intersection; conditional expectations along an antitone sequence of σ-algebras converge in `L¹` to the conditional expectation on the infimum; and conditional expectation over a `0`-`1` σ-algebra is the mean
* `Graphon.MeasureIso` — Atomless standard-Borel measure-isomorphism theorem (graphon-independent; mod-0 iso + everywhere upgrade)
* `Graphon.Overlay` — Overlay theorem: an MP bijection nearly achieves the cut distance (fourth Rokhlin core)
* `Graphon.Regularity` — Energy increment, Frieze–Kannan weak regularity lemma
* `Graphon.RegularityFinpartition` — exact adapter from measurable `Finpartition (Set.univ)` to graphon partitions, including the zero-measure-cell convention
* `Graphon.Counting` — Homomorphism density, counting lemma
* `Graphon.Compactness` — Total boundedness, completeness
* `Graphon.GraphonSpace` — The graphon space: compact Polish standard-Borel metric quotient under weak isomorphism (`GraphonSpace`, `StandardGraphonSpace`)
* `Graphon.InfiniteGraph` — The infinite graph space: `SimpleGraph ℕ` as a compact Polish standard-Borel space; continuous finite restrictions, cylinder π-system, finite-restriction measure extensionality (Aldous–Hoover brick A1)
* `Graphon.CaiGovorov` — Graph-free Vandermonde argument (Cai–Govorov §4), for #70 orbit separation
* `Graphon.Lovasz` — Connection-matrix algebra scaffolding (Lovász §3), incl. the Cai–Govorov #70 orbit theorem and rank theorem
* `Graphon.CrossSuper` — Cross-matrix super-surjective transfer (Cai–Govorov Lemma 5.1, two-matrix partition form)
* `Graphon.SimpleRank` — K=1 simple-graph rank theorem, algebra-atom framing (#70)
* `Graphon.CycleKrylov` — spectral slice of the cycle–Krylov square-moment proof (#70)
* `Graphon.MatrixDetermination` — Algebraic determination of step graphons
* `Graphon.SamplingICL` — Sampling route to the partition-size-independent quantitative inverse counting lemma
* `Graphon.SamplingConcentration` — Concentration scaffold for the First Sampling Lemma (conditional distribution, weighted sample, two-stage reduction)
* `Graphon.SamplingRounding` — The rounding half of the First Sampling Lemma, proved (cut certificate + finite Chernoff)
* `Graphon.SamplingPointwise` — The pointwise half of the First Sampling Lemma: AFKK cut-guessing bound, McDiarmid-at-MGF + soft-max infrastructure
* `Graphon.SamplingLemma` — The First Sampling Lemma, assembled from the two proved concentration events
* `Graphon.SamplingLaw` — The finite sample law of a graphon: `samplePMF`/`sampleLaw`, Möbius/upper-transform engine, relabeling invariance, arbitrary-injection consistency
* `Graphon.SamplingExamples` — The constant graphon samples Mathlib's binomial random graph `G(V, p)`
* `Graphon.SamplingDetermination` — The sample laws determine the graphon: `(∀ k, samplePMF U k = samplePMF W k) ↔ WeaklyIsomorphic U W`, and its `GraphonSpace` form
* `Graphon.SamplingCoordinates` — Continuous point-separating sample-law coordinates on the graphon space; compact coordinate embedding
* `Graphon.ExchangeableGraphLaw` — Exchangeable graph laws (consistent finite marginals) and graphon mixtures; mixtures are exchangeable
* `Graphon.MixtureConvergence` — Weak-convergence layer: mixture coordinates as integrals, Prokhorov extraction, empirical mixing measures
* `Graphon.HomDensityAlgebra` — Hom-density coordinates on the graphon space; multiplicativity over disjoint unions (`homDensity_sum`)
* `Graphon.MixtureCoordinates` — Shared mixture-coordinate layer: hom-density coordinates as bounded continuous functions; their integrals are mixture upper masses
* `Graphon.MixtureUniqueness` — Uniqueness of the graphon mixture: the coordinate StarSubalgebra separates points; `mixtureExchangeableLaw` is injective
* `Graphon.InjectionCounting` — pure counting of vertex maps `Fin k → Fin n` (#94 shared infrastructure): the union (birthday) bound `card_not_injective_le` with its `k²/(n+1)` proportion form, the reciprocal vertex-map-count weight, and the descending-factorial injective-map count `card_filter_injective_eq_descFactorial` — extracted from the mixture-existence collision estimate
* `Graphon.SamplingFinite` — The exact finite-sampling formula: sampling from an embedded finite graph is uniform vertex-map pullback
* `Graphon.SubgraphDensities` — the finite subgraph densities `t`, `t_inj`, `t_ind` (#94): labeled hom / injective-hom / induced-copy counts with their normalization conventions (`n ^ k` all maps vs the `descFactorial` injective count), and the all-maps exact-pullback count, with the small-host zero convention (combinatorics-only import closure)
* `Graphon.SubgraphDensityCopyBridge` — identification of `injHomCount` with Mathlib's `SimpleGraph.labelledCopyCount`
* `Graphon.SubgraphDensityBlueprint` — annotation-only blueprint wrapper for the finite density triangle (keeping `Graphon.SubgraphDensities` Architect-free)
* `Graphon.SubgraphDensityBridges` — the analytic bridges `homDensity_ofSimpleGraphOn_eq_t` / `sampleMass_ofSimpleGraphOn_eq_pullbackCount_div` from the finite densities to the empirical-graphon sampling formulas
* `Graphon.MixtureExistence` — Existence of the graphon mixture: the collision estimate for empirical mixing measures; every exchangeable law is a mixture (`exists_mixtureExchangeableLaw_eq`)
* `Graphon.MixtureRepresentation` — The Diaconis–Janson representation theorem: exchangeable graph laws = graphon mixtures, uniquely (`graphon_mixture_representation`, `mixtureExchangeableLawEquiv`)
* `Graphon.MixtureExtremality` — Diaconis–Janson extremality: dissociated exchangeable laws are exactly the Dirac mixtures (`isDissociated_mixtureExchangeableLaw_iff`)
* `Graphon.InfiniteLaw` — The infinite exchangeable graph law: unique extension of consistent finite marginals to `InfiniteGraph`, via Prokhorov compactness (Aldous–Hoover brick A2)
* `Graphon.InfiniteExchangeability` — Exchangeability of the infinite law under every relabeling; the equivalence `ExchangeableGraphLaw ≃ InfiniteExchangeableGraphLaw` (Aldous–Hoover brick A3)
* `Graphon.InfiniteRepresentation` — The infinite Diaconis–Janson/Aldous–Hoover correspondence: `ProbabilityMeasure (GraphonSpace α μ) ≃ InfiniteExchangeableGraphLaw` (`infiniteMixtureLawEquiv`)
* `Graphon.InfiniteSampleLaw` — The canonical infinite law of a graphon class: quotient descent, finite-restriction marginals, weak continuity, closed embedding into infinite laws
* `Graphon.EmpiricalGraphon` — Empirical graphons of an infinite exchangeable graph: their law is the empirical mixing measure; convergence in distribution to the representing measure
* `Graphon.InfiniteExtremality` — Extremality for infinite exchangeable laws: dissociated ↔ canonical law of a single graphon class ↔ Dirac representing measure
* `Graphon.InfiniteSampler` — Explicit infinite sampler for a fixed graphon: i.i.d. sources via `Measure.infinitePi`; the measurable sampler realizes `infiniteLaw (sampleExchangeableLaw W)` exactly
* `Graphon.MixtureKernel` — The barycenter interpretation: the represented infinite law is the `Measure.bind` mixture of the canonical fiber laws (`mixtureInfiniteLaw_eq`)
* `Graphon.InfiniteSamplingConvergence` — Convergence in probability: the sampled empirical graphons of a `W`-random infinite graph tend to the class of `W` in measure
* `Graphon.McDiarmid` — Bounded-differences concentration at MGF level, packaged as `HasSubgaussianMGF` (Mathlib-upstreaming candidate)
* `Graphon.SampleExposure` — The padded vertex-exposure sampler and the fixed-`F` exponential hom-density tail `2·exp(−ε²k/(2q²))` for `G(k, W)` (Lovász Cor 10.4 form), with the explicit-sampler tail and Borel–Cantelli summability bridge
* `Graphon.AlmostSureSampling` — Almost-sure convergence of the sampled empirical graphons to the class of `W` (Lovász Prop 11.32; Borel–Cantelli over the concentration tails)
* `Graphon.LimitGraphon` — The empirical graphon limit as a universal measurable random variable: `limitGraphon` with law `infiniteMixtureLawEquiv.symm M` under every exchangeable law
* `Graphon.DissociatedSampler` — Functional Aldous–Hoover for dissociated laws: an infinite exchangeable law is dissociated iff it is the law of the explicit `W`-random graph (`isDissociated_iff_exists_sampler`)
* `Graphon.VertexTail` — Vertex-tail infrastructure: the tail shift and σ-algebras, finite-deletion stability of empirical limits, and vertex-tail measurability of `limitGraphon`
* `Graphon.RestrictionIndependence` — Toward DJ Theorem 5.5: the vertex-tail σ-algebra and restriction independence; `RestrictionIndependent ⟹ VertexTailTrivial ⟹ dissociated` (via the tail-measurable empirical limit)
* `Graphon.RestrictionIndependenceReverse` — The reverse arc closing DJ Theorem 5.5: dissociation ⟹ restriction independence (two-block Möbius factorization), and the five-way extremality `tfae_extremality`
* `Graphon.InvariantAction` — The finite-permutation action toward ergodic decomposition (#59): `limitGraphon` is invariant under every finite relabeling, hence invariant-σ-algebra measurable; `IsErgodic`
* `Graphon.ErgodicDecomposition` — The ergodic-decomposition form of extremality (#59 part 2): the six-way equivalence `tfae_ergodic_extremality` adjoining ergodicity under the finite-permutation action, and `invariant_ae_eq_limitGraphon_classifier` — `limitGraphon` generates the invariant σ-algebra modulo null sets; built from fixed-fiber ergodicity (block swap + initial-cylinder approximation)
* `Graphon.PermutationExtension` — `exists_perm_extend`: every `Fin k ↪ ℕ` extends to a permutation of `ℕ` (graph-independent; reused by the graph and relational exchangeability APIs)
* `Graphon.RelationalSignature` — Generic AHK program (umbrella #103), R0 design checkpoint (#110): purely relational multi-sorted `RelSignature`, the `RelCoord`/`RelStructure` carriers, external `NoNullary`, finite/infinite value carriers, the sortwise `RelCoord.map`/`RelStructure.comap` action, and worked digraph/bipartite/ternary examples (the ternary `(i,i,j)` exercising repeated coordinates); no topology/probability yet
* `Graphon.RelationalStructure` — Generic AHK program R1a (#104): sortwise actions on relational structures — `map`/`comap` functoriality, `restrict`/`relabel`, finite restrictions `restrictFin`/`restrictLE`, padding `pad` with the section `restrict_pad`, and restriction composition `restrictLE_restrictFin`/`restrictLE_restrictLE`; still no topology/measure (that is R1b)
* `Graphon.RelExchangeableLaw` — Generic AHK program R2a (#105): exchangeable relational laws — size-vector-indexed `ProbabilityMeasure` marginals with arbitrary sortwise-injection consistency (`RelExchangeableLaw`), the measurable sortwise restriction, diagonal cofinality, and finite-exchangeability of the marginals; no infinite extension yet (R2b/R2c)
* `Graphon.RelInfiniteLaw` — Generic AHK program R2b (#105): the compactness-based infinite extension **realizing the marginals** — diagonal padded laws (`paddedLaw`), Prokhorov subsequence extraction on the compact metrizable structure space, and marginal identification via continuity, giving `infiniteLaw` with `infiniteLaw_map_restrictFin`; exchangeability/uniqueness/equivalence is R2c
* `Graphon.RelLawEquivalence` — Generic AHK program R2c (#105): the finite/infinite exchangeable relational law equivalence — the arbitrary-injection marginal theorem, exchangeability of `infiniteLaw`, `InfiniteRelExchangeableLaw`, the permutation extension, and `relExchangeableLawEquiv : RelExchangeableLaw S ≃ InfiniteRelExchangeableLaw S`
* `Graphon.InfiniteDigraph` — Directed umbrella (#84) D1 (#85): `InfiniteDigraph` as the one-sort binary R1 instance (`digraphSig`) — inheriting compact/standard-Borel, measurable finite restrictions, and measure extensionality (all topology on `InfiniteDigraph`); `Adj` (Prop) / `adjBit` (Bool); `digraphStructureEquiv V` the plain carrier equivalence with Mathlib's `Digraph V`, giving both the infinite `digraphEquiv` and the finite `finiteDigraphEquiv` (for D2); no exchangeable-law theory (that is D2)
* `Graphon.SimpleGraphDigraphBridge` — the symmetric loopless embedding `SimpleGraph.toFiniteDigraph` with its coordinate lemma, injectivity, and range classification, in its own module preserving D1's relational/directed dependency boundary
* `Graphon.RelRestrictionBlocks` — Generic AHK program R3a (#106): sortwise vertex shift `RelStructure.drop` and block embeddings `shiftEmb`; the labeling-free restriction invariance `InfiniteRelExchangeableLaw.law_map_restrict` and shift invariance `law_map_drop`; the initial / after-block / vertex-tail σ-algebras with monotonicity and `iSup_initialAlgebra_eq`; and `IsDissociated` — dissociation as exact finite-event block factorization, with its marginal API
* `Graphon.RelRestrictionIndependence` — Generic AHK program R3b (#106): `RestrictionIndependent` and `VertexTailTrivial` for exchangeable relational laws; **dissociation ↔ restriction independence** (comap-σ-algebra independence of the block maps *is* the block-pair factorization, and the finite windows exhaust the after-block σ-algebra) and **restriction independence → vertex-tail triviality** (independence from every initial σ-algebra upgrades to self-independence); and the **representation-free closing arrow** tail-trivial → dissociated (condition on successively later diagonal tail algebras; Lévy downward + triviality + exchangeability force the block factorization), completing dissociated ↔ restriction-independent ↔ tail-trivial
* `Graphon.RelInvariantAction` — R3c (#106): the finitely supported sortwise relabeling action (`SortwiseFinSupp` with group closure), the strictly invariant σ-algebra, `IsErgodic`, and the **invariant probability simplex** `invariantProbabilityMeasures` with the finitary-invariance bridge (finitary invariance ⇒ full sortwise invariance, via finite-restriction extensionality and finitely supported window extensions) identifying it with the laws of `InfiniteRelExchangeableLaw`
* `Graphon.RelErgodicLinks` — R3c: ergodicity linked into the dissociation triangle — the sortwise block swap, in-measure approximation by initial cylinders, the 4ε approximate-independence core (restriction independence ⇒ ergodicity), vertex-tail ⊆ invariant (ergodicity ⇒ tail triviality), and the iff chain
* `Graphon.RelErgodicExtreme` — R3c: the ergodic ↔ extreme-point theorem for the relabeling group (port of Mathlib's `Ergodic.iff_mem_extremePoints`), with the new absolute-continuity lemma `eq_of_absolutelyContinuous` and the a.e.-to-strict invariant hull upgrade over the countable group
* `Graphon.RelExtremality` — R3c headline: the **five-way extremality equivalence** `tfae_extremality` (dissociated ↔ restriction-independent ↔ tail-trivial ↔ ergodic ↔ extreme), representation-free, with the `digraphSig` regression examples
* `Graphon.RelEqualityPattern` — R4 design checkpoint (#107): sort-tagged values (`RelCoord.taggedValue`), the **equality pattern** as its kernel with the **bundled label-free `EqualityPattern`** (sort-compatible setoid + `blockSort`), the **support** as a finset of tagged values (blocks ≃ support), global and **local latent indices** (`LatentIndex`; `PatternLatentIndex` — the kernel's order-free domain — and `CoordLatentIndex`, canonically equivalent and two-way relabeling-equivariant via `congrMap`), and the `Sigma.map id` transport — the interface for the functional AHK representation (sampler and representation theorem deliberately held back); binary/diagonal/ternary/bipartite examples in their own namespace
* `Graphon.RelKernelEvaluator` — R4 evaluator layer (#107): `RelKernelFamily` (the label-free measurable representing kernels `f_{r,π}` on the finite pattern-local latent product), `RelCoord.localLatents` (the coordinate's window into the global latent source), the measurable `evalStructure`, and the **equivariance theorem** `evalStructure_relabel` (relabeling the evaluated structure = precomposing the source with the latent-index action) with the pattern↔image transport square `patternLatentIndexEquivCoord_map` — latent source measure, sampler pushforward, and representation theorem deliberately held for the next layers
* `Graphon.RelKernelSampler` — R4 sampler layer (#107): the evaluator over an arbitrary carrier (`RelKernelFamily.eval`, definitionally `evalStructure` on `Vinfinite`) with the pullback transport `eval_comap`; the i.i.d. uniform `latentSource` over global subset-latent indices with relabeling invariance (via `LatentIndex.relabelEquiv`); and the **evaluated exchangeable law** `RelKernelFamily.evalLaw` with its **dissociation** `evalLaw_isDissociated` (disjoint vertex windows read disjoint nonempty subset-latent collections, so the i.i.d. source factorizes) — the forward half of the dissociated functional AHK representation; the converse representation theorem is the remaining content of #107
* `Graphon.KernelRandomization` — R4 converse piece 1 (#107): the small adapter from Mathlib's kernel representation theorem (`Kernel.exists_measurable_map_eq_unitInterval`, Kallenberg Lemma 4.22) to the project's uniform source — `Kernel.exists_measurable_map_eq_uniform01` (a Markov kernel into a standard Borel space is the pushforward of `uniform01` by a jointly measurable map, the `[0,1]`-subtype input adapted through `Set.projIcc`) and the single-measure corollary `Measure.exists_measurable_map_eq_uniform01` — the randomization ("noise outsourcing") input for the converse representation theorem
* `Graphon.ForMathlib.BooleanMobius` — the upper zeta transform and its explicit signed inverse on finite Boolean lattices over `ℚ`, with `(-1) ^ #(t \ s)` counting elements added above `s`
* `Graphon.ForMathlib.CompProdComap` — **upstream candidate** (signature-free, Mathlib-only imports): change of variables in the *source* of a composition-product, `(μ ⊗ₘ κ.comap e he).map (Prod.map e id) = μ.map e ⊗ₘ κ`, with the composition-level corollary `Measure.comp_comap : (κ.comap e he) ∘ₘ μ = κ ∘ₘ μ.map e` obtained as its second marginal. Mathlib has `Kernel.comap` and `Measure.compProd` but not their interaction. Extracted from a private lemma in `Graphon.RelStepKernel` and **weakened from a measurable equivalence to a plain measurable `e`** — nothing in the argument uses an inverse, since the preimage step is definitional for `Prod.map e id` and `setLIntegral_map` needs only measurability. Consumers that must *cancel* the pushforward carry `MeasurableEmbedding e` themselves; surjectivity is never used here
* `Graphon.ForMathlib.CondExpComap` — signature-free, Mathlib-only imports: **conditioning along a factor map**. `condExp_comp_measurePreserving`: for `T` carrying `P` to `μ`, `(μ[g | m]) ∘ T =ᵐ[P] P[g ∘ T | m.comap T]` — the transported conditional expectation is the conditional expectation of the transported function, conditioned on the pullback algebra. `condIndepFun_comp_measurePreserving` / `iCondIndepFun_comp_measurePreserving` pull pair and family conditional independence back along `T` the same way, through the shared single-event form `condExp_set_comp_measurePreserving`. Mathlib's `CondIndepFun.comp` composes only on the codomain side; the domain-side transport is what lets facts proved on a coupling's marginal be consumed on the coupling itself
* `Graphon.ForMathlib.CouplingGluing` — signature-free, consumes only `RelativeFactorCoupling`: **gluing two couplings over a shared marginal** — the measure-theoretic core of the coupling-distance triangle inequality (Janson Lemma 6.5). `gluedCoupling` is the relative joining of the two couplings over their common middle factor, reordered to the triple product; the `(1,2)`-projection is exact and unconditional, the `(2,3)`-projection exact via the common-factor identity, and `gluedOuterCoupling` packages the induced `(1,3)` coupling with both marginals exact. `condDistrib` disintegration means **zero-mass middle atoms never divide by zero** — regressed by running the middle through a Dirac mass. Standard Borel carriers only (covering every finite discrete carrier); **this does not establish the arbitrary-carrier triangle inequality**, which additionally needs stability of the reduction under step approximation — addressed nowhere in this module. Extended with **factor-map pushforward laws** (`isProbabilityMeasure_map_prodMap`, `map_prodMap_map_fst/snd`): exact marginals of a coupling pushed through a pair of measurable factor maps — measurability only, no finiteness of targets and no cell positivity; finite quotients are a later consumer by instantiation
* `Graphon.CutNormPullback` — step 1 of the step-approximation programme: **cross-carrier cut-norm contraction** `cutNormDiff_pullback_le_measurePreserving` — pulling two graphons back along a measure-preserving map between **arbitrary probability carriers** does not increase the cut-norm difference, with **no standard Borel hypothesis**: the rectangle weights are Radon–Nikodym densities of the mapped restricted measures (`[0,1]`-valued a.e. since those measures are dominated by the target), truncated to land in the everywhere-bounded weighted estimate `abs_weighted_integral_diff_le`. The same-carrier `cutNormDiff_pullback_le` retains its statement; its `[StandardBorelSpace α]` is now demonstrably not needed for this inequality. Extended with step 4's outputs 1–2: **cross-carrier cut-norm isometry** `cutNormDiff_pullback_eq_measurePreserving` — for kernels factoring through the map the pullback is an exact isometry, not merely a contraction (`rectIntegralDiff_pullback_preimage` transports every rectangle test with equal value) — and **generic Lipschitz stability of coupling cost** `abs_cutNormDiff_pullback_sub_le`: changing both marginal kernels moves the pulled-back cut-norm difference by at most the sum of the marginal cut-norm differences
* `Graphon.StepCostTransport` — steps 4.3–4.4 of the step-approximation programme: **exact step-kernel cost transport** `cutNormDiff_pullback_prod_factor` — under any coupling pushing to the factor law, the coupling cost of pulled-back step kernels equals the quotient step-kernel cost, an equality via pullback functoriality + the cross-carrier isometry; the step-3 pushforwards packaged as `MeasurePreserving` witnesses; the instantiation `cutNormDiff_pullback_countableFactorLift` at the countable-factor lift; and `abs_cutNormDiff_pullback_sub_stepCost_le`, **the approximation bound step 5 consumes** — coupling cost differs from quotient step-kernel cost by at most the sum of the carrier-side step-approximation errors. Finite gluing and the triangle assembly remain later units
* `Graphon.FiniteFactorApproximation` — step 5a: **every graphon has a finite-factor approximation at every scale**. `FiniteFactorApproximation U ε` bundles a factor map `Ω → Fin (n + 1)`, its bundled `ProbabilityMeasure` law, the measure-preserving witness, and a kernel on the finite factor with `cutNormDiff U (pullback kernel factor) < ε`; `exists_finiteFactorApproximation` proves existence for every `0 < ε` with **no standard-Borel, surjectivity, or positive-cell hypothesis**. The Frieze–Kannan partition from `Graphon.regularity` is indexed by an enumeration of its parts, a final index absorbs the null set of points no part covers (so no covering assumption is needed), and the kernel is the matrix of rectangle averages — `rectAverage` is already zero on null cells. `pullback_stepKernel` identifies the pullback of that kernel with the stepification, which is what transports the regularity bound into factor form. This is the **individual** approximation applied once per graphon; there is no shared factor across carriers, and the triangle assembly reuses the middle graphon's approximation in both pairwise couplings
* `Graphon.CouplingTriangle` — step 5b, the closing unit: **the arbitrary-carrier coupling-cost triangle**, stated throughout at the level of the coupling cost at fixed couplings and never as a distance. `cutNormDiff_gluedOuterCoupling_le` is the factor-level cost triangle and is **lossless** — all three costs are pulled back to the glued triple law, where a single `cutNormDiff_triangle` applies, and the cross-carrier isometry identifies each pulled-back cost with the original, so the transport costs nothing. `exists_coupling_cutNormDiff_le_add_add` assembles it over **arbitrary probability carriers with no standard-Borel hypothesis** — gluing happens on the *finite* factors, where standard Borel is automatic: push both couplings to the finite factors (their middle marginals agree precisely because the middle graphon's approximation is **shared**), glue there, lift the glued factor law back by `countableFactorLift`, transport the cost exactly, and pay one approximation error at each of the three comparisons, `(e₁+e₃) + (e₁+e₂) + (e₂+e₃) = 2(e₁+e₂+e₃)`. `exists_coupling_cutNormDiff_le_add_add_of_pos` is the ε-form, invoking `exists_finiteFactorApproximation` at scale `ε/6`. A cross-carrier coupling *distance* and its triangle inequality would need an infimum over couplings, which this repository does not yet define — hence the deliberate "cost" phrasing throughout
* `Graphon.ForMathlib.CountableFactorLift` — step 3 of the step-approximation programme, signature-free: **lifting a countable-factor joint law to the carriers**. Given factor maps `q₁, q₂` into countable spaces with measurable singletons (explicit hypotheses — no hidden discrete instances) and a joint law `lam` on the factor product whose marginals are the pushed carrier measures, `countableFactorLift` couples the carriers by mixing normalized cell restrictions with weights `lam {(i,j)}`. Both carrier marginals are exact (`countableFactorLift_map_fst/snd`), the lift is a probability measure whenever a carrier is, and the acceptance test is the exact atomwise round-trip `countableFactorLift_map_prodMap`: pushing back through `Prod.map q₁ q₂` recovers `lam` on the nose. **Null cells are annihilated, never divided by**: marginal compatibility forces `lam` to vanish on any cell with a null fiber (the guards), so normalization only ever cancels against positive mass — regressed on a genuinely mixed example with one positive coin cell and one annihilated null cell. Cost transport across the lift and the triangle assembly are later units
* `Graphon.ForMathlib.CondExpRepresentable` — **upstream candidate** (signature-free, Mathlib-only imports): conditioning is insensitive to replacing a σ-algebra by one that represents it **modulo the measure**. Given `m₂ ≤ m₁` and an eventwise representative in `m₂` for every `m₁`-set, `condExp_eq_condExp_of_ae_representable` gives `μ[f | m₁] =ᵐ μ[f | m₂]`, and `iCondIndepFun_congr_of_ae_representable` transfers mutual conditional independence between the two. This is the recurring R4 situation where an abstractly defined conditioning algebra has a concrete factor-map realization that generates it only eventwise: no σ-algebra equality is available or claimed, but everything conditional expectation can see transfers. **The proof deliberately does not lift the hypothesis from sets to functions** — Mathlib's `EventuallyMeasurable` warns that eventual measurability is strictly weaker than a.e. equality to a measurable function and leaves the equivalence a TODO, so that route would mean redoing simple-function approximation. Instead the uniqueness argument runs in the other direction: `μ[f | m₂]` is the *candidate* at `m₁`, already `m₁`-strongly measurable since `m₂ ≤ m₁` is raw, and its set integrals over `m₁`-sets are computed by moving to an `m₂` representative. The conditional-expectation statement needs only `[IsFiniteMeasure μ]`; the standard Borel hypothesis on the `iCondIndepFun` corollary is forced by Mathlib defining `iCondIndepFun` through `condExpKernel`, not by the argument
* `Graphon.ForMathlib.CondIndepRefine` — signature-free, Mathlib-only imports: **refining the conditioning of mutual conditional independence**. `iCondIndep_of_condIndep_iSup`: a family mutually conditionally independent given `m'` stays so given any larger `m₂ ≥ m'` that is conditionally independent of the family's join given `m'`. The engine is a private projection identity `μ⟦E | m₂⟧ =ᵐ μ⟦E | m'⟧` for join-events `E`, proved by uniqueness of conditional expectation at `m₂` with candidate `μ⟦E | m'⟧`, the pull-out property, and the product identity of conditional independence; it stays private until a second consumer pins down its natural generality
* `Graphon.ForMathlib.CondIndepSup` — signature-free, Mathlib-only imports: three closure properties of conditional independence. `CondIndep.sup_right`: joining the conditioning algebra to one side is free — `m₁ ⊥⊥ m₂ ∣ m'` gives `m₁ ⊥⊥ (m' ⊔ m₂) ∣ m'`, via the π-system `{e ∩ f}` generating the join and the indicator pull-out `condExp_indicator`. `CondIndepFun.congr`: `CondIndepFun` respects a.e. equality of the functions — the conditional analogue of `IndepFun.congr`, absent from Mathlib; it is what lets a variable only a.e. equal to a conditioning-measurable one be absorbed into a side. `CondIndepFun.congr_cond`: the conditioning σ-algebra may be replaced by an equal one, the dependent `≤` proof moving by proof irrelevance once the equality is substituted — needed wherever a conditioning map is reindexed, and consumed by the rank-one coupling and screening arguments and by the pooled screening transport
* `Graphon.ForMathlib.RelativeFactorCoupling` — **upstream candidate** (signature-free, Mathlib-only imports): the **relatively independent joining over a common factor**, `relativeFactorCoupling μ ν q r = (condDistrib id q μ ×ₖ condDistrib id r ν) ∘ₘ μ.map q`, for measurable `q : Ω → Z`, `r : Ξ → Z` with `ν.map r = μ.map q`. Both sides are disintegrated over `Z` and the fibres multiplied independently; the independent product `μ.prod ν` would not identify the factors, and an arbitrary coupling that did could still let each side see more of the other. The engine is `map_condDistrib_id`, **fibre concentration**: pushing `condDistrib id q μ` through `q` is the deterministic identity kernel, i.e. conditioning on `q` pins down `q`. From it: both marginals, the common-factor identity `q ∘ Prod.fst =ᵐ r ∘ Prod.snd` (proved from the two fibre-concentration statements, one per side — equality of the factor *marginals* says nothing about the joint), and `condIndepFun_fst_snd_relativeFactorCoupling`, conditional independence of the two coordinates given `comap (q ∘ Prod.fst)`. The conditioning is deliberately on that variable, defined on the coupling space, rather than on the disintegration variable `∘ₘ` integrates out: only the former is visible to consumers, who see the coupling and not its construction. No σ-algebra equality `σ(q ∘ fst) = σ(snd)` is claimed — the latent may carry strictly more than the factor, as `U` carries more than `1_{U < p}`; what conditional independence excludes is that the surplus says anything further about the first coordinate. `map_prodMap_relativeFactorCoupling_two_sided` is the general symmetry: measure-preserving maps on both spaces shifting the two factors by one `e` give invariance under `Prod.map T U`, with the factor-law pushforward identity derived from the commuting square rather than assumed
* `Graphon.ForMathlib.UnitIntervalMap` — Mathlib-only packaging of its standard-Borel kernel representation as a measure-preserving map from `[0,1]`, with atomic and mixed-law regressions; this is a prescribed-pushforward theorem, not pointwise surjectivity
* `Graphon.UniformFactorCoupling` — R4 converse piece 3 (#107): the uniform specialization of the joining above, `exists_relativeFactorCoupling_uniform01`. The only uniform-specific input is `Measure.exists_measurable_map_eq_uniform01` (#140), which supplies the coding map `f : ℝ → Z` matching the two factor laws; everything after is generic. It runs in the direction `Graphon.KernelRandomization` does not — that module manufactures a variable with a prescribed law *out of* a uniform, whereas here a uniform is manufactured *alongside* an already-given variable — and it is reusable at every rank, so it replaces a port of an external de Finetti package with the narrow transfer step the recursion actually needs
* `Graphon.RelRankOneTransfer` — R4 converse piece 3 (#107): **I(1)**, the base of the rank recursion, instantiating the relative joining at `q = lowerFactorMap 1`. `lowerFactorMap_one_relabel` is the rank-one degeneracy that makes this work: `LowerIndex 1` holds exactly the indices anchored at `∅`, whose events are `invariantAlgebra`-measurable, so the rank-one factor map is relabeling invariant **on the nose** — not merely equivariant, no null sets, no transport of the factor space — and the equivariance square of `Graphon.RelLowerFactor` degenerates. Hence `map_prodMap_relabel_rankOneCoupling`: every finitely supported sortwise relabeling of the structure coordinate preserves the coupling, acting inside the fibres of the disintegration. At higher rank this fails and the statement will have to move the factor space by `lowerFactorSpaceEquiv` on the other side. `exists_rankOneUniformCoupling` bundles the six clauses; the conditional-independence clause is the one that cannot be dropped, since marginals plus the resolution identity `lowerFactorMap 1 X = f ξ` still permit a latent encoding arbitrary information about what rank one leaves unresolved. It is stated over the whole structure coordinate, so any particular unresolved reading follows by composition — recorded explicitly as `condIndepFun_comp_fst_snd_rankOne`
* `Graphon.RelRankOneCoupling` — R4 converse piece 3 (#107): the #161 coupling transported onto the rank-one **latent space**. `rankOneLatentCoupling f` moves the latent coordinate through `rankLatentOneEquiv`, and `exists_rankOneLatentCoupling` proves the coupling-side facts needed to build `RankRepresentation`: probability, law and `rankLatentSource` marginals, **joint** relabeling invariance (the latent side collapses by `rankLatentRelabel_one_eq`, so #161's structure-side invariance suffices — a rank-one degeneracy), resolution of the rank-one factor through a measurable latent read, and conditional independence of the latent from every measurable reading of the structure given the rank-one factor. The conditional-independence clause transports along the *reverse* measure-preserving direction via `condIndepFun_comp_measurePreserving`, with `MeasurableSpace.comap_comp` collapsing the conditioning and `CondIndepFun.comp` straightening the codomain. No σ-algebra equality between latent and factor is claimed
* `Graphon.RelRankOneRecovery` — R4 converse piece 3 (#107): the `lower_recovers` input for rank one. `exists_blockMap_recovery_of_card_lt_one`: under any coupling with the law as structure marginal that resolves the rank-one factor through a measurable latent read, the block strictly below rank one — the nullary block — is a.e. a measurable function of the latents visible at its own support. Coordinatewise: each nullary coordinate is an invariant event, #157's eventwise generation supplies a factor-event representative modulo the law, a `decide`-indicator codes the chosen events into `BlockSpace ∅`, the null disagreements combine over the countable `BlockIndex ∅` by `ae_all_iff` and transport along `fst`, and the latent read factors **exactly** through `localLatents ∅ 1` (a bijective reindexing at rank one). Stated over an abstract coupling so the assembly passes its destructured clauses; everything is modulo the coupling measure
* `Graphon.RelRankOneScreening` — R4 converse piece 3 (#107): **the conditioning ladder**. `iCondIndepFun_blockMap_singleton_comap_snd`: under the rank-one coupling clauses, the singleton blocks (through `singletonBlockRead`) are **mutually** conditionally independent given the full latent σ-algebra `comap snd` — the support-free core of `screening`. The conditioning climbs and descends by the merged tools: #173 peel pulled along `fst` (#175) at `invariantAlgebra.comap fst`; **down** to `comap (lowerFactorMap 1 ∘ fst)` by #163 with #157's eventwise generation pulled along `fst`; **up** to the join with the latent algebra by #174, its hypothesis from the coupling's cond-indep clause via `condIndepFun_iff_condIndep`, monotonicity, and `CondIndep.sup_right` (#176); **down** to `comap snd` alone by #163 again, the join's representability from the resolution identity and `eventuallyMeasurableSet_sup` (#176). Every move is modulo the coupling measure; no identification of the latent σ-algebra with the invariant algebra is asserted anywhere. Extended by the **per-support specialization** `condIndepFun_blockMap_restObservation_one` (basis-free — it consumes the ladder's conclusion as a hypothesis): one-vs-rest via `condIndep_iSup_of_disjoint`, the remainder rerouted through the recovered nullary read (`CondIndepFun.congr` absorbs the a.e. rerouting), and the conditioning restated through the raw rank-one identity `comap_localLatents_one_snd` (at rank one every latent coordinate is visible at every support)
* `Graphon.RelRankOneRepresentation` — R4 converse piece 3 (#107): **the rank-one representation exists**. `InfiniteRelExchangeableLaw.nonempty_rankRepresentation_one`: every exchangeable law has a `RankRepresentation 1` — no dissociation, no `NoNullary`, no basis in the statement (chosen internally via `nonempty_coherentBasis` and never escaping). Fields by provenance: coupling/marginals/invariance from `exists_rankOneLatentCoupling`; `lower_recovers` from the nullary recovery; `screening` from the per-support specialization of the conditioning ladder fed by the coupling's cond-indep clause at the identity reading. No identification of the invariant σ-algebra with the latent σ-algebra is asserted
* `Graphon.RelPoolGeometry` — R4 converse, stationary-extension layer 1 (#107): **law-free pool geometry**. `PoolVertex S s := Vinfinite S s ⊕ Vinfinite S s` with the original/pool embeddings (disjointness and exhaustivity definitional from `Sum`), the fixed sortwise identification `poolVertexEquiv : PoolVertex S s ≃ Vinfinite S s` (both summands together are again a countably infinite carrier — what transports the law in the cheap existence theorem), structure transport along sortwise equivalences as the measurable equivalence `RelStructure.congrCarrier` (both directions `comap`s), the two half-restrictions with measurability, transport–relabel naturality by conjugation, and the **split-only** restriction–relabel laws (`Equiv.sumCongr`, definitional). **Deliberately no mixed-permutation subtype**: the extension's relabeling action quantifies over raw `∀ s, Equiv.Perm (PoolVertex S s)` — boundary-crossing freedom is load-bearing for polling, and restriction–relabel commutation is stated only where it is honest
* `Graphon.RelStationaryExtension` — R4 converse, stationary-extension layer 2 (#107): the approved contract, exactly. `law_map_restrict_self` (the law of any sortwise injective self-restriction is the law, via `ext_of_map_restrictFin`); the minimal `StationaryExtension` structure (`law : ProbabilityMeasure` on the pooled space, original restriction = the law, invariance under **every** sortwise permutation of the pooled carrier — mixed permutations included, the load-bearing quantifier); the **exact mixed-window marginal** `law_map_restrict_window` (any sortwise finite embedding into the pooled carrier has the rank-`n` marginal — proved by moving the window into the original half with a permutation built from `exists_perm_extend`, absorbed by invariance via the #181 moved-window law); `extensionCoupling` with exact marginals (shared-array definitional; **no independence claimed — the exclusion is the design**); and the **cheap existence theorem** `nonempty_stationaryExtension` (transport along `poolVertexEquiv` + `congrCarrier`), explicitly marked as *not* the induction step: the hard theorem is extracting correlated auxiliary latents with recovery and screening. All measure identities exact
* `Graphon.RelExtensionLift` — R4 converse (#107): **the split-equivariant extension lift**. `RankRepresentation.extensionLift` glues a rank-`n` representation and a stationary extension by the relative joining over their common structure marginal; exact marginals (`extensionLift_map_fst` = the representation — recovery and screening pull back through it, no transfer lemmas needed; `extensionLift_map_snd` = the extended law); **split-diagonal invariance** `extensionLift_map_split` via the two-sided coupling transport (its second consumer) with the #181 split naturality — **and deliberately nothing stronger: mixed pooled permutations do not act on this object** (no factor square; old latents index original-carrier supports only) — the pooled-latent extension gate on #107 is a separate unit; and the joining clause `condIndepFun_fst_snd_extensionLift` (`(X, U_{<n}) ⊥⊥ X⁺ ∣ σ(X)`), which manufactures no correlated latents
* `Graphon.RelSingletonPeel` — R4 converse piece 3 (#107): `iCondIndepFun_of_fixingAlgebra_singleton`, mutual conditional independence at rank one for **any** vertex-indexed family measurable for its own singleton fixing algebra. Basis-free; the coherent-basis exact layers and the raw relation blocks are both instances. Fails above rank one because equal-rank supports can meet
* `Graphon.RelRankRepresentation` — R4 converse piece 3 (#107): the **specification** a rank-`n` joint representation must satisfy — coupling primitive, both marginals, joint relabeling invariance, local recovery, rank-truncated screening. **Interface only; no existence theorem at any rank.** Independent of `CoherentBasis`. See the module header for the design rationale and the two acceptance tests
* `Graphon.RelLatentGeometry` — R4 converse (#107), law-free: **carrier-parametric latent geometry**. Supports of cardinality below the working rank over an arbitrary sortwise carrier, the latent cube they index, its i.i.d. uniform source, the action of a **full** sortwise permutation family with identity/composition laws and exact source invariance, restriction along a sortwise embedding of carriers, and the naturality laws — including the honest moved-window form, since a permutation crossing the image of an embedding does not commute with restriction along it. The action is by the full family deliberately: finite support is a property of a particular carrier's automorphisms, not of latent cubes, so a finitely supported subgroup is obtained by restricting this action rather than the reverse. `RankLatentIndex` is now a compatibility alias for the core at `Vinfinite S` — definitionally, with no downstream change
* `Graphon.RelObservationGeometry` — R4 converse (#107): the **observation layer over an arbitrary carrier** — local latents, blocks of raw relation coordinates, and the rank-truncated remainder. The `Vinfinite`-indexed originals are compatibility aliases, so pooled recovery and screening instantiate this core rather than duplicating it. **The three do not transport equally, and the difference is truth rather than proof effort**: `localLatentsOver` and `blockMapOver` are local — they read only coordinates supported inside a given finite set — and admit naturality along an arbitrary sortwise **embedding**; `restObservationOver` is global, ranging over *every* rank-`≤ n` coordinate of the ambient carrier other than the one at `A`, so along an embedding into a larger carrier the target remainder sees coordinates the source cannot and an embedding-level commuting law would be **false**. It transports only along a carrier **equivalence** — for the pooled setting, the canonical `poolVertexEquiv`
* `Graphon.RelPooledLatents` — R4 converse (#107), stage 1 of the pooled-latent extension gate: the core instantiated at `PoolVertex S`. `PooledRankLatentIndex`/`PooledRankLatentSpace`/`pooledRankLatentSource`; `pooledRankLatentRelabel`, the action of the **full mixed** pooled family `∀ s, Equiv.Perm (PoolVertex S s)` — permutations moving vertices between halves included — with its identity and composition laws and exact source invariance; and `restrictOriginalLatents`, the measurable restriction to latents indexed by original supports, whose codomain is the rank-`n` cube itself because the index type is the carrier-parametric one. Naturality is stated in the **honest moved-window form** valid for every pooled permutation, with the commuting square available only as the split corollary. Law-free: no `RankRepresentation`, recovery, screening, or coupling appears, and those enter at later stages of the gate
* `Graphon.RelPooledExtension` — R4 converse (#107), stage 2 of the pooled-latent extension gate: **the pooled rank extension**. `PooledRankExtension C` carries exactly three fields — the joint law on the pooled structure space times the pooled latent cube, its exact restriction to `C.P` along the two original restrictions, and invariance under the **full** pooled permutation family (mixed permutations included, the load-bearing quantifier). **No independence field**: an independent pool would recreate the defect of the rejected factor coupling. `RankRepresentation.pooledExtension` is the cheap constructor, and both of its laws are `map_prodMap_restrict_self` in disguise — writing `pv` for `poolVertexEquiv` and `ov` for `originalVertex`, the transport is `comap pv` on structures and restriction along `pv` on latents; `restrictOriginal ∘ transport` is `comap (pv ∘ ov)` with `pv ∘ ov` a **self-injection** of the original carrier, and `relabel ρ ∘ transport = transport ∘ relabel κ` for the conjugate `κ = pv ∘ ρ ∘ pv⁻¹`, a **permutation** of it. The structure deliberately carries **no mixed-window field**: the joint mixed-window marginal, and current-rank recovery and screening on mixed pooled supports, are separate derived consequences of the three fields rather than part of the primitive, and nothing route-specific belongs here
* `Graphon.RelPooledAcceptance` — R4 converse (#107), stage 3 of the pooled-latent extension gate, organizing result: **the joint restriction theorem**. For *every* sortwise embedding `e : ∀ s, Vinfinite S s ↪ PoolVertex S s`, restricting a pooled rank extension jointly — structure and latents along the same embedding — returns the representation exactly: `Q.law.map (Prod.map (RelStructure.restrict e) (latentRestrictOver e n)) = C.P`. Being **joint** is the point: it recovers the `(X, U_{<n})` law and says strictly more than a structure-only window theorem. Proved by joint-cylinder extensionality plus finite agreement with a mixed pooled permutation — on a cylinder the combined vertex support is finite, the assignment `originalVertex v ↦ e v` there is a finite partial injection of the pooled carrier, and `exists_perm_extend_of_injOn` extends it; the full mixed invariance then absorbs the permutation, which is also what lets it be chosen independently on each sort with no finite-support or uniform-bound issue. The four route-neutral consequences follow from it: `map_snd` (the pooled latent marginal is the pooled i.i.d. source), `toStationaryExtension` (the structure marginal is a `StationaryExtension M`), `lower_recovers` (local recovery on every pooled support below rank `n`, the decoder conjugated through the local and block measurable equivalences), and `screening` (screening on every pooled support of rank `n`, a pullback through `measurePreserving_pooledJointEquiv` followed by `CondIndepFun.comp` on the codomains and `CondIndepFun.congr_cond` with `comap_measurableEquiv_comp` on the conditioning algebra — no conditional-expectation reasoning). `PooledRankExtension.map_poolVertexEquiv` is the canonical specialization; bundling that restriction as the measurable equivalence `pooledJointEquiv` and cancelling it yields **`PooledRankExtension.law_eq`, a uniqueness theorem** — every pooled rank extension *is* the cheap one. Marginals, the `StationaryExtension` structure, recovery and screening therefore transport from `C.P` through one canonical law identity rather than requiring separate measure arguments
* `Graphon.RelRankSuccessorContract` — R4 converse (#107), **interface only**: the shared witness both successor constructions must produce, and the two identically typed statements they target. `RankSuccessor C` carries the next representation together with **exact truncation compatibility**, `next.P.map (Prod.map id (rankLatentProjection (Nat.le_succ n))) = C.P` — the observable that makes the statement mention `C` at all. A theorem returning merely `Nonempty (RankRepresentation (n + 1))` could ignore `C` and produce an unrelated representation, which is the same underdetermination that sank the earlier shell attempt. The witness carries **no independence field** beyond `RankRepresentation`'s own, and **no equality between the two routes' outputs** is asserted — they prove one statement by different means and will not produce canonically equal representations. `AustinSuccessor` and `KallenbergSuccessor` are the same proposition by construction, so whichever lands first discharges the induction while the other remains an independent proof. Regression: `truncation_zero` shows the truncation equation is **automatic at rank zero** — the rank-zero latent cube is a single point, so both sides are determined by their structure marginals, which the representation axioms already pin, and the base case imposes nothing extra. The witness exposes no pooled carrier, so whether a construction genuinely used boundary-crossing permutations is observed by the pooled gate's `map_restrict_embedding` rather than by any final-output check here; each route's intermediate construction consumes that theorem. Adversarial examples are kept in route-independent regression modules, outside this interface
* `Graphon.DigraphCoordSupport` — shared regression infrastructure: the support of a digraph coordinate is the pair of its endpoints, with the off-diagonal cardinality corollary, over an arbitrary vertex type. A bridge module so that the D1 carrier `Graphon.InfiniteDigraph` does not acquire a dependency on the equality-pattern layer where `RelCoord.support` lives — the same separation `Graphon.SimpleGraphDigraphBridge` maintains for `SimpleGraph`. Stated with `[DecidableEq V]` and proved by membership, because `RelCoord.support` is built classically and over a concrete carrier the natural instance is not definitionally the classical one, so an image-shaped statement would not apply at the sites that need it
* `Graphon.RelAustinEnriched` — R4 converse (#107/#197), **route A (Austin) unit 2**: the Austin base, its action, and the base-extended bundle with its coherent-basis adapter. `AustinBaseSpace = PooledRankLatentSpace × ClusterSpace` is the equivariant base over which the enriched kernel is later built, and **its two components differ in kind**: the latent component carries no rank-`n` latent, every pooled index having cardinality `< n`, while the cluster component deliberately carries rank-`n` blocks at supports that are not wholly original — the clusters are correlated structural polling data, which is precisely why conditioning on them is informative. `poolLift` acts on the original half and fixes the spare half, and its preservation of `Sum.isRight` keeps mixed clusters mixed. **The orientation is contravariant** — `Equiv.trans` applies its first argument first, so `austinBaseRelabel (σ * τ) = austinBaseRelabel τ ∘ austinBaseRelabel σ`. `enrichedPollingMap_naturality` is **one square for all four components**: structure and pooled latents definitionally, clusters by `pollingClusters_relabel`, original latents by the split corollary `restrictOriginalLatents_sumCongr`; `enrichedPollingLaw_map_enrichedAction` derives exact invariance from it using nothing but `Measure.map_map` and the extension's own invariance. `austinEnrichedObject` builds the bundle as the **exact pushforward** of `enrichedPollingLaw` along the compression dropping the redundant original-latent coordinate, so `map_original` recovers `C.P` through `map_restrict_embedding` at the original-vertex embedding. The adapter is stated for an **arbitrary** coherent basis, so no `Fintype S.Srt` enters anywhere in this module; `map_recombine` recombines lower and layer through `lowerFactorSpaceSuccEquiv.symm` to return the rank-`(n+1)` lower-factor law exactly — a prerequisite for exact truncation rather than that statement itself, since it mentions neither `C.P` nor `rankLatentProjection`. The dependent cluster fibres are handled by `Bool`-valued pointwise bridges, with the single required cast isolated in one private lemma rather than by weakening `MixedClusterIndex`'s reducibility, which would expose a substantive subtype's implementation globally to solve a local elaboration problem
* `Graphon.RelAustinPolling` — R4 converse (#107/#197), **route A (Austin) unit 1**: pooled polling. Austin's Proposition 3.12 polls with swaps into a *spare vertex set*, and the pooled carrier is exactly that — `PoolVertex` is `Vinfinite ⊕ Vinfinite` with `originalVertex = Sum.inl` and `poolVertex = Sum.inr`, so the halves are disjoint definitionally, and the extension's invariance under the **full** pooled permutation family means the swaps carry no finite-support side condition. **The geometry is the delicate part**: the observed blocks are confined to the original half and the poll to supports containing a spare vertex, so the two families are disjoint by construction — reading the blocks through the canonical `pooledJointEquiv` instead is tempting, since it makes the transport to `C.P` exact, but it is wrong, because that bijection sends blocks across *both* summands and they would then overlap the poll. **The seam is an enriched law, not `C.P`**: Austin's polling data is the family of *mixed* clusters — those not wholly original, all-spare included — spanning the two halves, and forgetting it into a bare `C.P` statement would discard what the successor construction consumes, so `enrichedPollingLaw` retains the whole pooled rank-`n` latent array and the clusters alongside the original structure and old latents, with `enrichedPollingLaw_map_fst` recovering `C.P` exactly through `map_restrict_embedding` at the original-vertex embedding. `pollingCond` pins the conditioning concretely — the whole pooled rank-`n` latent array plus the mixed clusters — since an existential factor could be the whole joint object and make the conclusion vacuous. `PooledPollingWitness.mutualCondIndep` is `iCondIndepFun` over the **entire** rank-`n` block family: mutual, not pairwise, which is Austin's actual conclusion and what the #196 battery keeps honest. Needs only the ambient `Countable` assumptions — because the conditional independence comes from the assumed screening contract rather than from a polling argument, the `Fintype S.Srt` hypothesis the fixing-algebra stack carries is not required; rank zero is routed to `nonempty_rankRepresentation_one` with `truncation_zero`, respecting `stepKernel`'s deliberate lack of an `A = ∅` realization theorem
* `Graphon.RelBipartiteRegression` — R4 converse (#107/#196): the **bipartite regression** for the successor contract, a hand-built rank `1 → 2` witness over `digraphSig` whose purpose is to test that `RankSuccessor` is an expressive specification *before* either route is attempted. Each vertex carries an i.i.d. colour on its own fresh singleton coordinate and the edge is the parity, so the diagonal is constantly `false` for free. Three independent things make it a regression rather than a construction: the array law is defined **from the fresh singleton layer alone** and the rank-one coupling as the independent product `bipartiteLaw × rankLatentSource 1`, so `rankTwoCoupling_truncation` compares two separately described couplings and genuinely consumes the source factorization; the rank-two block decoder recovers **both** directed coordinates `X_uv` and `X_vu` as the same parity, exhibiting symmetry as a property of this law rather than of the signature; and `not_indepFun_rankTwoCoupling` is **numerical** — the edge and colour-parity events coincide with probability `1/2` against a product of marginals `1/4`, which a constant edge could not achieve even though it too would be "a function of the colours". `bipartiteSuccessor : RankSuccessor rankOneRep` is the witness itself
* `Graphon.RelIidEdgeRegression` — R4 converse (#107/#196): the **i.i.d.-edge regression** for the successor contract, a hand-built rank `2 → 3` witness over `digraphSig` that tests **staging and recovery** where the bipartite regression tested independence and symmetry. The array is keyed by a coordinate's *support*, which gives symmetry (`X_uv = X_vu`) and the empty diagonal by construction — each is still proved from a support computation, but neither requires a choice of orientation. Two things make it a regression rather than a construction. First, recovery is genuinely staged: at rank three a two-point block is decoded from the latent coordinate at its own support — carried by the rank-three array because `2 < 3` — while at rank two the same blocks are not latent-measurable at all, so the two ranks exercise opposite sides of `lower_recovers`. Second, rank-two screening is a genuine conditional-independence statement: the block reads one coordinate of the edge source and the remainder reads the others plus the whole latent array, so screening follows from **independence**, not from determinism as in the bipartite case. `iidEdgeLaw_edge_eq_half` pins the edge probability at exactly `1/2`, which rules out a *constant* block; that the block is not measurable from the old latents is a separate fact, supplied by the product independence built into the rank-two coupling. The private conditional-independence lemma is stated for abstract σ-algebras rather than for the two coordinates of a product because the ambient measure is a pushforward of a product and the current API only transports conditional independence **backward**: a source-level proof would require a new forward law-transport theorem, whereas transporting the unconditional independence needs no new theorem. `iidEdgeSuccessor : RankSuccessor rankTwoRep` is the witness itself
* `Graphon.RelRankInjectionInvariance` — R4 converse (#107), the isolated proof risk of the pooled-latent extension gate: **joint invariance under arbitrary sortwise self-injections**. `RankRepresentation.invariant` is stated for *finitely supported permutations*, but a pooled object built cheaply through `poolVertexEquiv` needs the joint law invariant under every self-injection; `RankRepresentation.map_prodMap_restrict_self` supplies exactly that, so full mixed pooled invariance later costs no additional mathematics. The route is finite-cylinder extensionality on the **joint** space, which had no machinery before — rank one's joint invariance goes through only because the rank-one latent action is trivial. `rankLatentIndexInj`/`rankLatentReindex` extend the latent action from permutations to injections (only injectivity is used — a support keeps its cardinality); `exists_finSuppPerm_agree_on_finset` matches an injection to a finitely supported permutation on any finite tagged-vertex support; `ext_of_prod_cylinders` is the joint extensionality, rectangles of coordinate cylinders on both factors. **No finiteness/`Fintype` hypothesis beyond `RankRepresentation`'s ambient countability.** Equality is tested on *coordinate* cylinders — finitely many `RelCoord`s and finitely many latent indices — whose combined vertex support is one finite `Finset (Σ s, Vinfinite S s)` and so touches only finitely many sorts; the injection is matched there by extending it on each active sort, taking the identity elsewhere, and maximizing finitely many support bounds. The coarser `restrictFin` cylinder family would instead force a uniform all-sort bound that no self-injection need admit
* `Graphon.RelRankCoding` — R4 converse piece 3 (#107): factor-law coding of the lower-rank factor. **Not** the inductive hypothesis of a working recursion: `RankCoding n → ShellProperty n` is **false**, refuted by Austin's random complete bipartite graph `X_uv = z_u ⊕ z_v` (arXiv:0801.1698 §3.6), where `lowerRankAlgebra 2` is trivial modulo the law but every triangle satisfies `X₁₂ ⊕ X₁₃ ⊕ X₂₃ = 0`, so the exact layers are pairwise but not mutually independent — while a `RankCoding 2` exists because the rank-2 factor law is a point mass. The example separates the true two-set theorem from mutuality, and shows the gap is not closable by coupling: a relatively independent joining over `lowerFactorMap` attaches latents that are conditionally independent of the structure given a trivial factor, whereas a representation needs the hidden colours, correlated with the array yet not recoverable from it. `RankCoding n` represents the rank-`n` factor by latents — a measurable coding map carrying the latent source to the factor law and intertwining the two relabeling actions **almost everywhere**. The a.e. form is forced: `lowerFactorSpaceEquiv σ n` fixes the *image* of `lowerFactorMap n`, not the whole Bool-cube, since it permutes distinct basis indices that name the same event, so the strict version is false already at rank one. `ShellProperty n` is the conclusion the recursion consumes, bundling mutual conditional independence of the exact layers over the rank-`n` supports **with** per-support locality; neither half implies the other, since mutual independence given the whole lower-rank factor permits dependence on all of it rather than only through `boundaryMap A`. `RankCoding.rankOne` is the base case, built from the #140 randomization adapter transported along `rankLatentOneEquiv`; its equivariance clause is genuinely exercised rather than vacuous, because at rank one the latent relabeling is the identity while the factor equivalence is not
* `Graphon.RelFixingAlgebra` — R4 converse piece 2a (#107): the **law-independent** factor-algebra layer — `SortwiseFixing` (the `A`-fixing stabilizer of finitely supported sortwise permutations, closed under `1`/`*`/`⁻¹`/conjugation), the raw `RelStructure.fixingAlgebra` (events invariant under the `A`-fixing group; deliberately *not* "generated by relations inside `A`", which loses hidden vertex information), monotonicity, `fixingAlgebra_empty = invariantAlgebra` (near-definitional), and the **transport equality** `fixingAlgebra_comap_relabel : comap (relabel σ) (fixingAlgebra A) = fixingAlgebra (image σ A)` via stabilizer conjugation — no completions, no law; the conditional-independence theorem is its own later PR
* `Graphon.RelPollingInfrastructure` — R4 (#107): the reusable polling engine, extracted from `RelFixingCondIndep` once the rankwise relative-independence argument became its second consumer. Three public declarations: the tail engine `condExp_ae_eq_condExp_of_comap_eq` (a measure-preserving `T` fixing `f` a.e. and pulling `m₁` back to `m₂ ≤ m₁` forces `μ[f|m₁] =ᵐ μ[f|m₂]`), `InfiniteRelExchangeableLaw.measurePreserving_relabel`, and `InfiniteRelExchangeableLaw.relabel_preimage_ae_eq_of_fixingAlgebra`. The `L²` squeeze and the conditional-expectation transport along `comap` stay private — they are the proof of the tail engine, not its interface
* `Graphon.RelFixingCondIndep` — R4 converse piece 2b (#107): the headline `InfiniteRelExchangeableLaw.condIndep_fixingAlgebra` — for **every** exchangeable law, with no dissociation hypothesis, `CondIndep (fixingAlgebra (A ∩ B)) (fixingAlgebra A) (fixingAlgebra B) (fixingAlgebra_le _) M.law` (Austin arXiv:0801.1698 Lemma 3.11 / Proposition 3.12; Kallenberg Lemma 7.6 as the closest precursor — Lemmas 7.18–7.19 there belong to the later realization recursion). The private machinery: the `L²`-energy squeeze, measure-preserving-map transport of conditional expectation, and the tail-property engine (a.e.-fixing + comap-pullback ⟹ equal conditional expectations); the upgrade of `fixingAlgebra A`-invariance from finitely supported to *arbitrary* sortwise permutations fixing `A`, modulo the law; the poll geometry (deep copies of `B \ A` laid out along a two-sided `ℤ`-orbit — a unilateral block shift is not a bijection — moved by a single residue-wise permutation fixing `A`); the tail **joins** `⨆_{m ≥ n} fixingAlgebra ((A ∩ B) ∪ Q m)`, whose intersection is `fixingAlgebra (A ∩ B)` as a *raw* σ-algebra equality; and the reduction `E[f | fixingAlgebra B] =ᵐ E[f | fixingAlgebra (A ∩ B)]` that the theorem factorizes through. Everything but the headline is `private`
* `Graphon.SeparableFactor` — R4 converse piece 3 (#107), the generic signature-free toolkit for the coherent factor realization; nothing here mentions relational structures, and the whole module is a Mathlib-upstream candidate (#24). `Measure.MeasureDense.exists_generateFrom_ae_eq_of_ne_top` upgrades a measure-dense family for a trimmed measure from *approximation* to honest **a.e. representatives** (`∀ E, MeasurableSet[m] E → ∃ E', MeasurableSet[generateFrom G] E' ∧ E' =ᵐ[μ] E`) by summable symmetric-difference approximation plus Borel–Cantelli, with no countability hypothesis — countability matters only when the family is turned into a factor space — and `exists_generateFrom_ae_eq` is its finite-measure corollary. `measure_symmDiff_threshold_le` is the threshold estimate `ν (E ∆ {x | 1/2 < f x}) ≤ 2‖1_E - f‖₁`, the bridge from an `L¹`-dense family of *functions* to a measure-dense family of *sets*. `MeasurableSpace.comap_mapNatBool` is the missing companion to Mathlib's `measurable_mapNatBool`: a countably generated σ-algebra is *literally* the pullback of the Cantor-space σ-algebra along `mapNatBool`, needing no `SeparatesPoints` since injectivity is irrelevant to the pullback identity. Throughout, the mod-null statements are deliberately eventwise rather than equalities of σ-algebras "modulo null sets", which would force a `Measure.trim`/`Measure.completion` choice at every use site and create diamonds between them
* `Graphon.RelCoherentBasis` — R4 converse piece 3 (#107): the **interface** for a simultaneous, coherent family of factors for the fixing σ-algebras, defined but deliberately not constructed. `CoherentBasis` carries one global countable index type whose indices are anchored at finite tagged vertex sets, closed under finite Boolean operations (a countable set ring), acted on by finitely supported relabelings with exact anchor and event transport, and measure-dense over each `A`. The derived factor at `A` maps into `BasisIndex A → Bool` — a *varying* countable index rather than `ℕ → Bool`, which is what keeps the inclusion for `C ⊆ A` literal, the factor projection an ordinary coordinate restriction, and its cocycle law definitional; `mapNatBool` loses exactly this, since its generating sequence is typeclass-chosen. `exists_comap_factorMap_ae_eq` is the payoff: every `fixingAlgebra A`-event has an a.e. representative in the factor's pullback
* `Graphon.RelBasisSyntax` — R4 converse piece 3 (#107): the Boolean **syntax** layer for a coherent basis. `BasisExpr` is the free `⊥`/complement/intersection syntax over an atom type, with `anchorOf` and `eval` computed by recursion and `act` acting on the tree. Syntax rather than a family of events closed under the operations, for two reasons recorded in the module docstring: the anchor is not determined by the event, so an event-indexed family would have to *choose* one and then make that choice equivariant; and closing a family of events forces representative choices that make `act_one` and `act_mul` hold only up to that choice. Here `act_one`, `act_mul`, `anchorOf_act`, and `eval_act` all follow by structural induction from the atom-level laws, and the anchor-as-union convention on `inter` is what keeps the indices anchored inside `A` closed under the operations
* `Graphon.RelBasisSaturation` — R4 converse piece 3 (#107): the saturated atom family. An atom is a seed event anchored at a finite vertex set together with a finitely supported relabeling of it; the relabeling action is **left multiplication in that coordinate**, which turns the two action laws into literal group laws in the finitely supported subgroup (`act_one` is `one_mul`, `act_mul` is `mul_assoc`), the anchor law into `Finset.image_image`, and the event law into `relabel_preimage_relabel_preimage` — the orientation matching because `relabel` is contravariant. Saturation lives in the index rather than being imposed afterwards, so the family is closed under the action by construction, with no orbit representatives and nothing to make equivariant after the fact. `SeedData` keeps the seeds abstract, so none of the structural laws depend on how they are produced; the seeds themselves come from separability of the law, and the module closes with **`InfiniteRelExchangeableLaw.nonempty_coherentBasis`** — every exchangeable law has a coherent basis, under `[Fintype S.Srt]` and `[Countable S.Rel]`, with no `NoNullary`. Stated as `Nonempty` rather than registered as an instance, since a coherent basis is chosen data and an instance would make later independent choices behave like typeclass diamonds
* `Graphon.RelFactorLaws` — R4 converse piece 3 (#107): the boundary/exact splitting of the coherent factors and their laws. `BoundaryIndex A` collects indices anchored *properly* inside `A` and `ExactIndex A` the exact-anchor layer, giving the measurable equivalence `FactorSpace A ≃ᵐ BoundarySpace A × ExactSpace A`. This partitions *coordinates by anchor*, not information: anchors are not minimal, so an expression anchored at `A` may still name an event measurable over a proper subset. This is the shape the AHK recursion needs — one kernel per finite `A`, conditioned on the whole proper-subset boundary and recursing by `|A|`: kernels for every pair `C ⊆ A` would be redundant and force compatibility between different a.e. versions of conditional distributions, while a linear chain would impose an arbitrary ordering and let the value at `A` depend on sets incomparable to it, breaking subset-locality. `factorLaw` / `boundaryLaw` / `exactLaw` are the pushforwards, with projection consistency along the sub-index inclusions and relabeling invariance from exchangeability — the first place in this layer where the law is used. `measurable_exactMap_fixingAlgebra` sharpens ambient measurability of the exact layer to measurability for `fixingAlgebra A`, which any argument bundling exact-layer events over a support needs
* `Graphon.RelStepKernel` — R4 converse piece 3 (#107): **one kernel per finite `A`**, `stepKernel A : Kernel (BoundarySpace A) (ExactSpace A)`, the conditional distribution of the exact-anchor layer given the whole proper-subset boundary — not one kernel per pair `C ⊆ A`, and not a chain. Built as `condDistrib`, whose standard-Borel hypothesis is exactly what the factor-space packaging supplies. Central identities: the disintegration `boundaryLaw A ⊗ₘ stepKernel A = M.law.map (boundaryMap A, exactMap A)`, marginal recovery `stepKernel A ∘ₘ boundaryLaw A = exactLaw A`, and the same read through `factorSpaceProdEquiv`. Valid for an arbitrary exchangeable law; the `A = ∅` base case is deliberately absent, since its determinism uses dissociation and belongs to the later realization layer
* `Graphon.RelRankAlgebra` — R4 converse piece 3 (#107): the **lower-rank conditioning algebra** `lowerRankAlgebra n = ⨆ A, ⨆ (_ : A.card < n), fixingAlgebra A` and its order theory — monotone in the rank bound, below the ambient algebra, containing each low-rank fixing algebra, `⊥` at rank `0`, and `invariantAlgebra` at rank `1` (the recursion's base, and the reason no `NoNullary` hypothesis is needed). Plus `comap_relabel_lowerRankAlgebra`, invariance under an **arbitrary** sortwise permutation family — relabelings displacing infinitely many vertices arise naturally downstream, so the finite-support hypothesis would be too weak — and `card_inter_lt_of_ne`, that distinct supports of equal rank meet in strictly lower rank. Law-free throughout
* `Graphon.RelLowerFactor` — R4 converse piece 3 (#107): the **structural lower-rank factor**, the object the rank recursion conditions on. `lowerFactorMap n` reads the coherent-basis coordinates whose anchor has cardinality `< n` into the standard Borel `LowerFactorSpace n`. It is stated about the *factor*, never about latents: a latent normally carries randomness beyond the factor it represents — already `1_{U < p}` generates strictly less than `U` — so a σ-algebra generated by latents is typically strictly larger. Generation is `comap (lowerFactorMap n) inferInstance ≤ lowerRankAlgebra n` together with an **eventwise** converse; no raw equality is asserted or supplied, the available converse being modulo `M.law`. The converse is proved support by support through `lowerToFactorProjection`, which exhibits `factorMap A` as a coordinate restriction whenever `A.card < n`, and the containments are joined inside `eventuallyMeasurableSpace` — already a σ-algebra, so the completion does the closing and no family of a.e. witnesses is ever chosen simultaneously through the `iSup`. `lowerIndexEquiv` gives `FinSuppPerm` equivariance as automorphisms of one fixed type (rank is preserved because anchors transport by an injective image map), so the action laws are honest equalities of equivalences with no dependent transport, and they commute with rank nesting definitionally. Rank `0` is `⊥` on the nose; rank `1` is the recursion's base, on the original law, with no augmented space and no coupling
* `Graphon.RelRankSuccessor` — R4 converse piece 3 (#107), unit 1 of the rank transition `n → n+1`: the law-free structural split of the factor space into everything below rank `n` and the layer at rank exactly `n`. **The layer is a Bool-cube, not a dependent product**, and that is a load-bearing choice: `Π A : RankSupport S n, ExactSpace A` would force every downstream conditional law to be a kernel into a dependent product, and Mathlib has no countable dependent product of kernels — there is no `Kernel.pi`, the only `Π`-valued kernels being the Ionescu–Tulcea trajectory kernels, which are ℕ-indexed chains whose source is the history rather than a fixed common parameter. Since `ExactSpace A = ExactIndex A → Bool` the dependent product is already a Bool-cube on `{i // (anchor i).card = n}`, so `RankLayerIndex`/`RankLayerSpace`/`rankLayerMap` are defined directly that way, with `sigmaExactIndexEquiv` recording the bridge to the per-support view and `rankLayerMap_sigmaExactIndexEquiv` identifying each block with `exactMap A`. Downstream this means a layer conditional law is an ordinary `condDistrib` into a standard Borel space and mutual conditional independence supplies the finite products that finite-cylinder extensionality consumes — no product kernel anywhere. `lowerIndexSuccEquiv`/`lowerFactorSpaceSuccEquiv` give the split `LowerFactorSpace (n+1) ≃ᵐ LowerFactorSpace n × RankLayerSpace n`; `lowerToBoundaryProjection` reads the boundary at each rank-`n` support, definitionally compatible with `boundaryMap`. The relabeling actions `rankSupportEquiv`/`rankLayerIndexEquiv`/`rankLayerSpaceEquiv` are automorphisms of fixed types, so the action laws need no dependent transport; the square `lowerIndexSuccEquiv_rankLayerIndexEquiv` against the successor split is **not** definitional, since the split branches on `card < n` and the two sides' branch conditions agree only after transporting anchor cardinality through the image map. The **space-level** successor square `lowerFactorSpaceSuccEquiv_lowerFactorSpaceEquiv` *is* definitional, escaping the case split because it is built from `lowerIndexSuccEquiv.symm`, a `Sum.elim` that computes on the constructors. Per-support API for units 2 and 3: `rankLayerToExactProjection` (with `rankLayerToExactProjection_rankLayerMap` definitional), and the naturality squares for it, for `lowerToBoundaryProjection`, and for the support/exact bridge — all definitional, so per-support kernel identification and coherent randomization inherit them without transport bookkeeping
* `Graphon.RelRankLatents` — R4 converse piece 3 (#107), the latent-side prerequisite for the coupled rank induction: `RankLatentIndex n` is the finite tagged supports of cardinality `< n` (so it contains `∅` exactly when `0 < n`), `RankLatentSpace n` is their real-valued cube, and `rankLatentSource n` supplies one independent `uniform01` coordinate per support. Rank nesting and its projection cocycle are definitional. `rankLatentIndexEquiv`/`rankLatentRelabel` give the genuine finitely-supported sortwise action and preserve the source exactly. At rank one, `rankLatentOneEquiv` is evaluation at the unique empty-support coordinate and pushes the source to `uniform01`. The successor measurable equivalence splits the source into the old rank-`n` latents and a fresh `RankSupport S n → ℝ` layer, with both the source-product identity and the relabeling square; unlike `LowerFactorSpace`, this is an `ℝ`-cube indexed by tagged supports, related to the Boolean coherent factor only later through a rank coding
* `Graphon.RelRankOneCondIndep` — R4 converse piece 3 (#107): the **rank-one mutual conditional independence**, `iCondIndepFun (fun v => exactMap {v}) invariantAlgebra M.law` — the singleton exact-anchor layers are mutually, not merely pairwise, conditionally independent given the invariant σ-algebra, for an arbitrary exchangeable law with no dissociation and no `NoNullary`. Proved entirely from the two-set `condIndep_fixingAlgebra` by peeling one vertex at a time: the accumulated events bundle into a single `fixingAlgebra s`-event by monotonicity, `{v} ∩ s = ∅`, so the two-set theorem conditions on `fixingAlgebra ∅ = invariantAlgebra` — the same algebra at every stage — and the products compose against the induction hypothesis. The peel is available *only* at rank one: for supports of rank `n > 1` the peeled support need not be disjoint from the accumulated union, and where it is not, that stage conditions on a larger algebra — and conditional independence is not preserved under enlarging the conditioning. A positive-rank intersection is not inevitable for every family, but it is possible, which is enough to break the induction. So no de Finetti representation, no mixing measure, and no identification of a mixing measure with an invariant conditional distribution is needed here
* `Graphon.DigraphMaps` — the minimal `Digraph.comap` pullback API for Mathlib's `Digraph` (mirroring `SimpleGraph.comap`; a Mathlib-upstream candidate tracked on #24), used by the D2 directed-law bridge
* `Graphon.InfiniteDigraphLaw` — Directed umbrella (#84) D2 (#86): the `PMF`-based finite directed law `ExchangeableDigraphLaw` (consistent under `Digraph.comap`), the finite bridge `digraphLawEquiv : ExchangeableDigraphLaw ≃ RelExchangeableLaw digraphSig` (via `finiteDigraphEquiv` + `PMF.toMeasure`/`Measure.toPMF`), and the headline `exchangeableDigraphLawEquiv : ExchangeableDigraphLaw ≃ InfiniteExchangeableDigraphLaw` composing with R2c — measurable structure stays on the relational carrier
* `Graphon.ExchangeableLawBlueprint` — annotation-only blueprint wrappers for the R2c relational (`relExchangeableLawEquiv`) and D2 directed (`exchangeableDigraphLawEquiv`) equivalences, keeping `Architect` out of the reusable foundational modules
* `Graphon.SamplerSources` — generic i.i.d. random sources (`uniform01`, `iidVertexSource`, `iidUniformSource`) shared by the graph and directed samplers
* `Graphon.Digraphon` — Directed umbrella (#84) D3a (#87): the five-component CAF `Digraphon` (four reciprocal-edge pair kernels + Bool loop, a.e. probability-vector + transpose law) with `ext`; measurable representatives; the transpose-symmetrized `pairSym`; and the **everywhere-valid 3-simplex representative** `simplexRep` (measurable, nonneg/sum-one/transpose-compatible everywhere, a.e.-equal to `pairProb`) — the prerequisite for the D3b sampler; no random sources yet
* `Graphon.DigraphSampler` — Directed umbrella (#84) D3b (#87): the per-pair four-state distribution `Digraphon.pairPMF`, the one-uniform categorical map `catOutcome` with its **exact four-state law** `uniform01_map_catOutcome`; the explicit finite/infinite digraph samplers (`sampleAdj` in the natural-number order, `sampleInfinite`, `sampleFinite`); the **exact finite-event product formula** over an arbitrary injective labeling; the sampled law (`sampleRelLaw` / `sampleDigraphLaw`) with the infinite-law identification through `exchangeableDigraphLawEquiv`; exchangeability and dissociation
* `Graphon.DigraphonConstructors` — Directed umbrella (#84) D3c (#87): the special-family digraphon constructors — the generic pointwise builder `Digraphon.ofFun`, the ordinary-graphon embedding `ofGraphon` (reciprocal edges fully correlated), the tournament digraphon `ofTournament` (exactly one direction per pair), and the asymmetric-kernel digraphon `ofKernel` (independent directions, all four products present) — each with its a.e. pair-kernel identification
* `Graphon.DigraphSamplerFamilies` — Directed umbrella (#84) D3c headlines (#87): the sampler laws of the special families — the embedded ordinary graphon samples exactly the undirected `W`-random graph (`map_sampleFinite_ofGraphon`, pushforward of `samplePMF` under the symmetric loopless embedding), the tournament digraphon samples an almost-sure tournament (`ofTournament_sample_isTournament`), and the asymmetric-kernel sample draws its two directions independently (`sampleEventIntegrand_ofKernel_ae`)
* `Graphon.RelationalTopology` — Generic AHK program R1b (#104): the Boolean-product topology / σ-algebra on `RelStructure` — compact/Polish/standard-Borel instances, measurability of the finite restrictions, the cylinder π-system `cylinders` generating the product σ-algebra (`generateFrom_cylinders_eq`; = Borel under the countability giving Polish), and finite-restriction measure extensionality (`ext_of_map_restrictFin`); no projective extension (that is R2)
* `Graphon.InverseCounting` — Inverse counting lemma, convergence equivalence
* `Graphon.Convergence` — Top-level convergence characterization

## Experimental

* `Graphon.Operations` — Pointwise product (direct sum and operator product are future work)
* `Graphon.Operator` — Kernel operator pointwise definition (full L² API is future work)
* `Graphon.Sampling` — W-random graph distribution (`sampleMass`) and expected edge density (concentration is proved in the `Sampling*` modules above, culminating in `Graphon.SamplingLemma`)
-/