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 comaps), 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 RelCoords 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)