feat: I(1), the rank-one transfer step (#107)

Graphon.lean

@@ -23,6 +23,7 @@ import Graphon.RelKernelSampler
 import Graphon.KernelRandomization
 import Graphon.ForMathlib.RelativeFactorCoupling
 import Graphon.UniformFactorCoupling
+import Graphon.RelRankOneTransfer
 import Graphon.RelFixingAlgebra
 import Graphon.RelRankAlgebra
 import Graphon.RelLowerFactor
@@ -203,6 +204,7 @@ in Lean 4 using Mathlib.
 * `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.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
 * `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.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/ForMathlib/RelativeFactorCoupling.lean

@@ -169,6 +169,38 @@ theorem map_factorProd_relativeFactorCoupling (hq : Measurable q) :
   filter_upwards [h1] with p hp
   simp [hp]
 
+omit [StandardBorelSpace Z] [Nonempty Z] in
+/-- **A symmetry of the first space that fixes the factor is a symmetry of the coupling.** If `T`
+preserves `μ` and satisfies `q ∘ T = q`, then `Prod.map T id` preserves the joining: `T` acts
+within the fibres of `q`, so it leaves each disintegration fibre invariant and never touches the
+outer integration. -/
+theorem map_prodMap_relativeFactorCoupling (hq : Measurable q) {T : Ω → Ω}
+    (hT : MeasurePreserving T μ μ) (hqT : q ∘ T = q) :
+    (relativeFactorCoupling μ ν q r).map (Prod.map T id) = relativeFactorCoupling μ ν q r := by
+  haveI : IsProbabilityMeasure (μ.map q) := Measure.isProbabilityMeasure_map hq.aemeasurable
+  have h1 : condDistrib T q μ =ᵐ[μ.map q] (condDistrib id q μ).map T := by
+    simpa using condDistrib_comp q aemeasurable_id hT.measurable
+  have h2 : condDistrib T q μ =ᵐ[μ.map q] condDistrib id q μ := by
+    rw [condDistrib_ae_eq_iff_measure_eq_compProd _ hT.measurable.aemeasurable,
+      compProd_map_condDistrib (aemeasurable_id (μ := μ))]
+    simp only [id_eq]
+    have hcomp : (fun x => (q x, T x)) = (fun y : Ω => (q y, y)) ∘ T := by
+      funext x
+      have hx : q (T x) = q x := congrFun hqT x
+      rw [Function.comp_apply, hx]
+    calc μ.map (fun x => (q x, T x))
+        = μ.map ((fun y : Ω => (q y, y)) ∘ T) := by rw [hcomp]
+      _ = (μ.map T).map (fun y : Ω => (q y, y)) :=
+          (Measure.map_map (by fun_prop) hT.measurable).symm
+      _ = μ.map (fun y : Ω => (q y, y)) := by rw [hT.map_eq]
+  have hcd : (condDistrib id q μ).map T =ᵐ[μ.map q] condDistrib id q μ := h1.symm.trans h2
+  rw [relativeFactorCoupling, Measure.map_comp _ _ (hT.measurable.prodMap measurable_id)]
+  refine Measure.comp_congr ?_
+  filter_upwards [hcd] with z hz
+  rw [Kernel.map_apply _ (hT.measurable.prodMap measurable_id), Kernel.prod_apply,
+    ← Measure.map_prod_map _ _ hT.measurable measurable_id,
+    ← Kernel.map_apply _ hT.measurable, hz, Measure.map_id]
+
 /-- **The two coordinates are conditionally independent given the common factor.** The
 conditioning σ-algebra is the one generated by `q ∘ Prod.fst`, a random variable on the coupling
 space itself rather than the integrated-out disintegration variable. -/
@@ -208,4 +240,16 @@ theorem condIndepFun_fst_snd_relativeFactorCoupling (hq : Measurable q) (hr : Me
   filter_upwards [hcd1, hcd2] with z h1 h2
   rw [Kernel.prod_apply, Kernel.prod_apply, Kernel.prod_apply, Kernel.prod_apply, h1, h2]
 
+/-- **The transfer clause.** Conditional independence passes to any measurable function of the
+first coordinate: the second coordinate tells nothing about *any* reading of the first beyond
+what the common factor already determines. Stated separately because this — not the marginals and
+not the common-factor identity — is what rules out the second coordinate secretly encoding the
+part of the first that the factor leaves unresolved. -/
+theorem condIndepFun_comp_fst_snd_relativeFactorCoupling (hq : Measurable q) (hr : Measurable r)
+    (hqr : ν.map r = μ.map q) {Y : Type*} [MeasurableSpace Y] {g : Ω → Y} (hg : Measurable g) :
+    CondIndepFun (MeasurableSpace.comap (q ∘ Prod.fst) inferInstance)
+      (hq.comp measurable_fst).comap_le (g ∘ Prod.fst) Prod.snd
+      (relativeFactorCoupling μ ν q r) :=
+  (condIndepFun_fst_snd_relativeFactorCoupling hq hr hqr).comp hg measurable_id
+
 end ProbabilityTheory

Graphon/RelRankOneTransfer.lean

@@ -0,0 +1,143 @@
+/-
+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.RelLowerFactor
+import Graphon.UniformFactorCoupling
+
+/-!
+# The rank-one transfer step, I(1) (R4 converse piece 3, #107)
+
+The instantiation of `ProbabilityTheory.relativeFactorCoupling` at `q = lowerFactorMap 1`: the
+base of the rank recursion, in which the rank-one factor of an exchangeable law is carried by a
+single uniform latent that says nothing further about the structure.
+
+## The rank-one factor is relabeling invariant, on the nose
+
+`LowerIndex 1` consists of the indices anchored at a set of cardinality `< 1`, i.e. at `∅`, and a
+basis event anchored at `∅` is measurable for `fixingAlgebra ∅ = invariantAlgebra` — so it is
+literally invariant under every finitely supported sortwise relabeling, not merely invariant
+modulo the law. Hence `lowerFactorMap 1 ∘ relabel σ = lowerFactorMap 1` as functions
+(`lowerFactorMap_one_relabel`), and the equivariance square of `Graphon.RelLowerFactor` degenerates
+at rank one: no transport of the factor space is needed, and the conditioning factor of the
+coupling does not move with `σ`.
+
+That is what makes the coupling itself relabeling invariant
+(`map_prodMap_relabel_rankOneCoupling`): the relabeling acts inside the fibres of the factor, so
+it preserves each disintegration fibre and never disturbs the outer integration. At higher rank
+this fails — the factor map is only *equivariant*, not invariant — and the corresponding statement
+will have to move the factor space by `lowerFactorSpaceEquiv` on the other side.
+
+## What I(1) has to say, and what it must not leave out
+
+`exists_rankOneUniformCoupling` bundles the six clauses. The marginals and the common-factor
+identity are not by themselves the full statement: they say the latent *resolves* the factor, but
+nothing about what else the latent might know. Without the conditional-independence clause the
+latent could encode arbitrary further information about the part of the structure that rank one
+leaves unresolved, which would make the recursion's next step unsound. The clause is stated in
+its strongest form — conditional independence of the *whole* structure coordinate from the
+latent — so the reading for any particular unresolved part follows by measurable composition;
+`condIndepFun_comp_fst_snd_rankOne` records that transfer explicitly.
+
+No σ-algebra equality between the latent and the factor is claimed. The latent may carry strictly
+more than `lowerFactorMap 1` reads; conditional independence is exactly the statement that the
+surplus is irrelevant to the structure.
+-/
+
+open MeasureTheory ProbabilityTheory
+
+namespace RelSignature
+
+namespace CoherentBasis
+
+universe u
+
+variable {S : RelSignature.{u}} {M : InfiniteRelExchangeableLaw S} (B : CoherentBasis M)
+
+/-! ### Rank one is invariant, not merely equivariant -/
+
+/-- A rank-one basis index is anchored at the empty set. -/
+theorem anchor_eq_empty_of_lowerIndex_one (i : B.LowerIndex 1) : B.anchor i.1 = ∅ :=
+  Finset.card_eq_zero.mp (by have := i.2; omega)
+
+open scoped Classical in
+/-- **The rank-one factor map is relabeling invariant on the nose.** Its coordinates are basis
+events anchored at `∅`, hence `invariantAlgebra`-measurable, hence literally fixed by every
+finitely supported sortwise relabeling — no null sets and no transport of the factor space. -/
+theorem lowerFactorMap_one_relabel (σ : FinSuppPerm S) :
+    B.lowerFactorMap 1 ∘ RelStructure.relabel σ.1 = B.lowerFactorMap 1 := by
+  classical
+  funext X i
+  have hmem := B.event_mem i.1
+  rw [B.anchor_eq_empty_of_lowerIndex_one i, RelStructure.fixingAlgebra_empty] at hmem
+  have hiff : (RelStructure.relabel σ.1 X ∈ B.event i.1) ↔ (X ∈ B.event i.1) :=
+    Set.ext_iff.mp (hmem.2 σ.1 σ.2) X
+  show decide (RelStructure.relabel σ.1 X ∈ B.event i.1) = decide (X ∈ B.event i.1)
+  exact decide_eq_decide.mpr hiff
+
+/-! ### The rank-one coupling -/
+
+variable [Countable S.Rel]
+
+/-- **Relabeling compatibility of the rank-one coupling.** Every finitely supported sortwise
+relabeling of the structure coordinate preserves the coupling. It fixes the rank-one factor
+exactly, so it acts within the fibres of the disintegration. -/
+theorem map_prodMap_relabel_rankOneCoupling (f : ℝ → B.LowerFactorSpace 1) (σ : FinSuppPerm S) :
+    (relativeFactorCoupling (M.law : Measure (RelStructure S (Vinfinite S))) uniform01
+        (B.lowerFactorMap 1) f).map (Prod.map (RelStructure.relabel σ.1) id) =
+      relativeFactorCoupling (M.law : Measure (RelStructure S (Vinfinite S))) uniform01
+        (B.lowerFactorMap 1) f :=
+  map_prodMap_relativeFactorCoupling (B.measurable_lowerFactorMap' 1)
+    (M.measurePreserving_relabel σ.1) (B.lowerFactorMap_one_relabel σ)
+
+/-- **I(1)**: the rank-one factor of an arbitrary exchangeable law is carried by a uniform latent
+that says nothing further about the structure.
+
+The six clauses: `f` is measurable; the coupling is a probability measure; its structure marginal
+is the original law; its latent marginal is uniform; the latent **resolves** the rank-one factor,
+`lowerFactorMap 1 X = f ξ` almost surely; and the structure and the latent are **conditionally
+independent given that factor**.
+
+The last clause is the one that cannot be dropped. The marginals and the resolution identity
+together still permit a latent that encodes information about everything rank one does not
+resolve; conditional independence is what forbids it, and it is stated over the whole structure
+coordinate so that the reading for any particular unresolved part follows by composition
+(`condIndepFun_comp_fst_snd_rankOne`).
+
+Relabeling compatibility holds for this coupling as for any other and is recorded separately in
+`map_prodMap_relabel_rankOneCoupling`. -/
+theorem exists_rankOneUniformCoupling :
+    ∃ f : ℝ → B.LowerFactorSpace 1, Measurable f ∧
+      IsProbabilityMeasure (relativeFactorCoupling
+        (M.law : Measure (RelStructure S (Vinfinite S))) uniform01 (B.lowerFactorMap 1) f) ∧
+      (relativeFactorCoupling (M.law : Measure (RelStructure S (Vinfinite S))) uniform01
+        (B.lowerFactorMap 1) f).map Prod.fst = (M.law : Measure (RelStructure S (Vinfinite S))) ∧
+      (relativeFactorCoupling (M.law : Measure (RelStructure S (Vinfinite S))) uniform01
+        (B.lowerFactorMap 1) f).map Prod.snd = uniform01 ∧
+      B.lowerFactorMap 1 ∘ Prod.fst =ᵐ[relativeFactorCoupling
+        (M.law : Measure (RelStructure S (Vinfinite S))) uniform01 (B.lowerFactorMap 1) f]
+          f ∘ Prod.snd ∧
+      CondIndepFun (MeasurableSpace.comap (B.lowerFactorMap 1 ∘ Prod.fst) inferInstance)
+        ((B.measurable_lowerFactorMap' 1).comp measurable_fst).comap_le Prod.fst Prod.snd
+        (relativeFactorCoupling (M.law : Measure (RelStructure S (Vinfinite S))) uniform01
+          (B.lowerFactorMap 1) f) :=
+  exists_relativeFactorCoupling_uniform01 (M.law : Measure (RelStructure S (Vinfinite S)))
+    (B.measurable_lowerFactorMap' 1)
+
+/-- **The transfer clause at rank one.** The latent is conditionally independent, given the
+rank-one factor, of *every* measurable reading of the structure — in particular of whatever the
+rank-one factor leaves unresolved. This is the form the next step of the recursion consumes. -/
+theorem condIndepFun_comp_fst_snd_rankOne {f : ℝ → B.LowerFactorSpace 1} (hf : Measurable f)
+    (hfq : uniform01.map f =
+      (M.law : Measure (RelStructure S (Vinfinite S))).map (B.lowerFactorMap 1))
+    {Y : Type*} [MeasurableSpace Y] {g : RelStructure S (Vinfinite S) → Y} (hg : Measurable g) :
+    CondIndepFun (MeasurableSpace.comap (B.lowerFactorMap 1 ∘ Prod.fst) inferInstance)
+      ((B.measurable_lowerFactorMap' 1).comp measurable_fst).comap_le (g ∘ Prod.fst) Prod.snd
+      (relativeFactorCoupling (M.law : Measure (RelStructure S (Vinfinite S))) uniform01
+        (B.lowerFactorMap 1) f) :=
+  condIndepFun_comp_fst_snd_relativeFactorCoupling (B.measurable_lowerFactorMap' 1) hf hfq hg
+
+end CoherentBasis
+
+end RelSignature

scripts/axiom_audit.lean

@@ -246,3 +246,12 @@ custom axioms. Target list and policy: `scripts/check_census_and_axioms.py`
 #print axioms ProbabilityTheory.map_factorProd_relativeFactorCoupling
 #print axioms ProbabilityTheory.condIndepFun_fst_snd_relativeFactorCoupling
 #print axioms ProbabilityTheory.exists_relativeFactorCoupling_uniform01
+#print axioms ProbabilityTheory.map_prodMap_relativeFactorCoupling
+#print axioms ProbabilityTheory.condIndepFun_comp_fst_snd_relativeFactorCoupling
+
+-- R4 converse piece 3 (#107): I(1), the rank-one transfer step.
+#print axioms RelSignature.CoherentBasis.anchor_eq_empty_of_lowerIndex_one
+#print axioms RelSignature.CoherentBasis.lowerFactorMap_one_relabel
+#print axioms RelSignature.CoherentBasis.map_prodMap_relabel_rankOneCoupling
+#print axioms RelSignature.CoherentBasis.exists_rankOneUniformCoupling
+#print axioms RelSignature.CoherentBasis.condIndepFun_comp_fst_snd_rankOne