feat: rank-one mutual conditional independence (#107)

Graphon.lean

@@ -24,6 +24,7 @@ import Graphon.KernelRandomization
 import Graphon.RelFixingAlgebra
 import Graphon.RelRankAlgebra
 import Graphon.RelLowerFactor
+import Graphon.RelRankOneCondIndep
 import Graphon.RelPollingInfrastructure
 import Graphon.RelFixingCondIndep
 import Graphon.SeparableFactor
@@ -205,10 +206,11 @@ in Lean 4 using Mathlib.
 * `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
+* `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.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/RelFactorLaws.lean

@@ -155,6 +155,14 @@ theorem measurable_exactMap (A : Finset (Σ s : S.Srt, Vinfinite S s)) :
     Measurable (B.exactMap A) :=
   ((B.factorSpaceProdEquiv A).measurable.comp (B.measurable_factorMap' A)).snd
 
+open scoped Classical in
+/-- The exact-anchor layer at `A` is measurable for `fixingAlgebra A`, not merely for the
+ambient algebra. General factor API rather than a rank-one fact: any argument that bundles
+exact-layer events over a support needs this sharpening of `measurable_exactMap`. -/
+theorem measurable_exactMap_fixingAlgebra (A : Finset (Σ s : S.Srt, Vinfinite S s)) :
+    Measurable[RelStructure.fixingAlgebra A] (B.exactMap A) :=
+  ((B.factorSpaceProdEquiv A).measurable.comp (B.measurable_factorMap A)).snd
+
 /-! ### Relabeling the two layers -/
 
 open scoped Classical in

Graphon/RelRankOneCondIndep.lean

@@ -0,0 +1,112 @@
+/-
+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.RelFixingCondIndep
+import Graphon.RelFactorLaws
+
+/-!
+# The rank-one mutual conditional independence (R4 converse piece 3, #107)
+
+The rank-one instance of the target: the exact-anchor layers at the *singletons* are **mutually**
+conditionally independent given the invariant σ-algebra,
+
+`iCondIndepFun (fun v => exactMap {v}) invariantAlgebra M.law`.
+
+At rank one the conditioning factor is `lowerRankAlgebra 1 = invariantAlgebra`, so this is the
+conditional-independence half of the multi-sorted de Finetti statement, for an arbitrary
+exchangeable law — no dissociation, no `NoNullary`. Sort-orbit equality of the conditional
+kernels is the other half and is deliberately absent here; it is provable separately from
+exchangeability and uniqueness of conditional distributions.
+
+## Why no de Finetti machinery is needed
+
+Mutual conditional independence does not follow from pairwise conditional independence in
+general, and this is exactly the higher-rank obstruction recorded in `Graphon.RelRankAlgebra`.
+At rank one it can nevertheless be obtained from the *two-set* theorem
+`InfiniteRelExchangeableLaw.condIndep_fixingAlgebra` by peeling one vertex at a time:
+
+* peel a vertex `v` off the finite family;
+* bundle the remaining events into a single event measurable for `fixingAlgebra s`, where `s` is
+  the set of remaining vertices — legitimate because `fixingAlgebra` is monotone;
+* `{v} ∩ s = ∅`, so the two-set theorem conditions on `fixingAlgebra ∅ = invariantAlgebra`,
+  which is the conditioning algebra we want and does not change as the peel proceeds;
+* multiply by the induction hypothesis.
+
+The step that fails at higher rank is the third: for supports of rank `n > 1` the peeled support
+*need not be disjoint* from the accumulated union, and where it is not, the two-set theorem
+conditions on a different — and larger — algebra at that stage. Since conditional independence
+is not preserved under enlarging the conditioning, the stages no longer compose. A positive-rank
+intersection is not inevitable for every family, but it is possible, and that is enough to break
+the induction. At rank one the remaining union stays disjoint from the peeled singleton for
+*every* family, so the conditioning algebra is the same throughout and the products compose.
+
+Consequently the rank-one case needs no de Finetti representation, no mixing measure, and no
+identification of a mixing measure with an invariant conditional distribution.
+-/
+
+open MeasureTheory MeasurableSpace ProbabilityTheory
+
+namespace RelSignature
+
+namespace CoherentBasis
+
+universe u
+
+variable {S : RelSignature.{u}} {M : InfiniteRelExchangeableLaw S} (B : CoherentBasis M)
+
+open scoped Classical in
+/-- **Mutual conditional independence of the singleton exact layers given the invariant
+σ-algebra** — the rank-one instance of the rankwise theorem, for an arbitrary exchangeable law.
+
+Stated over the whole vertex index rather than for a fixed finite family: `iCondIndepFun` already
+quantifies over finite subfamilies, so finite families are a corollary. -/
+theorem iCondIndepFun_exactMap_singleton [Fintype S.Srt] [Countable S.Rel] :
+    iCondIndepFun RelStructure.invariantAlgebra (RelStructure.invariantAlgebra_le (S := S))
+      (fun v : Σ s : S.Srt, Vinfinite S s => B.exactMap {v})
+      (M.law : Measure (RelStructure S (Vinfinite S))) := by
+  classical
+  haveI : IsProbabilityMeasure (M.law : Measure (RelStructure S (Vinfinite S))) := M.law.2
+  rw [iCondIndepFun_iff_condExp_inter_preimage_eq_mul _ _
+    fun v => B.measurable_exactMap ({v} : Finset (Σ s : S.Srt, Vinfinite S s))]
+  intro T sets
+  induction T using Finset.induction_on with
+  | empty =>
+      intro _
+      simp only [Finset.notMem_empty, Set.iInter_of_empty, Set.iInter_univ, Finset.prod_empty,
+        Set.indicator_univ]
+      rw [condExp_const (μ := (M.law : Measure (RelStructure S (Vinfinite S))))
+        RelStructure.invariantAlgebra_le (1 : ℝ)]
+      rfl
+  | insert v s hvs ih =>
+      intro hsets
+      have ihs := ih fun i hi => hsets i (Finset.mem_insert_of_mem hi)
+      -- the accumulated event is measurable for the fixing algebra of the accumulated support
+      have hE : MeasurableSet[RelStructure.fixingAlgebra s]
+          (⋂ i ∈ s, B.exactMap ({i} : Finset (Σ s : S.Srt, Vinfinite S s)) ⁻¹' sets i) := by
+        refine Finset.measurableSet_biInter s fun i hi => ?_
+        exact RelStructure.fixingAlgebra_mono (Finset.singleton_subset_iff.mpr hi) _
+          (B.measurable_exactMap_fixingAlgebra _ (hsets i (Finset.mem_insert_of_mem hi)))
+      have hF : MeasurableSet[RelStructure.fixingAlgebra
+          ({v} : Finset (Σ s : S.Srt, Vinfinite S s))]
+          (B.exactMap ({v} : Finset (Σ s : S.Srt, Vinfinite S s)) ⁻¹' sets v) :=
+        B.measurable_exactMap_fixingAlgebra _ (hsets v (Finset.mem_insert_self v s))
+      -- the peeled singleton is disjoint from the accumulated support
+      have hinter : ({v} : Finset (Σ s : S.Srt, Vinfinite S s)) ∩ s = ∅ := by
+        ext x
+        simp only [Finset.mem_inter, Finset.mem_singleton, Finset.notMem_empty, iff_false, not_and]
+        rintro rfl
+        exact hvs
+      have hci := M.condIndep_fixingAlgebra ({v} : Finset (Σ s : S.Srt, Vinfinite S s)) s
+      rw [condIndep_iff _ _ _ _
+        (RelStructure.fixingAlgebra_le ({v} : Finset (Σ s : S.Srt, Vinfinite S s)))
+        (RelStructure.fixingAlgebra_le s)] at hci
+      have key := hci _ _ hF hE
+      rw [hinter, RelStructure.fixingAlgebra_empty] at key
+      rw [Finset.set_biInter_insert, Finset.prod_insert hvs]
+      exact key.trans (Filter.EventuallyEq.mul (Filter.EventuallyEq.refl _ _) ihs)
+
+end CoherentBasis
+
+end RelSignature

scripts/axiom_audit.lean

@@ -230,3 +230,5 @@ custom axioms. Target list and policy: `scripts/check_census_and_axioms.py`
 #print axioms RelSignature.CoherentBasis.lowerIndexEquiv_mul
 #print axioms RelSignature.CoherentBasis.lowerFactorSpaceEquiv_mul
 #print axioms RelSignature.CoherentBasis.lowerFactorProjection_lowerFactorSpaceEquiv
+#print axioms RelSignature.CoherentBasis.measurable_exactMap_fixingAlgebra
+#print axioms RelSignature.CoherentBasis.iCondIndepFun_exactMap_singleton

scripts/check_census_and_axioms.py

@@ -213,6 +213,8 @@
     "RelSignature.CoherentBasis.lowerIndexEquiv_mul",
     "RelSignature.CoherentBasis.lowerFactorSpaceEquiv_mul",
     "RelSignature.CoherentBasis.lowerFactorProjection_lowerFactorSpaceEquiv",
+    "RelSignature.CoherentBasis.measurable_exactMap_fixingAlgebra",
+    "RelSignature.CoherentBasis.iCondIndepFun_exactMap_singleton",
     "RelSignature.condExp_ae_eq_condExp_of_comap_eq",
     "RelSignature.InfiniteRelExchangeableLaw.measurePreserving_relabel",
     "RelSignature.InfiniteRelExchangeableLaw.relabel_preimage_ae_eq_of_fixingAlgebra",