The lower-rank conditioning algebra (#107)

Graphon.lean

@@ -22,6 +22,7 @@ import Graphon.RelKernelEvaluator
 import Graphon.RelKernelSampler
 import Graphon.KernelRandomization
 import Graphon.RelFixingAlgebra
+import Graphon.RelRankAlgebra
 import Graphon.RelPollingInfrastructure
 import Graphon.RelFixingCondIndep
 import Graphon.SeparableFactor
@@ -205,6 +206,7 @@ in Lean 4 using Mathlib.
 * `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.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.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/RelRankAlgebra.lean

@@ -0,0 +1,167 @@
+/-
+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.RelFixingAlgebra
+
+/-!
+# The lower-rank conditioning algebra (R4 converse piece 3, #107)
+
+The conditioning factor for the rankwise relative-independence theorem: the join of the fixing
+σ-algebras of *all* vertex sets of rank below `n`,
+
+`lowerRankAlgebra n = ⨆ A, ⨆ (_ : A.card < n), fixingAlgebra A`.
+
+## Why a single global factor
+
+The target theorem is that, for a finite family `F` of **distinct** vertex sets of rank exactly
+`n`, the exact-anchor layers at those sets are **mutually** — not merely pairwise —
+conditionally independent given everything of lower rank:
+
+`E[∏ A ∈ F, g A ∘ exactMap A | lowerRankAlgebra n] =ᵐ ∏ A ∈ F, E[g A ∘ exactMap A | lowerRankAlgebra n]`
+
+The conditioning must be this one global algebra, not a chain and not a separate conditioning
+per pair. Two things go wrong otherwise:
+
+* pairwise conditional independence does **not** imply mutual conditional independence, so the
+  finite-product identity cannot be assembled from two-set statements; and
+* conditional independence is **not** preserved when the conditioning algebra is enlarged, so a
+  statement proved against one conditioning factor cannot simply be re-read against another.
+
+`RelSignature.InfiniteRelExchangeableLaw.condIndep_fixingAlgebra` therefore serves here as
+infrastructure and as a regression check on the two-set case, not as the proof engine. The
+missing finite-family statement is analogous to Austin's Proposition 3.12 (arXiv:0801.1698); its
+proof belongs to the downstream rankwise coupling/induction layer and is deliberately not fixed
+here.
+
+This file is law-free: it defines the conditioning factor and its order theory only.
+
+## Contents
+
+* `RelStructure.lowerRankAlgebra` — the conditioning factor, with `_le` (below the ambient
+  algebra), `_mono` (monotone in the rank bound), `fixingAlgebra_le_lowerRankAlgebra` (each
+  low-rank factor sits inside it), and the degenerate values at ranks `0` and `1`.
+-/
+
+open MeasureTheory
+
+namespace RelSignature
+
+variable {S : RelSignature}
+
+/-- **The lower-rank conditioning algebra**: the join of the fixing σ-algebras of all vertex
+sets of cardinality strictly below `n`. -/
+@[implicit_reducible]
+noncomputable def RelStructure.lowerRankAlgebra (n : ℕ) :
+    MeasurableSpace (RelStructure S (Vinfinite S)) :=
+  ⨆ A : Finset (Σ s : S.Srt, Vinfinite S s), ⨆ _ : A.card < n, RelStructure.fixingAlgebra A
+
+theorem RelStructure.lowerRankAlgebra_le (n : ℕ) :
+    RelStructure.lowerRankAlgebra (S := S) n ≤
+      (inferInstance : MeasurableSpace (RelStructure S (Vinfinite S))) :=
+  iSup₂_le fun A _ => RelStructure.fixingAlgebra_le A
+
+/-- Each low-rank fixing algebra sits inside the conditioning factor. -/
+theorem RelStructure.fixingAlgebra_le_lowerRankAlgebra
+    {A : Finset (Σ s : S.Srt, Vinfinite S s)} {n : ℕ} (h : A.card < n) :
+    RelStructure.fixingAlgebra A ≤ RelStructure.lowerRankAlgebra (S := S) n :=
+  le_iSup₂_of_le A h le_rfl
+
+/-- **Monotone in the rank bound**: a larger bound admits more generators. -/
+theorem RelStructure.lowerRankAlgebra_mono : Monotone (RelStructure.lowerRankAlgebra (S := S)) :=
+  fun _ _ hmn => iSup₂_le fun _ hA =>
+    RelStructure.fixingAlgebra_le_lowerRankAlgebra (lt_of_lt_of_le hA hmn)
+
+/-- At rank bound `0` there are no generators. -/
+theorem RelStructure.lowerRankAlgebra_zero :
+    RelStructure.lowerRankAlgebra (S := S) 0 = ⊥ := by
+  refine le_antisymm (iSup₂_le fun A hA => absurd hA (by omega)) bot_le
+
+/-- At rank bound `1` the only generator is the empty set, so the conditioning factor is the
+invariant σ-algebra — the factor that carries whatever global information the law has. This is
+the base of the recursion, and the reason no `NoNullary` hypothesis is needed. -/
+theorem RelStructure.lowerRankAlgebra_one :
+    RelStructure.lowerRankAlgebra (S := S) 1 = RelStructure.invariantAlgebra := by
+  refine le_antisymm (iSup₂_le fun A hA => ?_) ?_
+  · rw [← RelStructure.fixingAlgebra_empty]
+    have hA0 : A = ∅ := Finset.card_eq_zero.mp (by omega)
+    subst hA0
+    exact le_rfl
+  · rw [← RelStructure.fixingAlgebra_empty]
+    exact RelStructure.fixingAlgebra_le_lowerRankAlgebra (by simp)
+
+/-! ### Invariance under relabeling -/
+
+open scoped Classical in
+private theorem sigmaMap_injective (σ : ∀ _ : S.Srt, Equiv.Perm ℕ) :
+    Function.Injective (Sigma.map id fun s => ⇑(σ s) :
+      (Σ s : S.Srt, Vinfinite S s) → Σ s : S.Srt, Vinfinite S s) := by
+  have hinv : Function.LeftInverse
+      (Sigma.map id fun s => ⇑(σ s)⁻¹ :
+        (Σ s : S.Srt, Vinfinite S s) → Σ s : S.Srt, Vinfinite S s)
+      (Sigma.map id fun s => ⇑(σ s)) := by
+    rintro ⟨s, x⟩
+    show (⟨s, (σ s)⁻¹ (σ s x)⟩ : Σ s : S.Srt, Vinfinite S s) = ⟨s, x⟩
+    rw [show (σ s)⁻¹ (σ s x) = x from (σ s).symm_apply_apply x]
+  exact hinv.injective
+
+open scoped Classical in
+private theorem image_image_inv_rank (σ : ∀ _ : S.Srt, Equiv.Perm ℕ)
+    (A : Finset (Σ s : S.Srt, Vinfinite S s)) :
+    (A.image (Sigma.map id fun s => ⇑(σ s)⁻¹)).image
+      (Sigma.map id fun s => ⇑(σ s)) = A := by
+  rw [Finset.image_image]
+  refine (Finset.image_congr fun v _ => ?_).trans A.image_id
+  obtain ⟨s, x⟩ := v
+  show (⟨s, σ s ((σ s)⁻¹ x)⟩ : Σ s : S.Srt, Vinfinite S s) = ⟨s, x⟩
+  rw [show σ s ((σ s)⁻¹ x) = x from (σ s).apply_symm_apply x]
+
+open scoped Classical in
+/-- **The conditioning factor is relabeling invariant**, for an **arbitrary** sortwise
+permutation family under finitely many sorts — not merely a finitely supported one.
+
+The generality is essential rather than cosmetic. Relabelings that displace infinitely many
+vertices arise naturally in the polling arguments this factor is built for — a map that shifts a
+block at every slot is not finitely supported — and the finite-support transport is simply
+unavailable for them. Since the proof needs nothing beyond each `σ s` being an `Equiv`, the
+hypothesis should not be narrowed.
+
+Any such relabeling permutes the vertex sets of each rank, so it permutes the generators of
+`lowerRankAlgebra n` among themselves. -/
+theorem RelStructure.comap_relabel_lowerRankAlgebra [Fintype S.Srt]
+    (σ : ∀ _ : S.Srt, Equiv.Perm ℕ) (n : ℕ) :
+    MeasurableSpace.comap (RelStructure.relabel σ)
+        (RelStructure.lowerRankAlgebra (S := S) n) =
+      RelStructure.lowerRankAlgebra n := by
+  classical
+  rw [RelStructure.lowerRankAlgebra]
+  simp_rw [MeasurableSpace.comap_iSup,
+    RelStructure.fixingAlgebra_comap_relabel_of_fintype σ]
+  refine le_antisymm (iSup₂_le fun A hA => ?_) (iSup₂_le fun A hA => ?_)
+  · exact le_iSup₂_of_le (A.image (Sigma.map id fun s => ⇑(σ s)))
+      (by rwa [Finset.card_image_of_injective _ (sigmaMap_injective σ)]) le_rfl
+  · refine le_iSup₂_of_le (A.image (Sigma.map id fun s => ⇑(σ s)⁻¹))
+      (by rwa [Finset.card_image_of_injective _ (sigmaMap_injective fun s => (σ s)⁻¹)])
+      (le_of_eq ?_)
+    rw [image_image_inv_rank σ A]
+
+/-! ### The rank bridge -/
+
+open scoped Classical in
+/-- **Distinct supports of the same rank meet in lower rank.** This is the exact bridge into
+`lowerRankAlgebra`: in the peel argument every `C_A = A ∩ A₀` is a generator of the conditioning
+factor, because `A` and `A₀` are distinct sets of the same cardinality. -/
+theorem card_inter_lt_of_ne {A A₀ : Finset (Σ s : S.Srt, Vinfinite S s)} {n : ℕ}
+    (hA : A.card = n) (hA₀ : A₀.card = n) (hne : A ≠ A₀) : (A ∩ A₀).card < n := by
+  classical
+  have hle : (A ∩ A₀).card ≤ n := hA ▸ Finset.card_le_card Finset.inter_subset_left
+  rcases lt_or_eq_of_le hle with h | h
+  · exact h
+  · exfalso
+    have h1 : A ∩ A₀ = A :=
+      Finset.eq_of_subset_of_card_le Finset.inter_subset_left (by omega)
+    have h2 : A ⊆ A₀ := h1 ▸ Finset.inter_subset_right
+    exact hne (Finset.eq_of_subset_of_card_le h2 (by omega))
+
+end RelSignature

scripts/axiom_audit.lean

@@ -206,3 +206,10 @@ custom axioms. Target list and policy: `scripts/check_census_and_axioms.py`
 #print axioms RelSignature.condExp_ae_eq_condExp_of_comap_eq
 #print axioms RelSignature.InfiniteRelExchangeableLaw.measurePreserving_relabel
 #print axioms RelSignature.InfiniteRelExchangeableLaw.relabel_preimage_ae_eq_of_fixingAlgebra
+#print axioms RelSignature.RelStructure.lowerRankAlgebra_le
+#print axioms RelSignature.RelStructure.fixingAlgebra_le_lowerRankAlgebra
+#print axioms RelSignature.RelStructure.lowerRankAlgebra_mono
+#print axioms RelSignature.RelStructure.lowerRankAlgebra_zero
+#print axioms RelSignature.RelStructure.lowerRankAlgebra_one
+#print axioms RelSignature.RelStructure.comap_relabel_lowerRankAlgebra
+#print axioms RelSignature.card_inter_lt_of_ne

scripts/check_census_and_axioms.py

@@ -189,6 +189,13 @@
     "MeasureTheory.Digraphon.measurable_sampleInfinite",
     "MeasureTheory.Digraphon.measurable_sampleFinite",
     "RelSignature.InfiniteRelExchangeableLaw.condIndep_fixingAlgebra",
+    "RelSignature.RelStructure.lowerRankAlgebra_le",
+    "RelSignature.RelStructure.fixingAlgebra_le_lowerRankAlgebra",
+    "RelSignature.RelStructure.lowerRankAlgebra_mono",
+    "RelSignature.RelStructure.lowerRankAlgebra_zero",
+    "RelSignature.RelStructure.lowerRankAlgebra_one",
+    "RelSignature.RelStructure.comap_relabel_lowerRankAlgebra",
+    "RelSignature.card_inter_lt_of_ne",
     "RelSignature.condExp_ae_eq_condExp_of_comap_eq",
     "RelSignature.InfiniteRelExchangeableLaw.measurePreserving_relabel",
     "RelSignature.InfiniteRelExchangeableLaw.relabel_preimage_ae_eq_of_fixingAlgebra",