From 4d952eb857cd5c69c02848f231a88cddc7e62caa Mon Sep 17 00:00:00 2001
From: Cameron Freer <cameronfreer@gmail.com>
Date: Sat, 15 Aug 2026 15:33:27 +0000
Subject: [PATCH 01/13] =?UTF-8?q?feat:=20extend=20a=20finite=20partial=20i?=
 =?UTF-8?q?njection=20of=20=E2=84=95=20to=20a=20permutation=20(#195=20stag?=
 =?UTF-8?q?e=203)?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

exists_perm_extend_of_injOn generalizes exists_perm_extend from an
initial segment to an arbitrary finite domain, by the same
Equiv.Set.compl argument. It is the finite-agreement step for the joint
restriction theorem: on a joint cylinder, the combined vertex support is
finite, and a pooled permutation must be found carrying the original
embedding to an arbitrary one there.
---
 Graphon/PermutationExtension.lean | 22 ++++++++++++++++++++++
 1 file changed, 22 insertions(+)

diff --git a/Graphon/PermutationExtension.lean b/Graphon/PermutationExtension.lean
index 6e40d6c..f5a7ebb 100644
--- a/Graphon/PermutationExtension.lean
+++ b/Graphon/PermutationExtension.lean
@@ -43,3 +43,25 @@ theorem exists_perm_extend {k : ℕ} (g : Fin k ↪ ℕ) :
   show ((Equiv.ofInjective g g.injective)
     ((Equiv.ofInjective _ Fin.val_injective).symm ⟨(↑a : ℕ), ⟨a, rfl⟩⟩) : ℕ) = g a
   rw [h1]; rfl
+
+/-- **Every finite partial injection of `ℕ` extends to a permutation**: the domain and its image
+are finite, so their complements are countably infinite and hence equivalent, and
+`Equiv.Set.compl` assembles the permutation. Generalizes `exists_perm_extend` from an initial
+segment to an arbitrary finite domain. -/
+theorem exists_perm_extend_of_injOn {A : Finset ℕ} {g : ℕ → ℕ} (hg : Set.InjOn g ↑A) :
+    ∃ σ : Equiv.Perm ℕ, ∀ a ∈ A, σ a = g a := by
+  classical
+  let e₀ : (↑A : Set ℕ) ≃ (g '' ↑A : Set ℕ) := Equiv.Set.imageOfInjOn g (↑A : Set ℕ) hg
+  have hsc : ((↑A : Set ℕ)ᶜ).Infinite := (A.finite_toSet).infinite_compl
+  have htc : ((g '' ↑A : Set ℕ)ᶜ).Infinite :=
+    ((A.finite_toSet).image g).infinite_compl
+  haveI := hsc.to_subtype
+  haveI := htc.to_subtype
+  haveI : Denumerable ((↑A : Set ℕ)ᶜ : Set ℕ) := Denumerable.ofEncodableOfInfinite _
+  haveI : Denumerable ((g '' ↑A : Set ℕ)ᶜ : Set ℕ) := Denumerable.ofEncodableOfInfinite _
+  obtain ⟨σ, hσ⟩ := (Equiv.Set.compl e₀).symm
+    ((Denumerable.eqv _).trans (Denumerable.eqv _).symm)
+  refine ⟨σ, fun a ha => ?_⟩
+  have h := hσ ⟨a, ha⟩
+  rw [h]
+  rfl

From f867572c721c6d8096080c28a0bb414ddd564811 Mon Sep 17 00:00:00 2001
From: Cameron Freer <cameronfreer@gmail.com>
Date: Sat, 15 Aug 2026 17:35:18 +0000
Subject: [PATCH 02/13] feat: the joint restriction theorem and transport
 characterization (#195 stage 3)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

PooledRankExtension.map_restrict_embedding: for EVERY sortwise embedding
e into the pooled carrier, restricting jointly — structure and latents
along the same e — returns C.P exactly. Joint, so it recovers the
(X, U_<n) law rather than only a structure window.

Proof: joint-cylinder extensionality plus finite agreement with a mixed
pooled permutation. On a cylinder the combined vertex support is finite;
originalVertex v ↦ e v is a finite partial injection of the pooled
carrier, extended by exists_perm_extend_of_injOn; full mixed invariance
absorbs the permutation and permits choosing it per sort.

latentIndexEmbed_eq_of_agree is the support-wise index lemma, proved with
ABSTRACT carriers per the standing rule — instantiating at PoolVertex
(a Sum) under Classical Finset.image otherwise clashes with the derived
DecidableEq, which it did again here before the lemma was generalized.

map_poolVertexEquiv is the reviewer's checkpoint: the canonical
specialization, isolating map directions while the claim is still just an
equality of joint laws, plus the agreement of any two extensions after
that identification. Audit 384 -> 389.
---
 Graphon.lean                       |   2 +
 Graphon/RelLatentGeometry.lean     |  15 +++
 Graphon/RelPooledAcceptance.lean   | 207 +++++++++++++++++++++++++++++
 scripts/axiom_audit.lean           |   7 +
 scripts/check_census_and_axioms.py |   5 +
 5 files changed, 236 insertions(+)
 create mode 100644 Graphon/RelPooledAcceptance.lean

diff --git a/Graphon.lean b/Graphon.lean
index ddf5012..db174f3 100644
--- a/Graphon.lean
+++ b/Graphon.lean
@@ -46,6 +46,7 @@ import Graphon.RelRankInjectionInvariance
 import Graphon.RelLatentGeometry
 import Graphon.RelPooledLatents
 import Graphon.RelPooledExtension
+import Graphon.RelPooledAcceptance
 import Graphon.RelSingletonPeel
 import Graphon.RelFixingAlgebra
 import Graphon.RelRankAlgebra
@@ -263,6 +264,7 @@ in Lean 4 using Mathlib.
 * `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.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. `PooledRankExtension.map_poolVertexEquiv` is the canonical specialization, giving the transport characterization and the agreement of any two extensions after that identification
 * `Graphon.RelRankInjectionInvariance` — R4 converse (#107), the isolated proof risk of the pooled-latent extension gate: **joint invariance under arbitrary sortwise self-injections**. `RankRepresentation.invariant` is stated for *finitely supported permutations*, but a pooled object built cheaply through `poolVertexEquiv` needs the joint law invariant under every self-injection; `RankRepresentation.map_prodMap_restrict_self` supplies exactly that, so full mixed pooled invariance later costs no additional mathematics. The route is finite-cylinder extensionality on the **joint** space, which had no machinery before — rank one's joint invariance goes through only because the rank-one latent action is trivial. `rankLatentIndexInj`/`rankLatentReindex` extend the latent action from permutations to injections (only injectivity is used — a support keeps its cardinality); `exists_finSuppPerm_agree_on_finset` matches an injection to a finitely supported permutation on any finite tagged-vertex support; `ext_of_prod_cylinders` is the joint extensionality, rectangles of coordinate cylinders on both factors. **No finiteness/`Fintype` hypothesis beyond `RankRepresentation`'s ambient countability.** Equality is tested on *coordinate* cylinders — finitely many `RelCoord`s and finitely many latent indices — whose combined vertex support is one finite `Finset (Σ s, Vinfinite S s)` and so touches only finitely many sorts; the injection is matched there by extending it on each active sort, taking the identity elsewhere, and maximizing finitely many support bounds. The coarser `restrictFin` cylinder family would instead force a uniform all-sort bound that no self-injection need admit
 * `Graphon.RelRankCoding` — R4 converse piece 3 (#107): factor-law coding of the lower-rank factor. **Not** the inductive hypothesis of a working recursion: `RankCoding n → ShellProperty n` is **false**, refuted by Austin's random complete bipartite graph `X_uv = z_u ⊕ z_v` (arXiv:0801.1698 §3.6), where `lowerRankAlgebra 2` is trivial modulo the law but every triangle satisfies `X₁₂ ⊕ X₁₃ ⊕ X₂₃ = 0`, so the exact layers are pairwise but not mutually independent — while a `RankCoding 2` exists because the rank-2 factor law is a point mass. The example separates the true two-set theorem from mutuality, and shows the gap is not closable by coupling: a relatively independent joining over `lowerFactorMap` attaches latents that are conditionally independent of the structure given a trivial factor, whereas a representation needs the hidden colours, correlated with the array yet not recoverable from it. `RankCoding n` represents the rank-`n` factor by latents — a measurable coding map carrying the latent source to the factor law and intertwining the two relabeling actions **almost everywhere**. The a.e. form is forced: `lowerFactorSpaceEquiv σ n` fixes the *image* of `lowerFactorMap n`, not the whole Bool-cube, since it permutes distinct basis indices that name the same event, so the strict version is false already at rank one. `ShellProperty n` is the conclusion the recursion consumes, bundling mutual conditional independence of the exact layers over the rank-`n` supports **with** per-support locality; neither half implies the other, since mutual independence given the whole lower-rank factor permits dependence on all of it rather than only through `boundaryMap A`. `RankCoding.rankOne` is the base case, built from the #140 randomization adapter transported along `rankLatentOneEquiv`; its equivariance clause is genuinely exercised rather than vacuous, because at rank one the latent relabeling is the identity while the factor equivalence is not
 * `Graphon.RelFixingAlgebra` — R4 converse piece 2a (#107): the **law-independent** factor-algebra layer — `SortwiseFixing` (the `A`-fixing stabilizer of finitely supported sortwise permutations, closed under `1`/`*`/`⁻¹`/conjugation), the raw `RelStructure.fixingAlgebra` (events invariant under the `A`-fixing group; deliberately *not* "generated by relations inside `A`", which loses hidden vertex information), monotonicity, `fixingAlgebra_empty = invariantAlgebra` (near-definitional), and the **transport equality** `fixingAlgebra_comap_relabel : comap (relabel σ) (fixingAlgebra A) = fixingAlgebra (image σ A)` via stabilizer conjugation — no completions, no law; the conditional-independence theorem is its own later PR
diff --git a/Graphon/RelLatentGeometry.lean b/Graphon/RelLatentGeometry.lean
index 0377c7c..e2afa18 100644
--- a/Graphon/RelLatentGeometry.lean
+++ b/Graphon/RelLatentGeometry.lean
@@ -238,6 +238,21 @@ theorem latentRestrictOver_toEmbedding (ρ : ∀ s, Equiv.Perm (V s)) (n : ℕ)
   refine Finset.ext fun v => ?_
   simp [Finset.mem_image]
 
+open scoped Classical in
+/-- **Support-wise agreement**: if a permutation of the target carrier carries one embedding to
+another on every vertex of a support, the two induced index maps agree there. Stated with
+abstract carriers, so instantiating never manipulates `Finset.image` under a derived
+`DecidableEq`. -/
+theorem latentIndexEmbed_eq_of_agree {e f : ∀ s, V s ↪ W s} {ρ : ∀ s, Equiv.Perm (W s)} {n : ℕ}
+    {A : LatentIndexOver S V n} (h : ∀ v ∈ A.1, ρ v.1 (e v.1 v.2) = f v.1 v.2) :
+    latentIndexEmbed f n A = latentIndexPerm ρ n (latentIndexEmbed e n A) := by
+  refine Subtype.ext ?_
+  rw [latentIndexEmbed_coe, latentIndexPerm_apply_coe, latentIndexEmbed_coe, Finset.image_image]
+  refine Finset.image_congr fun v hv => ?_
+  obtain ⟨s, x⟩ := v
+  show (⟨s, f s x⟩ : Σ s : S.Srt, W s) = ⟨s, ρ s (e s x)⟩
+  rw [h ⟨s, x⟩ hv]
+
 /-- **The conjugation square for a carrier equivalence** — the latent-side mirror of
 `RelStructure.congrCarrier_relabel`. Transporting along `e` intertwines a permutation of the
 source carrier with its conjugate on the target. Proved carrier-generically, so instantiating at
diff --git a/Graphon/RelPooledAcceptance.lean b/Graphon/RelPooledAcceptance.lean
new file mode 100644
index 0000000..5754931
--- /dev/null
+++ b/Graphon/RelPooledAcceptance.lean
@@ -0,0 +1,207 @@
+/-
+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.RelPooledExtension
+
+/-!
+# The joint restriction theorem for a pooled rank extension (R4 converse, #107)
+
+Stage 3 of the pooled-latent extension gate, organizing result:
+
+`PooledRankExtension.map_restrict_embedding` — for **every** sortwise embedding
+`e : ∀ s, Vinfinite S s ↪ PoolVertex S s`, restricting the extension jointly along `e` returns the
+representation exactly:
+
+```
+Q.law.map (Prod.map (RelStructure.restrict e) (latentRestrictOver e n)) = C.P
+```
+
+This is joint, not a structure marginal: the structure and the latents are restricted along the
+same embedding, so it recovers the joint `(X, U_{<n})` law and says strictly more than a
+structure-only window theorem.
+
+The proof is joint-cylinder extensionality together with finite agreement by a mixed pooled
+permutation. On a joint cylinder the combined vertex support is finite; the partial assignment
+`originalVertex v ↦ e v` on it is a finite partial injection of the pooled carrier, since both
+embeddings are injective, so it extends to a pooled permutation `ρ` with `ρ (ov v) = e v` there.
+Both restrictions then read the same moved coordinates, and the full mixed invariance of the
+extension absorbs `ρ`. Choosing `ρ` separately on each sort is exactly what the *full* action
+permits — no finite-support or uniform-bound issue arises.
+-/
+
+open MeasureTheory
+
+namespace RelSignature
+
+namespace InfiniteRelExchangeableLaw
+
+universe u
+
+variable {S : RelSignature.{u}} [Countable S.Srt] [Countable S.Rel]
+  {M : InfiniteRelExchangeableLaw S} {n : ℕ}
+
+/-- **Finite agreement by a pooled permutation**: any sortwise embedding into the pooled carrier
+agrees with a pooled permutation composed with the original embedding, on any finite set of
+original vertices. The permutation is chosen independently on each sort, which the full mixed
+action allows. -/
+theorem exists_poolPerm_agree (e : ∀ s, Vinfinite S s ↪ PoolVertex S s)
+    (V : Finset (Σ s : S.Srt, Vinfinite S s)) :
+    ∃ ρ : ∀ s, Equiv.Perm (PoolVertex S s),
+      ∀ v ∈ V, ρ v.1 (originalVertex S v.1 v.2) = e v.1 v.2 := by
+  classical
+  set W : Finset ℕ := V.image (fun v => v.2) with hW
+  have hsort : ∀ s : S.Srt, ∃ ρ : Equiv.Perm (PoolVertex S s),
+      ∀ x ∈ W, ρ (originalVertex S s x) = e s x := by
+    intro s
+    set pv : PoolVertex S s ≃ ℕ := poolVertexEquiv S s with hpv
+    set g : ℕ → ℕ := fun y =>
+      if h : ∃ x, pv (originalVertex S s x) = y then pv (e s h.choose) else y with hg
+    have hinj : ∀ x₁ x₂ : ℕ, pv (originalVertex S s x₁) = pv (originalVertex S s x₂) → x₁ = x₂ :=
+      fun x₁ x₂ h => (originalVertex S s).injective (pv.injective h)
+    have hgval : ∀ x : ℕ, g (pv (originalVertex S s x)) = pv (e s x) := by
+      intro x
+      have hex : ∃ x', pv (originalVertex S s x') = pv (originalVertex S s x) := ⟨x, rfl⟩
+      rw [hg]
+      simp only [dif_pos hex]
+      exact congrArg (fun z => pv (e s z)) (hinj _ _ hex.choose_spec)
+    have hInjOn : Set.InjOn g ↑(W.image fun x => pv (originalVertex S s x)) := by
+      intro y₁ hy₁ y₂ hy₂ hy
+      simp only [Finset.coe_image, Set.mem_image, Finset.mem_coe] at hy₁ hy₂
+      obtain ⟨x₁, -, rfl⟩ := hy₁
+      obtain ⟨x₂, -, rfl⟩ := hy₂
+      rw [hgval, hgval] at hy
+      exact congrArg (fun z => pv (originalVertex S s z))
+        ((e s).injective (pv.injective hy))
+    obtain ⟨σ, hσ⟩ := exists_perm_extend_of_injOn hInjOn
+    refine ⟨pv.symm.permCongr σ, fun x hx => ?_⟩
+    have hmem : pv (originalVertex S s x) ∈ W.image fun x => pv (originalVertex S s x) :=
+      Finset.mem_image.mpr ⟨x, hx, rfl⟩
+    show pv.symm (σ (pv (originalVertex S s x))) = e s x
+    rw [hσ _ hmem, hgval, Equiv.symm_apply_apply]
+  choose ρ hρ using hsort
+  refine ⟨ρ, fun v hv => hρ v.1 v.2 ?_⟩
+  exact Finset.mem_image.mpr ⟨v, hv, rfl⟩
+
+/-- **The joint restriction theorem.** Restricting a pooled rank extension along *any* sortwise
+embedding into the pooled carrier — structure and latents together — returns the representation
+exactly. Mixed windows are included: the embedding may land anywhere in the pooled carrier. -/
+theorem PooledRankExtension.map_restrict_embedding {C : M.RankRepresentation n}
+    (Q : PooledRankExtension C) (e : ∀ s, Vinfinite S s ↪ PoolVertex S s) :
+    (Q.law : Measure (RelStructure S (PoolVertex S) × PooledRankLatentSpace S n)).map
+      (Prod.map (RelStructure.restrict e) (latentRestrictOver e n)) = C.P := by
+  classical
+  haveI := C.isProbabilityMeasure_P
+  have hjointE : Measurable
+      (Prod.map (RelStructure.restrict e) (latentRestrictOver (S := S) e n)) :=
+    (measurable_restrict e).prodMap (measurable_latentRestrictOver e n)
+  haveI : IsProbabilityMeasure
+      ((Q.law : Measure (RelStructure S (PoolVertex S) × PooledRankLatentSpace S n)).map
+        (Prod.map (RelStructure.restrict e) (latentRestrictOver (S := S) e n))) :=
+    Measure.isProbabilityMeasure_map hjointE.aemeasurable
+  refine ext_of_prod_cylinders ?_ (by simp)
+  rintro A hA B hB
+  have hAmeas : MeasurableSet A := MeasurableSet.of_mem_measurableCylinders hA
+  have hBmeas : MeasurableSet B := MeasurableSet.of_mem_measurableCylinders hB
+  rw [mem_measurableCylinders] at hA hB
+  obtain ⟨Fs, T, hT, rfl⟩ := hA
+  obtain ⟨Fl, T', hT', rfl⟩ := hB
+  obtain ⟨ρ, hρ⟩ := exists_poolPerm_agree e
+    (Fs.biUnion RelCoord.support ∪ Fl.biUnion fun A => A.1)
+  have hmemL : ∀ v ∈ Fs.biUnion RelCoord.support,
+      ρ v.1 (originalVertex S v.1 v.2) = e v.1 v.2 := fun v hv =>
+    hρ v (Finset.mem_union_left _ hv)
+  have hmemR : ∀ v ∈ Fl.biUnion fun A => A.1,
+      ρ v.1 (originalVertex S v.1 v.2) = e v.1 v.2 := fun v hv =>
+    hρ v (Finset.mem_union_right _ hv)
+  -- on this cylinder, restricting along `e` is restricting along `ov` after relabeling by `ρ`
+  have hstruct : RelStructure.restrict e ⁻¹' cylinder Fs T
+      = (restrictOriginal S ∘ RelStructure.relabel ρ) ⁻¹' cylinder Fs T := by
+    ext X
+    simp only [Set.mem_preimage, mem_cylinder, Function.comp_apply]
+    refine Iff.of_eq (congrArg (fun y => y ∈ T) ?_)
+    funext c
+    show X (RelCoord.map (fun s => ⇑(e s)) c)
+      = X (RelCoord.map (fun s => ⇑(ρ s)) (RelCoord.map (fun s => ⇑(originalVertex S s)) c))
+    refine congrArg X (Sigma.ext rfl (heq_of_eq (funext fun i => ?_)))
+    exact (hmemL ((c : RelCoord S (Vinfinite S)).taggedValue i)
+      (Finset.mem_biUnion.mpr ⟨c, c.2, (RelCoord.mem_support_iff _ _).mpr ⟨i, rfl⟩⟩)).symm
+  have hlat : latentRestrictOver e n ⁻¹' cylinder Fl T'
+      = (restrictOriginalLatents S n ∘ pooledRankLatentRelabel ρ n) ⁻¹' cylinder Fl T' := by
+    ext ω
+    simp only [Set.mem_preimage, mem_cylinder, Function.comp_apply]
+    refine Iff.of_eq (congrArg (fun y => y ∈ T') ?_)
+    funext i
+    show ω (latentIndexEmbed e n i)
+      = ω (latentIndexPerm ρ n (latentIndexEmbed (fun s => originalVertex S s) n i))
+    exact congrArg ω (latentIndexEmbed_eq_of_agree fun v hv =>
+      hmemR v (Finset.mem_biUnion.mpr ⟨i, i.2, hv⟩))
+  have hOvMeas : Measurable (Prod.map (restrictOriginal S) (restrictOriginalLatents S n)) :=
+    (measurable_restrictOriginal).prodMap (measurable_restrictOriginalLatents n)
+  have hRhoMeas : Measurable
+      (Prod.map (RelStructure.relabel ρ) (pooledRankLatentRelabel ρ n)) :=
+    (measurable_relabel ρ).prodMap (pooledRankLatentRelabel ρ n).measurable
+  have hcomp : Prod.map (RelStructure.restrict e) (latentRestrictOver (S := S) e n) ⁻¹'
+        (cylinder Fs T ×ˢ cylinder Fl T')
+      = Prod.map (RelStructure.relabel ρ) (pooledRankLatentRelabel ρ n) ⁻¹'
+          (Prod.map (restrictOriginal S) (restrictOriginalLatents S n) ⁻¹'
+            (cylinder Fs T ×ˢ cylinder Fl T')) := by
+    rw [Set.preimage_prod_map_prod, hstruct, hlat, Set.preimage_prod_map_prod,
+      Set.preimage_prod_map_prod, Set.preimage_comp, Set.preimage_comp]
+  calc ((Q.law : Measure (RelStructure S (PoolVertex S) × PooledRankLatentSpace S n)).map
+        (Prod.map (RelStructure.restrict e) (latentRestrictOver (S := S) e n)))
+        (cylinder Fs T ×ˢ cylinder Fl T')
+      = (Q.law : Measure (RelStructure S (PoolVertex S) × PooledRankLatentSpace S n))
+          (Prod.map (RelStructure.relabel ρ) (pooledRankLatentRelabel ρ n) ⁻¹'
+            (Prod.map (restrictOriginal S) (restrictOriginalLatents S n) ⁻¹'
+              (cylinder Fs T ×ˢ cylinder Fl T'))) := by
+        rw [Measure.map_apply hjointE (hAmeas.prod hBmeas), hcomp]
+    _ = ((Q.law : Measure (RelStructure S (PoolVertex S) × PooledRankLatentSpace S n)).map
+          (Prod.map (RelStructure.relabel ρ) (pooledRankLatentRelabel ρ n)))
+            (Prod.map (restrictOriginal S) (restrictOriginalLatents S n) ⁻¹'
+              (cylinder Fs T ×ˢ cylinder Fl T')) :=
+        (Measure.map_apply hRhoMeas (hOvMeas (hAmeas.prod hBmeas))).symm
+    _ = (Q.law : Measure (RelStructure S (PoolVertex S) × PooledRankLatentSpace S n))
+          (Prod.map (restrictOriginal S) (restrictOriginalLatents S n) ⁻¹'
+            (cylinder Fs T ×ˢ cylinder Fl T')) := by rw [Q.invariant ρ]
+    _ = C.P (cylinder Fs T ×ˢ cylinder Fl T') := by
+        rw [← Measure.map_apply hOvMeas (hAmeas.prod hBmeas), Q.map_restrictOriginal]
+
+/-! ### The transport characterization -/
+
+/-- **Transport characterization**: identifying the pooled carrier with the original one by
+`poolVertexEquiv` carries *any* pooled rank extension back to the representation, jointly. This is
+the organizing theorem at the canonical embedding, and it is stated before recovery or screening
+deliberately — it isolates the map directions while the claim is still just an equality of joint
+laws. -/
+theorem PooledRankExtension.map_poolVertexEquiv {C : M.RankRepresentation n}
+    (Q : PooledRankExtension C) :
+    (Q.law : Measure (RelStructure S (PoolVertex S) × PooledRankLatentSpace S n)).map
+        (Prod.map (RelStructure.restrict fun s => (poolVertexEquiv S s).symm.toEmbedding)
+          (latentRestrictOver (fun s => (poolVertexEquiv S s).symm.toEmbedding) n)) = C.P :=
+  Q.map_restrict_embedding _
+
+/-- **Any two pooled rank extensions agree after the canonical identification.** Both are carried
+to the same representation, so the pooled object is unique as far as that identification sees. -/
+theorem PooledRankExtension.map_poolVertexEquiv_congr {C : M.RankRepresentation n}
+    (Q Q' : PooledRankExtension C) :
+    (Q.law : Measure (RelStructure S (PoolVertex S) × PooledRankLatentSpace S n)).map
+        (Prod.map (RelStructure.restrict fun s => (poolVertexEquiv S s).symm.toEmbedding)
+          (latentRestrictOver (fun s => (poolVertexEquiv S s).symm.toEmbedding) n)) =
+      (Q'.law : Measure (RelStructure S (PoolVertex S) × PooledRankLatentSpace S n)).map
+        (Prod.map (RelStructure.restrict fun s => (poolVertexEquiv S s).symm.toEmbedding)
+          (latentRestrictOver (fun s => (poolVertexEquiv S s).symm.toEmbedding) n)) := by
+  rw [Q.map_poolVertexEquiv, Q'.map_poolVertexEquiv]
+
+/-- The cheap extension satisfies the joint restriction theorem, for every embedding. -/
+theorem RankRepresentation.pooledExtension_map_restrict_embedding (C : M.RankRepresentation n)
+    (e : ∀ s, Vinfinite S s ↪ PoolVertex S s) :
+    ((C.pooledExtension).law :
+        Measure (RelStructure S (PoolVertex S) × PooledRankLatentSpace S n)).map
+      (Prod.map (RelStructure.restrict e) (latentRestrictOver e n)) = C.P :=
+  (C.pooledExtension).map_restrict_embedding e
+
+end InfiniteRelExchangeableLaw
+
+end RelSignature
diff --git a/scripts/axiom_audit.lean b/scripts/axiom_audit.lean
index ea2971f..0b9a9c5 100644
--- a/scripts/axiom_audit.lean
+++ b/scripts/axiom_audit.lean
@@ -309,6 +309,13 @@ custom axioms. Target list and policy: `scripts/check_census_and_axioms.py`
 #print axioms RelSignature.latentRestrictOver_comp
 #print axioms RelSignature.latentRestrictOver_latentRelabelOver_conj
 #print axioms RelSignature.InfiniteRelExchangeableLaw.RankRepresentation.pooledExtension
+
+-- R4 converse (#107): the joint restriction theorem for a pooled extension (gate 1a, stage 3).
+#print axioms exists_perm_extend_of_injOn
+#print axioms RelSignature.latentIndexEmbed_eq_of_agree
+#print axioms RelSignature.InfiniteRelExchangeableLaw.exists_poolPerm_agree
+#print axioms RelSignature.InfiniteRelExchangeableLaw.PooledRankExtension.map_restrict_embedding
+#print axioms RelSignature.InfiniteRelExchangeableLaw.PooledRankExtension.map_poolVertexEquiv
 #print axioms MeasureTheory.condExp_comp_measurePreserving
 #print axioms ProbabilityTheory.condExp_set_comp_measurePreserving
 #print axioms ProbabilityTheory.condIndepFun_comp_measurePreserving
diff --git a/scripts/check_census_and_axioms.py b/scripts/check_census_and_axioms.py
index b5ff23c..b317773 100644
--- a/scripts/check_census_and_axioms.py
+++ b/scripts/check_census_and_axioms.py
@@ -276,6 +276,11 @@
     "RelSignature.latentRestrictOver_comp",
     "RelSignature.latentRestrictOver_latentRelabelOver_conj",
     "RelSignature.InfiniteRelExchangeableLaw.RankRepresentation.pooledExtension",
+    "exists_perm_extend_of_injOn",
+    "RelSignature.latentIndexEmbed_eq_of_agree",
+    "RelSignature.InfiniteRelExchangeableLaw.exists_poolPerm_agree",
+    "RelSignature.InfiniteRelExchangeableLaw.PooledRankExtension.map_restrict_embedding",
+    "RelSignature.InfiniteRelExchangeableLaw.PooledRankExtension.map_poolVertexEquiv",
     "MeasureTheory.condExp_comp_measurePreserving",
     "ProbabilityTheory.condExp_set_comp_measurePreserving",
     "ProbabilityTheory.condIndepFun_comp_measurePreserving",

From d313275c6e0dfc95ac2d2cfc68d9fa147400e775 Mon Sep 17 00:00:00 2001
From: Cameron Freer <cameronfreer@gmail.com>
Date: Sat, 15 Aug 2026 18:23:58 +0000
Subject: [PATCH 03/13] =?UTF-8?q?feat:=20canonical=20law=20identity=20?=
 =?UTF-8?q?=E2=80=94=20every=20pooled=20rank=20extension=20is=20the=20chea?=
 =?UTF-8?q?p=20one=20(#195=20stage=203)?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Bundles the canonical restriction at poolVertexEquiv.symm as the
measurable equivalence pooledJointEquiv and cancels its pushforward,
upgrading map_poolVertexEquiv_congr to the uncancelled equality

  PooledRankExtension.law_eq : Q.law = (C.pooledExtension).law

so marginals, StationaryExtension, recovery and screening become
transports of statements about C.P through one canonical identity rather
than four bespoke measure arguments.

Supporting carrier-generic machinery: latentIndexCongr (index bijection
from a carrier equivalence, via latentIndexEmbed_comp and the identity
embedding) and latentCongrOver (its measurable equivalence on the cube),
both proved with abstract carriers. Audit 389 -> 391.
---
 Graphon.lean                       |  2 +-
 Graphon/RelLatentGeometry.lean     | 46 ++++++++++++++++++++++++++++++
 Graphon/RelPooledAcceptance.lean   | 40 ++++++++++++++++++++++++++
 scripts/axiom_audit.lean           |  2 ++
 scripts/check_census_and_axioms.py |  2 ++
 5 files changed, 91 insertions(+), 1 deletion(-)

diff --git a/Graphon.lean b/Graphon.lean
index db174f3..48a584a 100644
--- a/Graphon.lean
+++ b/Graphon.lean
@@ -264,7 +264,7 @@ in Lean 4 using Mathlib.
 * `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.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. `PooledRankExtension.map_poolVertexEquiv` is the canonical specialization, giving the transport characterization and the agreement of any two extensions after that identification
+* `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. `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.RelRankInjectionInvariance` — R4 converse (#107), the isolated proof risk of the pooled-latent extension gate: **joint invariance under arbitrary sortwise self-injections**. `RankRepresentation.invariant` is stated for *finitely supported permutations*, but a pooled object built cheaply through `poolVertexEquiv` needs the joint law invariant under every self-injection; `RankRepresentation.map_prodMap_restrict_self` supplies exactly that, so full mixed pooled invariance later costs no additional mathematics. The route is finite-cylinder extensionality on the **joint** space, which had no machinery before — rank one's joint invariance goes through only because the rank-one latent action is trivial. `rankLatentIndexInj`/`rankLatentReindex` extend the latent action from permutations to injections (only injectivity is used — a support keeps its cardinality); `exists_finSuppPerm_agree_on_finset` matches an injection to a finitely supported permutation on any finite tagged-vertex support; `ext_of_prod_cylinders` is the joint extensionality, rectangles of coordinate cylinders on both factors. **No finiteness/`Fintype` hypothesis beyond `RankRepresentation`'s ambient countability.** Equality is tested on *coordinate* cylinders — finitely many `RelCoord`s and finitely many latent indices — whose combined vertex support is one finite `Finset (Σ s, Vinfinite S s)` and so touches only finitely many sorts; the injection is matched there by extending it on each active sort, taking the identity elsewhere, and maximizing finitely many support bounds. The coarser `restrictFin` cylinder family would instead force a uniform all-sort bound that no self-injection need admit
 * `Graphon.RelRankCoding` — R4 converse piece 3 (#107): factor-law coding of the lower-rank factor. **Not** the inductive hypothesis of a working recursion: `RankCoding n → ShellProperty n` is **false**, refuted by Austin's random complete bipartite graph `X_uv = z_u ⊕ z_v` (arXiv:0801.1698 §3.6), where `lowerRankAlgebra 2` is trivial modulo the law but every triangle satisfies `X₁₂ ⊕ X₁₃ ⊕ X₂₃ = 0`, so the exact layers are pairwise but not mutually independent — while a `RankCoding 2` exists because the rank-2 factor law is a point mass. The example separates the true two-set theorem from mutuality, and shows the gap is not closable by coupling: a relatively independent joining over `lowerFactorMap` attaches latents that are conditionally independent of the structure given a trivial factor, whereas a representation needs the hidden colours, correlated with the array yet not recoverable from it. `RankCoding n` represents the rank-`n` factor by latents — a measurable coding map carrying the latent source to the factor law and intertwining the two relabeling actions **almost everywhere**. The a.e. form is forced: `lowerFactorSpaceEquiv σ n` fixes the *image* of `lowerFactorMap n`, not the whole Bool-cube, since it permutes distinct basis indices that name the same event, so the strict version is false already at rank one. `ShellProperty n` is the conclusion the recursion consumes, bundling mutual conditional independence of the exact layers over the rank-`n` supports **with** per-support locality; neither half implies the other, since mutual independence given the whole lower-rank factor permits dependence on all of it rather than only through `boundaryMap A`. `RankCoding.rankOne` is the base case, built from the #140 randomization adapter transported along `rankLatentOneEquiv`; its equivariance clause is genuinely exercised rather than vacuous, because at rank one the latent relabeling is the identity while the factor equivalence is not
 * `Graphon.RelFixingAlgebra` — R4 converse piece 2a (#107): the **law-independent** factor-algebra layer — `SortwiseFixing` (the `A`-fixing stabilizer of finitely supported sortwise permutations, closed under `1`/`*`/`⁻¹`/conjugation), the raw `RelStructure.fixingAlgebra` (events invariant under the `A`-fixing group; deliberately *not* "generated by relations inside `A`", which loses hidden vertex information), monotonicity, `fixingAlgebra_empty = invariantAlgebra` (near-definitional), and the **transport equality** `fixingAlgebra_comap_relabel : comap (relabel σ) (fixingAlgebra A) = fixingAlgebra (image σ A)` via stabilizer conjugation — no completions, no law; the conditional-independence theorem is its own later PR
diff --git a/Graphon/RelLatentGeometry.lean b/Graphon/RelLatentGeometry.lean
index e2afa18..f62b110 100644
--- a/Graphon/RelLatentGeometry.lean
+++ b/Graphon/RelLatentGeometry.lean
@@ -253,6 +253,52 @@ theorem latentIndexEmbed_eq_of_agree {e f : ∀ s, V s ↪ W s} {ρ : ∀ s, Equ
   show (⟨s, f s x⟩ : Σ s : S.Srt, W s) = ⟨s, ρ s (e s x)⟩
   rw [h ⟨s, x⟩ hv]
 
+open scoped Classical in
+/-- Restriction along the identity embedding is the identity. -/
+theorem latentIndexEmbed_refl (n : ℕ) (A : LatentIndexOver S V n) :
+    latentIndexEmbed (fun s => Function.Embedding.refl (V s)) n A = A := by
+  refine Subtype.ext ?_
+  rw [latentIndexEmbed_coe]
+  refine (Finset.image_congr fun v _ => ?_).trans A.1.image_id
+  obtain ⟨s, x⟩ := v
+  rfl
+
+/-- **The index bijection induced by a carrier equivalence.** -/
+noncomputable def latentIndexCongr (e : ∀ s, V s ≃ W s) (n : ℕ) :
+    LatentIndexOver S V n ≃ LatentIndexOver S W n where
+  toFun := latentIndexEmbed (fun s => (e s).toEmbedding) n
+  invFun := latentIndexEmbed (fun s => (e s).symm.toEmbedding) n
+  left_inv A := by
+    rw [latentIndexEmbed_comp]
+    refine Eq.trans ?_ (latentIndexEmbed_refl n A)
+    congr 1
+    funext s
+    exact Function.Embedding.ext fun x => (e s).symm_apply_apply x
+  right_inv A := by
+    rw [latentIndexEmbed_comp]
+    refine Eq.trans ?_ (latentIndexEmbed_refl n A)
+    congr 1
+    funext s
+    exact Function.Embedding.ext fun x => (e s).apply_symm_apply x
+
+/-- **Transport of the latent cube along a carrier equivalence**, as a measurable equivalence.
+Its forward map is restriction along the equivalence, so the organizing restriction theorem can be
+cancelled rather than merely stated. -/
+noncomputable def latentCongrOver (e : ∀ s, V s ≃ W s) (n : ℕ) :
+    LatentSpaceOver S W n ≃ᵐ LatentSpaceOver S V n where
+  toEquiv := Equiv.arrowCongr (latentIndexCongr e n).symm (Equiv.refl ℝ)
+  measurable_toFun := measurable_pi_lambda _ fun _ => measurable_pi_apply _
+  measurable_invFun := measurable_pi_lambda _ fun _ => measurable_pi_apply _
+
+@[simp] theorem latentCongrOver_apply (e : ∀ s, V s ≃ W s) (n : ℕ)
+    (ω : LatentSpaceOver S W n) :
+    latentCongrOver e n ω = latentRestrictOver (fun s => (e s).toEmbedding) n ω := rfl
+
+@[simp] theorem latentCongrOver_symm_apply (e : ∀ s, V s ≃ W s) (n : ℕ)
+    (ω : LatentSpaceOver S V n) :
+    (latentCongrOver e n).symm ω =
+      latentRestrictOver (fun s => (e s).symm.toEmbedding) n ω := rfl
+
 /-- **The conjugation square for a carrier equivalence** — the latent-side mirror of
 `RelStructure.congrCarrier_relabel`. Transporting along `e` intertwines a permutation of the
 source carrier with its conjugate on the target. Proved carrier-generically, so instantiating at
diff --git a/Graphon/RelPooledAcceptance.lean b/Graphon/RelPooledAcceptance.lean
index 5754931..c9c2203 100644
--- a/Graphon/RelPooledAcceptance.lean
+++ b/Graphon/RelPooledAcceptance.lean
@@ -194,6 +194,46 @@ theorem PooledRankExtension.map_poolVertexEquiv_congr {C : M.RankRepresentation
           (latentRestrictOver (fun s => (poolVertexEquiv S s).symm.toEmbedding) n)) := by
   rw [Q.map_poolVertexEquiv, Q'.map_poolVertexEquiv]
 
+/-! ### The canonical law identity -/
+
+variable (S n) in
+/-- **The canonical joint identification** of the pooled objects with the original ones, bundled as
+a measurable equivalence: `poolVertexEquiv` on the structure and its latent transport. Its forward
+map is exactly the restriction appearing in `map_poolVertexEquiv`, which is what lets that theorem
+be *cancelled* rather than merely stated. -/
+noncomputable def pooledJointEquiv :
+    (RelStructure S (PoolVertex S) × PooledRankLatentSpace S n) ≃ᵐ
+      (RelStructure S (Vinfinite S) × RankLatentSpace S n) :=
+  (RelStructure.congrCarrier fun s => poolVertexEquiv S s).prodCongr
+    (latentCongrOver (fun s => (poolVertexEquiv S s).symm) n)
+
+theorem pooledJointEquiv_coe :
+    ((pooledJointEquiv S n : _ ≃ᵐ _) : _ → _) =
+      Prod.map (RelStructure.restrict fun s => (poolVertexEquiv S s).symm.toEmbedding)
+        (latentRestrictOver (fun s => (poolVertexEquiv S s).symm.toEmbedding) n) := rfl
+
+theorem pooledJointEquiv_symm_coe :
+    (((pooledJointEquiv S n : _ ≃ᵐ _).symm : _ ≃ᵐ _) : _ → _) =
+      RankRepresentation.pooledTransport (S := S) (n := n) := rfl
+
+/-- **The canonical law identity**: a pooled rank extension is *determined* — it is the cheap one.
+Every marginal, `StationaryExtension`, recovery and screening statement about a pooled extension is
+therefore a transport of the corresponding statement about `C.P`, rather than a separate measure
+argument. -/
+theorem PooledRankExtension.law_eq {C : M.RankRepresentation n} (Q : PooledRankExtension C) :
+    (Q.law : Measure (RelStructure S (PoolVertex S) × PooledRankLatentSpace S n)) =
+      ((C.pooledExtension).law :
+        Measure (RelStructure S (PoolVertex S) × PooledRankLatentSpace S n)) := by
+  haveI := C.isProbabilityMeasure_P
+  calc (Q.law : Measure (RelStructure S (PoolVertex S) × PooledRankLatentSpace S n))
+      = ((Q.law : Measure (RelStructure S (PoolVertex S) × PooledRankLatentSpace S n)).map
+          (pooledJointEquiv S n)).map (pooledJointEquiv S n).symm :=
+        (MeasurableEquiv.map_symm_map _).symm
+    _ = C.P.map (pooledJointEquiv S n).symm := by
+        rw [pooledJointEquiv_coe, Q.map_poolVertexEquiv]
+    _ = ((C.pooledExtension).law :
+          Measure (RelStructure S (PoolVertex S) × PooledRankLatentSpace S n)) := rfl
+
 /-- The cheap extension satisfies the joint restriction theorem, for every embedding. -/
 theorem RankRepresentation.pooledExtension_map_restrict_embedding (C : M.RankRepresentation n)
     (e : ∀ s, Vinfinite S s ↪ PoolVertex S s) :
diff --git a/scripts/axiom_audit.lean b/scripts/axiom_audit.lean
index 0b9a9c5..4a7716e 100644
--- a/scripts/axiom_audit.lean
+++ b/scripts/axiom_audit.lean
@@ -316,6 +316,8 @@ custom axioms. Target list and policy: `scripts/check_census_and_axioms.py`
 #print axioms RelSignature.InfiniteRelExchangeableLaw.exists_poolPerm_agree
 #print axioms RelSignature.InfiniteRelExchangeableLaw.PooledRankExtension.map_restrict_embedding
 #print axioms RelSignature.InfiniteRelExchangeableLaw.PooledRankExtension.map_poolVertexEquiv
+#print axioms RelSignature.latentCongrOver
+#print axioms RelSignature.InfiniteRelExchangeableLaw.PooledRankExtension.law_eq
 #print axioms MeasureTheory.condExp_comp_measurePreserving
 #print axioms ProbabilityTheory.condExp_set_comp_measurePreserving
 #print axioms ProbabilityTheory.condIndepFun_comp_measurePreserving
diff --git a/scripts/check_census_and_axioms.py b/scripts/check_census_and_axioms.py
index b317773..d8fbd03 100644
--- a/scripts/check_census_and_axioms.py
+++ b/scripts/check_census_and_axioms.py
@@ -281,6 +281,8 @@
     "RelSignature.InfiniteRelExchangeableLaw.exists_poolPerm_agree",
     "RelSignature.InfiniteRelExchangeableLaw.PooledRankExtension.map_restrict_embedding",
     "RelSignature.InfiniteRelExchangeableLaw.PooledRankExtension.map_poolVertexEquiv",
+    "RelSignature.latentCongrOver",
+    "RelSignature.InfiniteRelExchangeableLaw.PooledRankExtension.law_eq",
     "MeasureTheory.condExp_comp_measurePreserving",
     "ProbabilityTheory.condExp_set_comp_measurePreserving",
     "ProbabilityTheory.condIndepFun_comp_measurePreserving",

From 89e4bdf6a9811ecce43ad47740aababee43b6a07 Mon Sep 17 00:00:00 2001
From: Cameron Freer <cameronfreer@gmail.com>
Date: Sat, 15 Aug 2026 19:31:51 +0000
Subject: [PATCH 04/13] feat: carrier-parametric observation layer with the
 transport boundary (#195 stage 3, pin 1)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

localLatentsOver / blockMapOver / restObservationOver over an arbitrary
carrier; the Vinfinite-indexed originals become compatibility aliases, so
pooled recovery and screening instantiate this core rather than
duplicating it.

The module header records the boundary that matters: local and block
observations read only coordinates supported inside a finite set and
admit naturality along an arbitrary sortwise EMBEDDING, whereas the
remainder is global — it ranges over every rank-≤n coordinate of the
ambient carrier — 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, which for the pooled setting is poolVertexEquiv.

Downstream cost of the aliasing was two simp sets that unfolded the old
definitions directly (RelSingletonPeel, RelRankOneScreening); both now
name the generic definition as well.
---
 Graphon.lean                        |   2 +
 Graphon/RelObservationGeometry.lean | 124 ++++++++++++++++++++++++++++
 Graphon/RelPooledExtension.lean     |   1 +
 Graphon/RelRankOneScreening.lean    |   4 +-
 Graphon/RelRankRepresentation.lean  |  19 +++--
 Graphon/RelSingletonPeel.lean       |   2 +-
 6 files changed, 140 insertions(+), 12 deletions(-)
 create mode 100644 Graphon/RelObservationGeometry.lean

diff --git a/Graphon.lean b/Graphon.lean
index 48a584a..a97ce3d 100644
--- a/Graphon.lean
+++ b/Graphon.lean
@@ -44,6 +44,7 @@ import Graphon.RelRankCoding
 import Graphon.RelRankRepresentation
 import Graphon.RelRankInjectionInvariance
 import Graphon.RelLatentGeometry
+import Graphon.RelObservationGeometry
 import Graphon.RelPooledLatents
 import Graphon.RelPooledExtension
 import Graphon.RelPooledAcceptance
@@ -262,6 +263,7 @@ in Lean 4 using Mathlib.
 * `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. `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
diff --git a/Graphon/RelObservationGeometry.lean b/Graphon/RelObservationGeometry.lean
new file mode 100644
index 0000000..60950f4
--- /dev/null
+++ b/Graphon/RelObservationGeometry.lean
@@ -0,0 +1,124 @@
+/-
+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.RelLatentGeometry
+import Graphon.RelEqualityPattern
+
+/-!
+# Carrier-parametric observation layer (R4 converse, #107)
+
+The observations used by recovery and screening — local latents, blocks of raw relation
+coordinates, and the rank-truncated remainder — over an **arbitrary sortwise carrier**. The
+`Vinfinite`-indexed originals become compatibility aliases, and the pooled statements instantiate
+this core rather than introducing parallel pooled definitions.
+
+## The transport boundary
+
+The three observations do **not** transport equally well, and the difference is a matter of truth,
+not of proof effort:
+
+* `localLatentsOver` and `blockMapOver` are **local** — they read only coordinates supported inside
+  a given finite set — so they admit naturality along an arbitrary sortwise **embedding** of
+  carriers: an embedding restricts to a bijection between the supports inside `A` and those inside
+  its image.
+* `restObservationOver` is **global**: its remainder ranges over *every* rank-`≤ n` coordinate of
+  the ambient carrier other than the one at `A`. Along an embedding into a larger carrier the
+  target remainder sees coordinates outside the image, which the source remainder cannot, so an
+  embedding-level commuting law would be **false**. It transports only along a carrier
+  **equivalence**.
+
+Screening therefore transports along the canonical `poolVertexEquiv`, which the pooled uniqueness
+identity makes available; recovery, being local, is free to use embeddings.
+-/
+
+open MeasureTheory
+
+namespace RelSignature
+
+universe u v
+
+variable {S : RelSignature.{u}} {V W : S.Srt → Type v}
+
+/-! ### Local latents -/
+
+/-- The latent coordinates visible at `A`: supports contained in `A`. -/
+def LocalLatentIndexOver (V : S.Srt → Type v) (A : Finset (Σ s : S.Srt, V s)) (n : ℕ) :=
+  {B : LatentIndexOver S V n // B.1 ⊆ A}
+
+instance [Countable S.Srt] [∀ s, Countable (V s)] (A : Finset (Σ s : S.Srt, V s)) (n : ℕ) :
+    Countable (LocalLatentIndexOver V A n) := Subtype.countable
+
+/-- The local latent space at `A`. -/
+abbrev LocalLatentSpaceOver (V : S.Srt → Type v) (A : Finset (Σ s : S.Srt, V s)) (n : ℕ) :=
+  LocalLatentIndexOver V A n → ℝ
+
+/-- Restriction of the latent array to the coordinates visible at `A`. -/
+def localLatentsOver (A : Finset (Σ s : S.Srt, V s)) (n : ℕ) :
+    LatentSpaceOver S V n → LocalLatentSpaceOver V A n := fun ω B => ω B.1
+
+theorem measurable_localLatentsOver (A : Finset (Σ s : S.Srt, V s)) (n : ℕ) :
+    Measurable (localLatentsOver (S := S) A n) :=
+  measurable_pi_lambda _ fun _ => measurable_pi_apply _
+
+/-! ### Blocks of raw relation coordinates -/
+
+open scoped Classical in
+/-- Raw relation coordinates whose tagged support is exactly `A`. -/
+def BlockIndexOver (V : S.Srt → Type v) (A : Finset (Σ s : S.Srt, V s)) :=
+  {c : RelCoord S V // c.support = A}
+
+open scoped Classical in
+instance [Countable S.Rel] [∀ s, Countable (V s)] (A : Finset (Σ s : S.Srt, V s)) :
+    Countable (BlockIndexOver V A) := Subtype.countable
+
+open scoped Classical in
+/-- The block of the structure at `A`. -/
+abbrev BlockSpaceOver (V : S.Srt → Type v) (A : Finset (Σ s : S.Srt, V s)) :=
+  BlockIndexOver V A → Bool
+
+open scoped Classical in
+/-- Read the block at `A` off a structure. -/
+def blockMapOver (A : Finset (Σ s : S.Srt, V s)) :
+    RelStructure S V → BlockSpaceOver V A := fun X c => X c.1
+
+open scoped Classical in
+theorem measurable_blockMapOver [Countable S.Rel] [∀ s, Countable (V s)]
+    (A : Finset (Σ s : S.Srt, V s)) :
+    Measurable (blockMapOver (S := S) A) :=
+  measurable_pi_lambda _ fun _ => measurable_pi_apply _
+
+/-! ### The rank-truncated remainder
+
+Global, hence transportable only along carrier equivalences — see the module header. -/
+
+open scoped Classical in
+/-- Coordinates of rank at most `n` other than those at `A`. -/
+def RestIndexOver (V : S.Srt → Type v) (n : ℕ) (A : Finset (Σ s : S.Srt, V s)) :=
+  {c : RelCoord S V // c.support.card ≤ n ∧ c.support ≠ A}
+
+open scoped Classical in
+instance [Countable S.Rel] [∀ s, Countable (V s)] (n : ℕ) (A : Finset (Σ s : S.Srt, V s)) :
+    Countable (RestIndexOver V n A) := Subtype.countable
+
+open scoped Classical in
+/-- The remaining rank-`≤ n` structure. -/
+abbrev RestSpaceOver (V : S.Srt → Type v) (n : ℕ) (A : Finset (Σ s : S.Srt, V s)) :=
+  RestIndexOver V n A → Bool
+
+open scoped Classical in
+/-- **The rank-truncated remainder observation** over a carrier: the other blocks of rank at most
+`n`, together with the whole latent array. -/
+def restObservationOver (n : ℕ) (A : Finset (Σ s : S.Srt, V s)) :
+    RelStructure S V × LatentSpaceOver S V n →
+      RestSpaceOver V n A × LatentSpaceOver S V n :=
+  fun p => (fun c => p.1 c.1, p.2)
+
+open scoped Classical in
+theorem measurable_restObservationOver [Countable S.Rel] [∀ s, Countable (V s)] (n : ℕ)
+    (A : Finset (Σ s : S.Srt, V s)) :
+    Measurable (restObservationOver (S := S) n A) :=
+  (measurable_pi_lambda _ fun _ => measurable_fst.eval).prodMk measurable_snd
+
+end RelSignature
diff --git a/Graphon/RelPooledExtension.lean b/Graphon/RelPooledExtension.lean
index c38cec2..f35e045 100644
--- a/Graphon/RelPooledExtension.lean
+++ b/Graphon/RelPooledExtension.lean
@@ -77,6 +77,7 @@ noncomputable def pooledTransport :
   Prod.map (RelStructure.congrCarrier fun s => (poolVertexEquiv S s).symm)
     (latentRestrictOver (fun s => (poolVertexEquiv S s).toEmbedding) n)
 
+omit [Countable S.Srt] [Countable S.Rel] in
 theorem measurable_pooledTransport :
     Measurable (pooledTransport (S := S) (n := n)) :=
   (RelStructure.congrCarrier _).measurable.prodMap
diff --git a/Graphon/RelRankOneScreening.lean b/Graphon/RelRankOneScreening.lean
index d55ed03..ba1b0dd 100644
--- a/Graphon/RelRankOneScreening.lean
+++ b/Graphon/RelRankOneScreening.lean
@@ -188,9 +188,9 @@ theorem condIndepFun_blockMap_restObservation_one {S : RelSignature.{u}}
     refine Prod.ext ?_ rfl
     funext c
     by_cases hc : c.1.support = ∅
-    · simp only [restObservation, dif_pos hc]
+    · simp only [restObservation, restObservationOver, dif_pos hc]
       exact congrFun hp ⟨c.1, hc⟩
-    · simp only [restObservation, dif_neg hc]
+    · simp only [restObservation, restObservationOver, dif_neg hc]
   -- assemble
   have h3 := condIndep_of_condIndep_of_le_right h2 (measurable_iff_comap_le.mp hR'measJ)
   have h4 := (condIndepFun_iff_condIndep _ _ (singletonBlockRead S v₀) R' P).mpr h3
diff --git a/Graphon/RelRankRepresentation.lean b/Graphon/RelRankRepresentation.lean
index 99dfb87..4466904 100644
--- a/Graphon/RelRankRepresentation.lean
+++ b/Graphon/RelRankRepresentation.lean
@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Cameron Freer
 -/
 import Graphon.RelRankLatents
+import Graphon.RelObservationGeometry
 import Graphon.RelEqualityPattern
 import Graphon.RelInfiniteLaw
 
@@ -70,8 +71,8 @@ variable {S : RelSignature}
 
 /-- The latent coordinates visible at `A`: supports contained in `A`. Within `RankLatentIndex n`
 this automatically means *proper* subsets when `A.card = n`. -/
-def LocalLatentIndex (A : Finset (Σ s : S.Srt, Vinfinite S s)) (n : ℕ) :=
-  {B : RankLatentIndex S n // B.1 ⊆ A}
+@[reducible] def LocalLatentIndex (A : Finset (Σ s : S.Srt, Vinfinite S s)) (n : ℕ) :=
+  LocalLatentIndexOver (Vinfinite S) A n
 
 instance [Countable S.Srt] (A : Finset (Σ s : S.Srt, Vinfinite S s)) (n : ℕ) :
     Countable (LocalLatentIndex A n) := Subtype.countable
@@ -82,7 +83,7 @@ abbrev LocalLatentSpace (A : Finset (Σ s : S.Srt, Vinfinite S s)) (n : ℕ) :=
 
 /-- Restriction of the latent array to the coordinates visible at `A`. -/
 def localLatents (A : Finset (Σ s : S.Srt, Vinfinite S s)) (n : ℕ) :
-    RankLatentSpace S n → LocalLatentSpace A n := fun ω B => ω B.1
+    RankLatentSpace S n → LocalLatentSpace A n := localLatentsOver A n
 
 theorem measurable_localLatents [Countable S.Srt]
     (A : Finset (Σ s : S.Srt, Vinfinite S s)) (n : ℕ) :
@@ -107,8 +108,8 @@ theorem rankLatentIndex_ssubset_of_card_eq {A : Finset (Σ s : S.Srt, Vinfinite
 open scoped Classical in
 /-- Raw relation coordinates whose tagged support is exactly `A`. Raw coordinates, not basis
 events: the eventual descent to label-free kernels is indexed by these. -/
-def BlockIndex (A : Finset (Σ s : S.Srt, Vinfinite S s)) :=
-  {c : RelCoord S (Vinfinite S) // c.support = A}
+@[reducible] def BlockIndex (A : Finset (Σ s : S.Srt, Vinfinite S s)) :=
+  BlockIndexOver (Vinfinite S) A
 
 open scoped Classical in
 instance [Countable S.Rel] (A : Finset (Σ s : S.Srt, Vinfinite S s)) :
@@ -121,7 +122,7 @@ abbrev BlockSpace (A : Finset (Σ s : S.Srt, Vinfinite S s)) := BlockIndex A →
 open scoped Classical in
 /-- Read the block at `A` off a structure. -/
 def blockMap (A : Finset (Σ s : S.Srt, Vinfinite S s)) :
-    RelStructure S (Vinfinite S) → BlockSpace A := fun X c => X c.1
+    RelStructure S (Vinfinite S) → BlockSpace A := blockMapOver A
 
 open scoped Classical in
 theorem measurable_blockMap [Countable S.Rel] (A : Finset (Σ s : S.Srt, Vinfinite S s)) :
@@ -134,8 +135,8 @@ open scoped Classical in
 /-- Coordinates of rank at most `n` other than those at `A`. The truncation is essential:
 coordinates of rank above `n` that contain `A` legitimately share `A`'s latents, so screening
 against them would be false. -/
-def RestIndex (n : ℕ) (A : Finset (Σ s : S.Srt, Vinfinite S s)) :=
-  {c : RelCoord S (Vinfinite S) // c.support.card ≤ n ∧ c.support ≠ A}
+@[reducible] def RestIndex (n : ℕ) (A : Finset (Σ s : S.Srt, Vinfinite S s)) :=
+  RestIndexOver (Vinfinite S) n A
 
 open scoped Classical in
 instance [Countable S.Rel] (n : ℕ) (A : Finset (Σ s : S.Srt, Vinfinite S s)) :
@@ -150,7 +151,7 @@ open scoped Classical in
 with the whole latent array — which at rank `n` contains no coordinate at `A`. -/
 def restObservation (n : ℕ) (A : Finset (Σ s : S.Srt, Vinfinite S s)) :
     RelStructure S (Vinfinite S) × RankLatentSpace S n → RestSpace n A × RankLatentSpace S n :=
-  fun p => (fun c => p.1 c.1, p.2)
+  restObservationOver n A
 
 open scoped Classical in
 theorem measurable_restObservation [Countable S.Rel] (n : ℕ)
diff --git a/Graphon/RelSingletonPeel.lean b/Graphon/RelSingletonPeel.lean
index 15070f1..6a529e1 100644
--- a/Graphon/RelSingletonPeel.lean
+++ b/Graphon/RelSingletonPeel.lean
@@ -75,7 +75,7 @@ theorem measurable_blockMap_fixingAlgebra [Countable S.Rel]
   refine measurable_pi_iff.mpr fun c => measurable_to_bool ?_
   convert key c.1 c.2 using 1
   ext X
-  simp [blockMap]
+  simp [blockMap, blockMapOver]
 
 namespace InfiniteRelExchangeableLaw
 

From f7b86094bb6334a98928e1738fa77de26267980d Mon Sep 17 00:00:00 2001
From: Cameron Freer <cameronfreer@gmail.com>
Date: Sat, 15 Aug 2026 21:31:38 +0000
Subject: [PATCH 05/13] feat: measure-preserving canonical equivalence +
 support transport (#195 stage 3)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

measurePreserving_pooledJointEquiv packages the canonical identification
as measure-preserving from Q.law to C.P — the handle that lets
condIndepFun_comp_measurePreserving pull C.screening BACK to the pooled
law, so conditional independence is never pushed forward and no further
conditional-expectation theorem is needed.

supportImage and latentIndexEmbed_subset_supportImage_iff are the
bijection underlying local naturality: an embedding restricts to a
bijection between supports inside A and those inside its image. Stated as
an equivalence with pointwise lemmas first, per review, which also keeps
the proof on Function.Injective.mem_finset_image rather than dependent
sigma destructuring.
---
 Graphon/RelObservationGeometry.lean | 38 +++++++++++++++++++++++++++++
 Graphon/RelPooledAcceptance.lean    | 11 +++++++++
 scripts/axiom_audit.lean            |  2 ++
 scripts/check_census_and_axioms.py  |  2 ++
 4 files changed, 53 insertions(+)

diff --git a/Graphon/RelObservationGeometry.lean b/Graphon/RelObservationGeometry.lean
index 60950f4..67115e7 100644
--- a/Graphon/RelObservationGeometry.lean
+++ b/Graphon/RelObservationGeometry.lean
@@ -121,4 +121,42 @@ theorem measurable_restObservationOver [Countable S.Rel] [∀ s, Countable (V s)
     Measurable (restObservationOver (S := S) n A) :=
   (measurable_pi_lambda _ fun _ => measurable_fst.eval).prodMk measurable_snd
 
+/-! ### Support and index transport
+
+Equivalences first, with pointwise `_apply` lemmas; the function-level naturality laws are derived
+from these. Keeping the bijections primitive is what limits coercion and `DecidableEq` friction. -/
+
+open scoped Classical in
+/-- The image of a support under a sortwise embedding of carriers. -/
+noncomputable def supportImage (e : ∀ s, V s ↪ W s) (A : Finset (Σ s : S.Srt, V s)) :
+    Finset (Σ s : S.Srt, W s) :=
+  A.image (Sigma.map id fun s => ⇑(e s))
+
+theorem injective_sigmaMap (e : ∀ s, V s ↪ W s) :
+    Function.Injective (Sigma.map id fun s => ⇑(e s) : (Σ s : S.Srt, V s) → Σ s : S.Srt, W s) :=
+  Function.injective_id.sigma_map fun s => (e s).injective
+
+open scoped Classical in
+@[simp] theorem mem_supportImage_map {e : ∀ s, V s ↪ W s} {A : Finset (Σ s : S.Srt, V s)}
+    {v : Σ s : S.Srt, V s} :
+    Sigma.map id (fun s => ⇑(e s)) v ∈ supportImage e A ↔ v ∈ A :=
+  (injective_sigmaMap e).mem_finset_image
+
+open scoped Classical in
+/-- **A support lies inside `A` exactly when its image lies inside the image of `A`.** This is the
+bijection underlying local naturality: an embedding restricts to a bijection between the supports
+inside `A` and those inside its image. -/
+theorem latentIndexEmbed_subset_supportImage_iff (e : ∀ s, V s ↪ W s)
+    {A : Finset (Σ s : S.Srt, V s)} {n : ℕ} (B : LatentIndexOver S V n) :
+    (latentIndexEmbed e n B).1 ⊆ supportImage e A ↔ B.1 ⊆ A := by
+  classical
+  rw [latentIndexEmbed_coe, supportImage]
+  constructor
+  · intro h v hv
+    have hmem := h (Finset.mem_image_of_mem (Sigma.map id fun s => ⇑(e s)) hv)
+    rwa [(injective_sigmaMap e).mem_finset_image] at hmem
+  · intro h w hw
+    obtain ⟨v, hv, rfl⟩ := Finset.mem_image.mp hw
+    exact Finset.mem_image_of_mem _ (h hv)
+
 end RelSignature
diff --git a/Graphon/RelPooledAcceptance.lean b/Graphon/RelPooledAcceptance.lean
index c9c2203..6503881 100644
--- a/Graphon/RelPooledAcceptance.lean
+++ b/Graphon/RelPooledAcceptance.lean
@@ -234,6 +234,17 @@ theorem PooledRankExtension.law_eq {C : M.RankRepresentation n} (Q : PooledRankE
     _ = ((C.pooledExtension).law :
           Measure (RelStructure S (PoolVertex S) × PooledRankLatentSpace S n)) := rfl
 
+/-- **The canonical identification is measure-preserving** from a pooled extension to the
+representation. This is the handle for transporting conditional-independence statements: composing
+with a measure-preserving map pulls `C.P`-statements *back* to `Q.law`, so nothing has to be pushed
+forward and no further conditional-expectation theorem is needed. -/
+theorem PooledRankExtension.measurePreserving_pooledJointEquiv {C : M.RankRepresentation n}
+    (Q : PooledRankExtension C) :
+    MeasurePreserving (pooledJointEquiv S n)
+      (Q.law : Measure (RelStructure S (PoolVertex S) × PooledRankLatentSpace S n)) C.P :=
+  ⟨(pooledJointEquiv S n).measurable, by
+    rw [pooledJointEquiv_coe]; exact Q.map_poolVertexEquiv⟩
+
 /-- The cheap extension satisfies the joint restriction theorem, for every embedding. -/
 theorem RankRepresentation.pooledExtension_map_restrict_embedding (C : M.RankRepresentation n)
     (e : ∀ s, Vinfinite S s ↪ PoolVertex S s) :
diff --git a/scripts/axiom_audit.lean b/scripts/axiom_audit.lean
index 4a7716e..f12f350 100644
--- a/scripts/axiom_audit.lean
+++ b/scripts/axiom_audit.lean
@@ -318,6 +318,8 @@ custom axioms. Target list and policy: `scripts/check_census_and_axioms.py`
 #print axioms RelSignature.InfiniteRelExchangeableLaw.PooledRankExtension.map_poolVertexEquiv
 #print axioms RelSignature.latentCongrOver
 #print axioms RelSignature.InfiniteRelExchangeableLaw.PooledRankExtension.law_eq
+#print axioms RelSignature.latentIndexEmbed_subset_supportImage_iff
+#print axioms RelSignature.InfiniteRelExchangeableLaw.PooledRankExtension.measurePreserving_pooledJointEquiv
 #print axioms MeasureTheory.condExp_comp_measurePreserving
 #print axioms ProbabilityTheory.condExp_set_comp_measurePreserving
 #print axioms ProbabilityTheory.condIndepFun_comp_measurePreserving
diff --git a/scripts/check_census_and_axioms.py b/scripts/check_census_and_axioms.py
index d8fbd03..17782ea 100644
--- a/scripts/check_census_and_axioms.py
+++ b/scripts/check_census_and_axioms.py
@@ -283,6 +283,8 @@
     "RelSignature.InfiniteRelExchangeableLaw.PooledRankExtension.map_poolVertexEquiv",
     "RelSignature.latentCongrOver",
     "RelSignature.InfiniteRelExchangeableLaw.PooledRankExtension.law_eq",
+    "RelSignature.latentIndexEmbed_subset_supportImage_iff",
+    "RelSignature.InfiniteRelExchangeableLaw.PooledRankExtension.measurePreserving_pooledJointEquiv",
     "MeasureTheory.condExp_comp_measurePreserving",
     "ProbabilityTheory.condExp_set_comp_measurePreserving",
     "ProbabilityTheory.condIndepFun_comp_measurePreserving",

From 9f3a4e98945c7ecf108c5cb38b20e9e2f558b8f4 Mon Sep 17 00:00:00 2001
From: Cameron Freer <cameronfreer@gmail.com>
Date: Sun, 16 Aug 2026 00:41:18 +0000
Subject: [PATCH 06/13] feat: bundled coordinate carrier equivalence (#195
 stage 3)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

RelCoord.congrCarrier, the coordinate mirror of RelStructure.congrCarrier
— the repository had RelCoord.map and support_map but no bundled
equivalence. The remainder index is global, so its transport needs a
genuine equivalence of coordinates rather than an embedding, and this is
the reuse point for it. support_congrCarrier records that transport
carries a support to its image.
---
 Graphon/RelObservationGeometry.lean | 30 +++++++++++++++++++++++++++++
 scripts/axiom_audit.lean            |  1 +
 scripts/check_census_and_axioms.py  |  1 +
 3 files changed, 32 insertions(+)

diff --git a/Graphon/RelObservationGeometry.lean b/Graphon/RelObservationGeometry.lean
index 67115e7..f572556 100644
--- a/Graphon/RelObservationGeometry.lean
+++ b/Graphon/RelObservationGeometry.lean
@@ -121,6 +121,28 @@ theorem measurable_restObservationOver [Countable S.Rel] [∀ s, Countable (V s)
     Measurable (restObservationOver (S := S) n A) :=
   (measurable_pi_lambda _ fun _ => measurable_fst.eval).prodMk measurable_snd
 
+/-! ### Coordinate transport along a carrier equivalence
+
+The coordinate mirror of `RelStructure.congrCarrier`, bundled once here: the remainder index is
+global, so its transport needs a genuine equivalence of coordinates rather than an embedding. -/
+
+/-- **Transport of relation coordinates along a sortwise equivalence of carriers**, bundled. -/
+def RelCoord.congrCarrier (e : ∀ s, V s ≃ W s) : RelCoord S V ≃ RelCoord S W where
+  toFun := RelCoord.map fun s => ⇑(e s)
+  invFun := RelCoord.map fun s => ⇑(e s).symm
+  left_inv c := by
+    refine congrArg (fun w => (⟨c.1, w⟩ : RelCoord S V)) (funext fun i => ?_)
+    exact (e _).symm_apply_apply (c.2 i)
+  right_inv c := by
+    refine congrArg (fun w => (⟨c.1, w⟩ : RelCoord S W)) (funext fun i => ?_)
+    exact (e _).apply_symm_apply (c.2 i)
+
+@[simp] theorem RelCoord.congrCarrier_apply (e : ∀ s, V s ≃ W s) (c : RelCoord S V) :
+    RelCoord.congrCarrier e c = RelCoord.map (fun s => ⇑(e s)) c := rfl
+
+@[simp] theorem RelCoord.congrCarrier_symm_apply (e : ∀ s, V s ≃ W s) (c : RelCoord S W) :
+    (RelCoord.congrCarrier e).symm c = RelCoord.map (fun s => ⇑(e s).symm) c := rfl
+
 /-! ### Support and index transport
 
 Equivalences first, with pointwise `_apply` lemmas; the function-level naturality laws are derived
@@ -159,4 +181,12 @@ theorem latentIndexEmbed_subset_supportImage_iff (e : ∀ s, V s ↪ W s)
     obtain ⟨v, hv, rfl⟩ := Finset.mem_image.mp hw
     exact Finset.mem_image_of_mem _ (h hv)
 
+open scoped Classical in
+/-- Transporting a coordinate carries its support to the image of that support. -/
+theorem RelCoord.support_congrCarrier (e : ∀ s, V s ≃ W s) (c : RelCoord S V) :
+    (RelCoord.congrCarrier e c).support =
+      supportImage (fun s => (e s).toEmbedding) c.support := by
+  rw [RelCoord.congrCarrier_apply, RelCoord.support_map, supportImage]
+  rfl
+
 end RelSignature
diff --git a/scripts/axiom_audit.lean b/scripts/axiom_audit.lean
index f12f350..de740ac 100644
--- a/scripts/axiom_audit.lean
+++ b/scripts/axiom_audit.lean
@@ -318,6 +318,7 @@ custom axioms. Target list and policy: `scripts/check_census_and_axioms.py`
 #print axioms RelSignature.InfiniteRelExchangeableLaw.PooledRankExtension.map_poolVertexEquiv
 #print axioms RelSignature.latentCongrOver
 #print axioms RelSignature.InfiniteRelExchangeableLaw.PooledRankExtension.law_eq
+#print axioms RelSignature.RelCoord.support_congrCarrier
 #print axioms RelSignature.latentIndexEmbed_subset_supportImage_iff
 #print axioms RelSignature.InfiniteRelExchangeableLaw.PooledRankExtension.measurePreserving_pooledJointEquiv
 #print axioms MeasureTheory.condExp_comp_measurePreserving
diff --git a/scripts/check_census_and_axioms.py b/scripts/check_census_and_axioms.py
index 17782ea..b3247d2 100644
--- a/scripts/check_census_and_axioms.py
+++ b/scripts/check_census_and_axioms.py
@@ -283,6 +283,7 @@
     "RelSignature.InfiniteRelExchangeableLaw.PooledRankExtension.map_poolVertexEquiv",
     "RelSignature.latentCongrOver",
     "RelSignature.InfiniteRelExchangeableLaw.PooledRankExtension.law_eq",
+    "RelSignature.RelCoord.support_congrCarrier",
     "RelSignature.latentIndexEmbed_subset_supportImage_iff",
     "RelSignature.InfiniteRelExchangeableLaw.PooledRankExtension.measurePreserving_pooledJointEquiv",
     "MeasureTheory.condExp_comp_measurePreserving",

From 04d7ca999ba506181f45d07d6f9083a76b98bfa5 Mon Sep 17 00:00:00 2001
From: Cameron Freer <cameronfreer@gmail.com>
Date: Sun, 16 Aug 2026 02:01:09 +0000
Subject: [PATCH 07/13] feat: conditioning-algebra invariance + bundled
 remainder equivalence (#195 stage 3)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

comap_measurableEquiv_comp: postcomposing an observation with a
measurable EQUIVALENCE leaves the generated comap sigma-algebra
unchanged. Named so the screening assembly can straighten a transported
conditioning map without a further probabilistic lemma — measurability in
both directions is exactly what makes the comap survive.

restSpaceCongr bundles the remainder transport as a measurable
equivalence (not merely an index bijection), built on RelCoord.congrCarrier
and requiring a carrier EQUIVALENCE, since the remainder ranges over every
rank-≤n coordinate of the ambient carrier.
---
 Graphon/RelObservationGeometry.lean | 77 +++++++++++++++++++++++++++++
 scripts/axiom_audit.lean            |  2 +
 scripts/check_census_and_axioms.py  |  2 +
 3 files changed, 81 insertions(+)

diff --git a/Graphon/RelObservationGeometry.lean b/Graphon/RelObservationGeometry.lean
index f572556..a1b9f9f 100644
--- a/Graphon/RelObservationGeometry.lean
+++ b/Graphon/RelObservationGeometry.lean
@@ -121,6 +121,19 @@ theorem measurable_restObservationOver [Countable S.Rel] [∀ s, Countable (V s)
     Measurable (restObservationOver (S := S) n A) :=
   (measurable_pi_lambda _ fun _ => measurable_fst.eval).prodMk measurable_snd
 
+/-! ### Reindexing does not move the conditioning algebra
+
+Screening conditions on a σ-algebra generated by an observation map. Transporting the observation
+through a measurable *equivalence* of codomains leaves that σ-algebra unchanged — measurability in
+both directions is exactly what makes the comap survive. Named here so the screening assembly can
+straighten a transported conditioning map without a further probabilistic lemma. -/
+
+/-- **Postcomposition with a measurable equivalence does not change the generated σ-algebra.** -/
+theorem comap_measurableEquiv_comp {Ω α β : Type*} [MeasurableSpace α] [MeasurableSpace β]
+    (φ : α ≃ᵐ β) (f : Ω → α) :
+    MeasurableSpace.comap (⇑φ ∘ f) inferInstance = MeasurableSpace.comap f inferInstance := by
+  rw [← MeasurableSpace.comap_comp, φ.measurableEmbedding.comap_eq]
+
 /-! ### Coordinate transport along a carrier equivalence
 
 The coordinate mirror of `RelStructure.congrCarrier`, bundled once here: the remainder index is
@@ -189,4 +202,68 @@ theorem RelCoord.support_congrCarrier (e : ∀ s, V s ≃ W s) (c : RelCoord S V
   rw [RelCoord.congrCarrier_apply, RelCoord.support_map, supportImage]
   rfl
 
+/-! ### The remainder transports along a carrier equivalence
+
+Bundled as a measurable equivalence, not merely an index bijection, so that the screening assembly
+can straighten the transported remainder codomain directly. -/
+
+open scoped Classical in
+theorem supportImage_injective (e : ∀ s, V s ≃ W s) :
+    Function.Injective (supportImage fun s => (e s).toEmbedding) :=
+  fun _ _ h => Finset.image_injective (injective_sigmaMap fun s => (e s).toEmbedding) h
+
+open scoped Classical in
+/-- **The remainder index transports along a carrier equivalence.** An equivalence is required:
+the remainder ranges over every rank-`≤ n` coordinate of the ambient carrier, so an embedding into
+a larger carrier would leave coordinates outside its image unmatched. -/
+noncomputable def restIndexCongr (e : ∀ s, V s ≃ W s) (n : ℕ)
+    (A : Finset (Σ s : S.Srt, V s)) :
+    RestIndexOver V n A ≃ RestIndexOver W n (supportImage (fun s => (e s).toEmbedding) A) where
+  toFun c := ⟨RelCoord.congrCarrier e c.1, by
+    obtain ⟨c, hcard, hne⟩ := c
+    rw [RelCoord.support_congrCarrier, supportImage]
+    refine ⟨?_, ?_⟩
+    · rw [Finset.card_image_of_injective _ (injective_sigmaMap fun s => (e s).toEmbedding)]
+      exact hcard
+    · exact fun h => hne (supportImage_injective e h)⟩
+  invFun c := ⟨(RelCoord.congrCarrier e).symm c.1, by
+    obtain ⟨c, hcard, hne⟩ := c
+    refine ⟨?_, ?_⟩
+    · have hsupp : (RelCoord.congrCarrier e ((RelCoord.congrCarrier e).symm c)).support =
+          supportImage (fun s => (e s).toEmbedding)
+            ((RelCoord.congrCarrier e).symm c).support :=
+        RelCoord.support_congrCarrier e _
+      rw [Equiv.apply_symm_apply, supportImage] at hsupp
+      rw [← Finset.card_image_of_injective
+        (((RelCoord.congrCarrier e).symm c).support)
+        (injective_sigmaMap fun s => (e s).toEmbedding), ← hsupp]
+      exact hcard
+    · intro h
+      refine hne ?_
+      have hsupp : (RelCoord.congrCarrier e ((RelCoord.congrCarrier e).symm c)).support =
+          supportImage (fun s => (e s).toEmbedding)
+            ((RelCoord.congrCarrier e).symm c).support :=
+        RelCoord.support_congrCarrier e _
+      rw [Equiv.apply_symm_apply] at hsupp
+      rw [hsupp, h]⟩
+  left_inv c := Subtype.ext (Equiv.symm_apply_apply _ _)
+  right_inv c := Subtype.ext (Equiv.apply_symm_apply _ _)
+
+open scoped Classical in
+/-- The remainder space equivalence induced by a carrier equivalence, as a **measurable**
+equivalence. -/
+noncomputable def restSpaceCongr (e : ∀ s, V s ≃ W s) (n : ℕ)
+    (A : Finset (Σ s : S.Srt, V s)) :
+    RestSpaceOver W n (supportImage (fun s => (e s).toEmbedding) A) ≃ᵐ RestSpaceOver V n A where
+  toEquiv := Equiv.arrowCongr (restIndexCongr e n A).symm (Equiv.refl Bool)
+  measurable_toFun := measurable_pi_lambda _ fun _ => measurable_pi_apply _
+  measurable_invFun := measurable_pi_lambda _ fun _ => measurable_pi_apply _
+
+open scoped Classical in
+@[simp] theorem restSpaceCongr_apply (e : ∀ s, V s ≃ W s) (n : ℕ)
+    (A : Finset (Σ s : S.Srt, V s))
+    (x : RestSpaceOver W n (supportImage (fun s => (e s).toEmbedding) A))
+    (c : RestIndexOver V n A) :
+    restSpaceCongr e n A x c = x (restIndexCongr e n A c) := rfl
+
 end RelSignature
diff --git a/scripts/axiom_audit.lean b/scripts/axiom_audit.lean
index de740ac..23264cb 100644
--- a/scripts/axiom_audit.lean
+++ b/scripts/axiom_audit.lean
@@ -319,6 +319,8 @@ custom axioms. Target list and policy: `scripts/check_census_and_axioms.py`
 #print axioms RelSignature.latentCongrOver
 #print axioms RelSignature.InfiniteRelExchangeableLaw.PooledRankExtension.law_eq
 #print axioms RelSignature.RelCoord.support_congrCarrier
+#print axioms RelSignature.comap_measurableEquiv_comp
+#print axioms RelSignature.restSpaceCongr
 #print axioms RelSignature.latentIndexEmbed_subset_supportImage_iff
 #print axioms RelSignature.InfiniteRelExchangeableLaw.PooledRankExtension.measurePreserving_pooledJointEquiv
 #print axioms MeasureTheory.condExp_comp_measurePreserving
diff --git a/scripts/check_census_and_axioms.py b/scripts/check_census_and_axioms.py
index b3247d2..35221de 100644
--- a/scripts/check_census_and_axioms.py
+++ b/scripts/check_census_and_axioms.py
@@ -284,6 +284,8 @@
     "RelSignature.latentCongrOver",
     "RelSignature.InfiniteRelExchangeableLaw.PooledRankExtension.law_eq",
     "RelSignature.RelCoord.support_congrCarrier",
+    "RelSignature.comap_measurableEquiv_comp",
+    "RelSignature.restSpaceCongr",
     "RelSignature.latentIndexEmbed_subset_supportImage_iff",
     "RelSignature.InfiniteRelExchangeableLaw.PooledRankExtension.measurePreserving_pooledJointEquiv",
     "MeasureTheory.condExp_comp_measurePreserving",

From f052a9c4011105ce23401934f0ffec59da1545b5 Mon Sep 17 00:00:00 2001
From: Cameron Freer <cameronfreer@gmail.com>
Date: Sun, 16 Aug 2026 11:21:56 +0000
Subject: [PATCH 08/13] feat: local and block observation bundles with exact
 naturality (#195 stage 3)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Both follow the pinned pattern: index equivalence, space-level
MeasurableEquiv via contravariant Equiv.arrowCongr, pointwise _apply, and
an exact naturality theorem against the observation.

localLatentIndexCongr needs no Finset.preimage — a support inside
supportImage e A is the image of the part of A landing in it, so the
inverse is a filter of A.

blockIndexCongr keeps its inverse LOCAL to the exact-support subtype:
exists_preimage_of_block draws the range witness for each argument from
the coordinate's support being exactly supportImage e A, so nothing
pretends the embedding is globally surjective.

supportImage_injective generalized from equivalences to embeddings (only
injectivity is used), and supportImage_support records that the image of
a coordinate's support is the transported coordinate's support — the
equation lemma for the noncomputable supportImage will not fire under rw.
Audit 396 -> 400.
---
 Graphon/RelObservationGeometry.lean | 165 +++++++++++++++++++++++++++-
 scripts/axiom_audit.lean            |   4 +
 scripts/check_census_and_axioms.py  |   4 +
 3 files changed, 167 insertions(+), 6 deletions(-)

diff --git a/Graphon/RelObservationGeometry.lean b/Graphon/RelObservationGeometry.lean
index a1b9f9f..6309ae6 100644
--- a/Graphon/RelObservationGeometry.lean
+++ b/Graphon/RelObservationGeometry.lean
@@ -171,6 +171,17 @@ theorem injective_sigmaMap (e : ∀ s, V s ↪ W s) :
     Function.Injective (Sigma.map id fun s => ⇑(e s) : (Σ s : S.Srt, V s) → Σ s : S.Srt, W s) :=
   Function.injective_id.sigma_map fun s => (e s).injective
 
+open scoped Classical in
+theorem supportImage_injective (e : ∀ s, V s ↪ W s) :
+    Function.Injective (supportImage (S := S) e) :=
+  fun _ _ h => Finset.image_injective (injective_sigmaMap e) h
+
+open scoped Classical in
+/-- The image of a coordinate's support is the support of the transported coordinate. -/
+theorem supportImage_support (e : ∀ s, V s ↪ W s) (d : RelCoord S V) :
+    supportImage e d.support = (RelCoord.map (fun s => ⇑(e s)) d).support :=
+  (RelCoord.support_map _ d).symm
+
 open scoped Classical in
 @[simp] theorem mem_supportImage_map {e : ∀ s, V s ↪ W s} {A : Finset (Σ s : S.Srt, V s)}
     {v : Σ s : S.Srt, V s} :
@@ -202,16 +213,158 @@ theorem RelCoord.support_congrCarrier (e : ∀ s, V s ≃ W s) (c : RelCoord S V
   rw [RelCoord.congrCarrier_apply, RelCoord.support_map, supportImage]
   rfl
 
+/-! ### Local latents transport along an embedding
+
+Index equivalence, then the space-level measurable equivalence, then the pointwise lemma, then the
+exact naturality theorem against `localLatentsOver`. The inverse needs no `Finset.preimage`:
+a support inside the image of `A` is the image of the sub-support of `A` that lands in it. -/
+
+open scoped Classical in
+/-- A support inside `supportImage e A` is the image of the part of `A` that lands in it. -/
+theorem image_filter_mem (e : ∀ s, V s ↪ W s) {A : Finset (Σ s : S.Srt, V s)}
+    {B : Finset (Σ s : S.Srt, W s)} (h : B ⊆ supportImage e A) :
+    (A.filter fun v => Sigma.map id (fun s => ⇑(e s)) v ∈ B).image
+        (Sigma.map id fun s => ⇑(e s)) = B := by
+  ext w
+  simp only [Finset.mem_image, Finset.mem_filter]
+  constructor
+  · rintro ⟨v, ⟨-, hv⟩, rfl⟩
+    exact hv
+  · intro hw
+    obtain ⟨v, hv, rfl⟩ := Finset.mem_image.mp (h hw)
+    exact ⟨v, ⟨hv, hw⟩, rfl⟩
+
+open scoped Classical in
+/-- **The local latent index transports along an embedding.** -/
+noncomputable def localLatentIndexCongr (e : ∀ s, V s ↪ W s)
+    (A : Finset (Σ s : S.Srt, V s)) (n : ℕ) :
+    LocalLatentIndexOver V A n ≃ LocalLatentIndexOver W (supportImage e A) n where
+  toFun B := ⟨latentIndexEmbed e n B.1,
+    (latentIndexEmbed_subset_supportImage_iff e B.1).mpr B.2⟩
+  invFun B := ⟨⟨A.filter fun v => Sigma.map id (fun s => ⇑(e s)) v ∈ B.1.1, by
+      have hcard := B.1.2
+      rw [← image_filter_mem e B.2,
+        Finset.card_image_of_injective _ (injective_sigmaMap e)] at hcard
+      exact hcard⟩,
+    Finset.filter_subset _ _⟩
+  left_inv B := by
+    refine Subtype.ext (Subtype.ext ?_)
+    show A.filter (fun v => Sigma.map id (fun s => ⇑(e s)) v ∈
+      (latentIndexEmbed e n B.1).1) = B.1.1
+    ext v
+    simp only [Finset.mem_filter, latentIndexEmbed_coe]
+    rw [(injective_sigmaMap e).mem_finset_image]
+    exact ⟨fun h => h.2, fun h => ⟨B.2 h, h⟩⟩
+  right_inv B := by
+    refine Subtype.ext (Subtype.ext ?_)
+    rw [latentIndexEmbed_coe]
+    exact image_filter_mem e B.2
+
+open scoped Classical in
+/-- The local latent space equivalence induced by an embedding, as a **measurable** equivalence. -/
+noncomputable def localLatentSpaceCongr (e : ∀ s, V s ↪ W s)
+    (A : Finset (Σ s : S.Srt, V s)) (n : ℕ) :
+    LocalLatentSpaceOver W (supportImage e A) n ≃ᵐ LocalLatentSpaceOver V A n where
+  toEquiv := Equiv.arrowCongr (localLatentIndexCongr e A n).symm (Equiv.refl ℝ)
+  measurable_toFun := measurable_pi_lambda _ fun _ => measurable_pi_apply _
+  measurable_invFun := measurable_pi_lambda _ fun _ => measurable_pi_apply _
+
+open scoped Classical in
+@[simp] theorem localLatentSpaceCongr_apply (e : ∀ s, V s ↪ W s)
+    (A : Finset (Σ s : S.Srt, V s)) (n : ℕ)
+    (x : LocalLatentSpaceOver W (supportImage e A) n) (B : LocalLatentIndexOver V A n) :
+    localLatentSpaceCongr e A n x B = x (localLatentIndexCongr e A n B) := rfl
+
+open scoped Classical in
+/-- **Exact naturality of the local latents against an embedding.** Reading the latents visible at
+`A` after restricting along `e` is reading those visible at the image of `A` and transporting. -/
+theorem localLatentsOver_latentRestrictOver (e : ∀ s, V s ↪ W s)
+    (A : Finset (Σ s : S.Srt, V s)) (n : ℕ) :
+    localLatentsOver (S := S) A n ∘ latentRestrictOver e n =
+      localLatentSpaceCongr e A n ∘ localLatentsOver (supportImage e A) n := by
+  funext ω B
+  rfl
+
+/-! ### Blocks transport along an embedding
+
+The inverse is the delicate point and is kept **local to the exact-support subtype**: a coordinate
+whose support is exactly `supportImage e A` has every argument in the image of `e`, which supplies
+the range witness for each argument. Nothing pretends `e` is globally surjective. -/
+
+open scoped Classical in
+/-- Every argument of a coordinate with support exactly `supportImage e A` lies in the range of the
+embedding — the range witness the inverse needs, available only on this subtype. -/
+theorem exists_preimage_of_block (e : ∀ s, V s ↪ W s) {A : Finset (Σ s : S.Srt, V s)}
+    (c : BlockIndexOver W (supportImage e A)) (i : Fin (S.arity c.1.1)) :
+    ∃ v : V (S.argSort c.1.1 i), e _ v = c.1.2 i := by
+  have hmem : c.1.taggedValue i ∈ c.1.support := (RelCoord.mem_support_iff _ _).mpr ⟨i, rfl⟩
+  rw [c.2] at hmem
+  obtain ⟨u, -, heq⟩ := Finset.mem_image.mp hmem
+  obtain ⟨s, v⟩ := u
+  rw [Sigma.mk.injEq] at heq
+  obtain ⟨h1, h2⟩ := heq
+  subst h1
+  exact ⟨v, eq_of_heq h2⟩
+
+open scoped Classical in
+/-- The chosen preimage of an argument. -/
+noncomputable def blockPreimage (e : ∀ s, V s ↪ W s) {A : Finset (Σ s : S.Srt, V s)}
+    (c : BlockIndexOver W (supportImage e A)) (i : Fin (S.arity c.1.1)) :
+    V (S.argSort c.1.1 i) := (exists_preimage_of_block e c i).choose
+
+open scoped Classical in
+@[simp] theorem blockPreimage_spec (e : ∀ s, V s ↪ W s) {A : Finset (Σ s : S.Srt, V s)}
+    (c : BlockIndexOver W (supportImage e A)) (i : Fin (S.arity c.1.1)) :
+    e _ (blockPreimage e c i) = c.1.2 i := (exists_preimage_of_block e c i).choose_spec
+
+open scoped Classical in
+theorem map_blockPreimage (e : ∀ s, V s ↪ W s) {A : Finset (Σ s : S.Srt, V s)}
+    (c : BlockIndexOver W (supportImage e A)) :
+    RelCoord.map (fun s => ⇑(e s)) (⟨c.1.1, blockPreimage e c⟩ : RelCoord S V) = c.1 :=
+  congrArg (fun w => (⟨c.1.1, w⟩ : RelCoord S W)) (funext fun i => blockPreimage_spec e c i)
+
+open scoped Classical in
+/-- **The block index transports along an embedding.** -/
+noncomputable def blockIndexCongr (e : ∀ s, V s ↪ W s) (A : Finset (Σ s : S.Srt, V s)) :
+    BlockIndexOver V A ≃ BlockIndexOver W (supportImage e A) where
+  toFun c := ⟨RelCoord.map (fun s => ⇑(e s)) c.1, by
+    rw [RelCoord.support_map, c.2]; rfl⟩
+  invFun c := ⟨⟨c.1.1, blockPreimage e c⟩, by
+    refine supportImage_injective e ?_
+    rw [supportImage_support, map_blockPreimage e c, c.2]⟩
+  left_inv c := by
+    refine Subtype.ext ?_
+    refine congrArg (fun w => (⟨c.1.1, w⟩ : RelCoord S V)) (funext fun i => ?_)
+    exact (e _).injective (blockPreimage_spec e ⟨RelCoord.map (fun s => ⇑(e s)) c.1, by
+      rw [RelCoord.support_map, c.2]; rfl⟩ i)
+  right_inv c := Subtype.ext (map_blockPreimage e c)
+
+open scoped Classical in
+/-- The block space equivalence induced by an embedding, as a **measurable** equivalence. -/
+noncomputable def blockSpaceCongr (e : ∀ s, V s ↪ W s) (A : Finset (Σ s : S.Srt, V s)) :
+    BlockSpaceOver W (supportImage e A) ≃ᵐ BlockSpaceOver V A where
+  toEquiv := Equiv.arrowCongr (blockIndexCongr e A).symm (Equiv.refl Bool)
+  measurable_toFun := measurable_pi_lambda _ fun _ => measurable_pi_apply _
+  measurable_invFun := measurable_pi_lambda _ fun _ => measurable_pi_apply _
+
+open scoped Classical in
+@[simp] theorem blockSpaceCongr_apply (e : ∀ s, V s ↪ W s) (A : Finset (Σ s : S.Srt, V s))
+    (x : BlockSpaceOver W (supportImage e A)) (c : BlockIndexOver V A) :
+    blockSpaceCongr e A x c = x (blockIndexCongr e A c) := rfl
+
+open scoped Classical in
+/-- **Exact naturality of the block against an embedding.** -/
+theorem blockMapOver_restrict (e : ∀ s, V s ↪ W s) (A : Finset (Σ s : S.Srt, V s)) :
+    blockMapOver (S := S) A ∘ RelStructure.restrict e =
+      blockSpaceCongr e A ∘ blockMapOver (supportImage e A) := by
+  funext X c
+  rfl
+
 /-! ### The remainder transports along a carrier equivalence
 
 Bundled as a measurable equivalence, not merely an index bijection, so that the screening assembly
 can straighten the transported remainder codomain directly. -/
 
-open scoped Classical in
-theorem supportImage_injective (e : ∀ s, V s ≃ W s) :
-    Function.Injective (supportImage fun s => (e s).toEmbedding) :=
-  fun _ _ h => Finset.image_injective (injective_sigmaMap fun s => (e s).toEmbedding) h
-
 open scoped Classical in
 /-- **The remainder index transports along a carrier equivalence.** An equivalence is required:
 the remainder ranges over every rank-`≤ n` coordinate of the ambient carrier, so an embedding into
@@ -225,7 +378,7 @@ noncomputable def restIndexCongr (e : ∀ s, V s ≃ W s) (n : ℕ)
     refine ⟨?_, ?_⟩
     · rw [Finset.card_image_of_injective _ (injective_sigmaMap fun s => (e s).toEmbedding)]
       exact hcard
-    · exact fun h => hne (supportImage_injective e h)⟩
+    · exact fun h => hne (supportImage_injective _ h)⟩
   invFun c := ⟨(RelCoord.congrCarrier e).symm c.1, by
     obtain ⟨c, hcard, hne⟩ := c
     refine ⟨?_, ?_⟩
diff --git a/scripts/axiom_audit.lean b/scripts/axiom_audit.lean
index 23264cb..e2d2662 100644
--- a/scripts/axiom_audit.lean
+++ b/scripts/axiom_audit.lean
@@ -320,6 +320,10 @@ custom axioms. Target list and policy: `scripts/check_census_and_axioms.py`
 #print axioms RelSignature.InfiniteRelExchangeableLaw.PooledRankExtension.law_eq
 #print axioms RelSignature.RelCoord.support_congrCarrier
 #print axioms RelSignature.comap_measurableEquiv_comp
+#print axioms RelSignature.localLatentSpaceCongr
+#print axioms RelSignature.localLatentsOver_latentRestrictOver
+#print axioms RelSignature.blockSpaceCongr
+#print axioms RelSignature.blockMapOver_restrict
 #print axioms RelSignature.restSpaceCongr
 #print axioms RelSignature.latentIndexEmbed_subset_supportImage_iff
 #print axioms RelSignature.InfiniteRelExchangeableLaw.PooledRankExtension.measurePreserving_pooledJointEquiv
diff --git a/scripts/check_census_and_axioms.py b/scripts/check_census_and_axioms.py
index 35221de..41f528c 100644
--- a/scripts/check_census_and_axioms.py
+++ b/scripts/check_census_and_axioms.py
@@ -285,6 +285,10 @@
     "RelSignature.InfiniteRelExchangeableLaw.PooledRankExtension.law_eq",
     "RelSignature.RelCoord.support_congrCarrier",
     "RelSignature.comap_measurableEquiv_comp",
+    "RelSignature.localLatentSpaceCongr",
+    "RelSignature.localLatentsOver_latentRestrictOver",
+    "RelSignature.blockSpaceCongr",
+    "RelSignature.blockMapOver_restrict",
     "RelSignature.restSpaceCongr",
     "RelSignature.latentIndexEmbed_subset_supportImage_iff",
     "RelSignature.InfiniteRelExchangeableLaw.PooledRankExtension.measurePreserving_pooledJointEquiv",

From 17102651993b4795cc778e167d62cac4cb4ec619 Mon Sep 17 00:00:00 2001
From: Cameron Freer <cameronfreer@gmail.com>
Date: Sun, 16 Aug 2026 11:46:29 +0000
Subject: [PATCH 09/13] =?UTF-8?q?feat:=20consequences=201=20and=202=20?=
 =?UTF-8?q?=E2=80=94=20pooled=20latent=20marginal,=20stationary=20extensio?=
 =?UTF-8?q?n=20(#195=20stage=203)?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

latentSourceOver_map_latentCongrOver is the generic exact source
transport along a carrier equivalence — the same infinite-product
coordinate-equivalence argument as source invariance.

PooledRankExtension.map_snd: the pooled latent marginal is the pooled
i.i.d. source, a transport of C.map_snd through the canonical identity.

PooledRankExtension.toStationaryExtension: the structure marginal is a
StationaryExtension M, both fields being the corresponding pooled field
composed with Prod.fst.

Support lemmas: pooledExtension_law_coe and
rankLatentSource_eq_latentSourceOver bridge the alias boundary for rw,
which cannot see through the coercion or the def.
---
 Graphon/RelLatentGeometry.lean     |  9 ++++++
 Graphon/RelPooledAcceptance.lean   | 49 ++++++++++++++++++++++++++++++
 Graphon/RelPooledExtension.lean    |  6 ++++
 Graphon/RelRankLatents.lean        |  3 ++
 scripts/axiom_audit.lean           |  3 ++
 scripts/check_census_and_axioms.py |  3 ++
 6 files changed, 73 insertions(+)

diff --git a/Graphon/RelLatentGeometry.lean b/Graphon/RelLatentGeometry.lean
index f62b110..2259fd8 100644
--- a/Graphon/RelLatentGeometry.lean
+++ b/Graphon/RelLatentGeometry.lean
@@ -299,6 +299,15 @@ noncomputable def latentCongrOver (e : ∀ s, V s ≃ W s) (n : ℕ) :
     (latentCongrOver e n).symm ω =
       latentRestrictOver (fun s => (e s).symm.toEmbedding) n ω := rfl
 
+/-- **Exact source transport along a carrier equivalence.** The same infinite-product
+coordinate-equivalence argument as source invariance, with the index bijection now coming from an
+equivalence of carriers rather than a permutation of one. -/
+theorem latentSourceOver_map_latentCongrOver [Countable S.Srt] [∀ s, Countable (V s)]
+    [∀ s, Countable (W s)] (e : ∀ s, V s ≃ W s) (n : ℕ) :
+    (latentSourceOver S W n).map (latentCongrOver e n) = latentSourceOver S V n := by
+  rw [latentSourceOver, latentSourceOver, iidUniformSource, iidUniformSource]
+  exact Measure.infinitePi_map_comp_equiv _ (latentIndexCongr e n)
+
 /-- **The conjugation square for a carrier equivalence** — the latent-side mirror of
 `RelStructure.congrCarrier_relabel`. Transporting along `e` intertwines a permutation of the
 source carrier with its conjugate on the target. Proved carrier-generically, so instantiating at
diff --git a/Graphon/RelPooledAcceptance.lean b/Graphon/RelPooledAcceptance.lean
index 6503881..d000432 100644
--- a/Graphon/RelPooledAcceptance.lean
+++ b/Graphon/RelPooledAcceptance.lean
@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Cameron Freer
 -/
 import Graphon.RelPooledExtension
+import Graphon.RelStationaryExtension
 
 /-!
 # The joint restriction theorem for a pooled rank extension (R4 converse, #107)
@@ -253,6 +254,54 @@ theorem RankRepresentation.pooledExtension_map_restrict_embedding (C : M.RankRep
       (Prod.map (RelStructure.restrict e) (latentRestrictOver e n)) = C.P :=
   (C.pooledExtension).map_restrict_embedding e
 
+/-! ### Consequence 1: the pooled latent marginal -/
+
+/-- **The pooled latent marginal is the pooled i.i.d. source.** A transport of `C.map_snd` through
+the canonical identity, with the source transport doing the work on the latent factor. -/
+theorem PooledRankExtension.map_snd {C : M.RankRepresentation n} (Q : PooledRankExtension C) :
+    (Q.law : Measure (RelStructure S (PoolVertex S) × PooledRankLatentSpace S n)).map Prod.snd =
+      pooledRankLatentSource S n := by
+  haveI := C.isProbabilityMeasure_P
+  rw [Q.law_eq, RankRepresentation.pooledExtension_law_coe,
+    Measure.map_map measurable_snd RankRepresentation.measurable_pooledTransport,
+    show Prod.snd ∘ RankRepresentation.pooledTransport (S := S) (n := n) =
+      latentCongrOver (fun s => poolVertexEquiv S s) n ∘ Prod.snd from rfl,
+    ← Measure.map_map (latentCongrOver (fun s => poolVertexEquiv S s) n).measurable
+      measurable_snd,
+    C.map_snd, rankLatentSource_eq_latentSourceOver, pooledRankLatentSource,
+    latentSourceOver_map_latentCongrOver (fun s => poolVertexEquiv S s) n]
+
+/-! ### Consequence 2: the structure marginal is a stationary extension -/
+
+/-- **The structure marginal of a pooled rank extension is a stationary extension of the law.**
+Both fields are the corresponding pooled field composed with `Prod.fst`. -/
+noncomputable def PooledRankExtension.toStationaryExtension {C : M.RankRepresentation n}
+    (Q : PooledRankExtension C) : StationaryExtension M where
+  law := ⟨(Q.law : Measure (RelStructure S (PoolVertex S) × PooledRankLatentSpace S n)).map
+      Prod.fst, by
+    haveI : IsProbabilityMeasure
+        (Q.law : Measure (RelStructure S (PoolVertex S) × PooledRankLatentSpace S n)) := Q.law.2
+    exact Measure.isProbabilityMeasure_map measurable_fst.aemeasurable⟩
+  map_restrictOriginal := by
+    haveI := C.isProbabilityMeasure_P
+    rw [ProbabilityMeasure.coe_mk,
+      Measure.map_map measurable_restrictOriginal measurable_fst,
+      show restrictOriginal S ∘ (Prod.fst :
+          RelStructure S (PoolVertex S) × PooledRankLatentSpace S n → _) =
+        Prod.fst ∘ Prod.map (restrictOriginal S) (restrictOriginalLatents S n) from rfl,
+      ← Measure.map_map measurable_fst
+        (measurable_restrictOriginal.prodMap (measurable_restrictOriginalLatents n)),
+      Q.map_restrictOriginal, C.map_fst]
+  invariant := by
+    intro ρ
+    rw [ProbabilityMeasure.coe_mk, Measure.map_map (measurable_relabel ρ) measurable_fst,
+      show RelStructure.relabel ρ ∘ (Prod.fst :
+          RelStructure S (PoolVertex S) × PooledRankLatentSpace S n → _) =
+        Prod.fst ∘ Prod.map (RelStructure.relabel ρ) (pooledRankLatentRelabel ρ n) from rfl,
+      ← Measure.map_map measurable_fst
+        ((measurable_relabel ρ).prodMap (pooledRankLatentRelabel ρ n).measurable),
+      Q.invariant ρ]
+
 end InfiniteRelExchangeableLaw
 
 end RelSignature
diff --git a/Graphon/RelPooledExtension.lean b/Graphon/RelPooledExtension.lean
index f35e045..a0e9fed 100644
--- a/Graphon/RelPooledExtension.lean
+++ b/Graphon/RelPooledExtension.lean
@@ -156,6 +156,12 @@ noncomputable def pooledExtension : PooledRankExtension C where
         (pooledRankLatentRelabel ρ n).measurable) measurable_pooledTransport,
       hjoint, ← Measure.map_map measurable_pooledTransport hκmeas, hinvκ]
 
+/-- The cheap extension's law, unfolded. -/
+@[simp] theorem pooledExtension_law_coe :
+    ((C.pooledExtension).law :
+        Measure (RelStructure S (PoolVertex S) × PooledRankLatentSpace S n)) =
+      C.P.map pooledTransport := rfl
+
 end RankRepresentation
 
 end InfiniteRelExchangeableLaw
diff --git a/Graphon/RelRankLatents.lean b/Graphon/RelRankLatents.lean
index 5b51cf9..9b3e8f7 100644
--- a/Graphon/RelRankLatents.lean
+++ b/Graphon/RelRankLatents.lean
@@ -342,6 +342,9 @@ theorem rankLatentSpaceSuccEquiv_rankLatentRelabel (σ : FinSuppPerm S) (n : ℕ
       MeasurableEquiv.prodCongr (rankLatentRelabel σ n) (rankSupportLatentRelabel σ n) ∘
         rankLatentSpaceSuccEquiv n := rfl
 
+theorem rankLatentSource_eq_latentSourceOver (S : RelSignature) (n : ℕ) :
+    rankLatentSource S n = latentSourceOver S (Vinfinite S) n := rfl
+
 /-! ### Bridge to the carrier-parametric core
 
 The rank-indexed operations were built before the carrier-parametric core and choose their own
diff --git a/scripts/axiom_audit.lean b/scripts/axiom_audit.lean
index e2d2662..bf0a057 100644
--- a/scripts/axiom_audit.lean
+++ b/scripts/axiom_audit.lean
@@ -327,6 +327,9 @@ custom axioms. Target list and policy: `scripts/check_census_and_axioms.py`
 #print axioms RelSignature.restSpaceCongr
 #print axioms RelSignature.latentIndexEmbed_subset_supportImage_iff
 #print axioms RelSignature.InfiniteRelExchangeableLaw.PooledRankExtension.measurePreserving_pooledJointEquiv
+#print axioms RelSignature.latentSourceOver_map_latentCongrOver
+#print axioms RelSignature.InfiniteRelExchangeableLaw.PooledRankExtension.map_snd
+#print axioms RelSignature.InfiniteRelExchangeableLaw.PooledRankExtension.toStationaryExtension
 #print axioms MeasureTheory.condExp_comp_measurePreserving
 #print axioms ProbabilityTheory.condExp_set_comp_measurePreserving
 #print axioms ProbabilityTheory.condIndepFun_comp_measurePreserving
diff --git a/scripts/check_census_and_axioms.py b/scripts/check_census_and_axioms.py
index 41f528c..8e72f49 100644
--- a/scripts/check_census_and_axioms.py
+++ b/scripts/check_census_and_axioms.py
@@ -292,6 +292,9 @@
     "RelSignature.restSpaceCongr",
     "RelSignature.latentIndexEmbed_subset_supportImage_iff",
     "RelSignature.InfiniteRelExchangeableLaw.PooledRankExtension.measurePreserving_pooledJointEquiv",
+    "RelSignature.latentSourceOver_map_latentCongrOver",
+    "RelSignature.InfiniteRelExchangeableLaw.PooledRankExtension.map_snd",
+    "RelSignature.InfiniteRelExchangeableLaw.PooledRankExtension.toStationaryExtension",
     "MeasureTheory.condExp_comp_measurePreserving",
     "ProbabilityTheory.condExp_set_comp_measurePreserving",
     "ProbabilityTheory.condIndepFun_comp_measurePreserving",

From 544db718106dfc23fda0f702f3b083b9bb60f864 Mon Sep 17 00:00:00 2001
From: Cameron Freer <cameronfreer@gmail.com>
Date: Sun, 16 Aug 2026 12:05:42 +0000
Subject: [PATCH 10/13] refactor: extract CondIndepFun.congr_cond as shared
 glue (#195 stage 3)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

The conditioning-algebra congruence lemma was duplicated verbatim as a
private theorem in RelRankOneCoupling and RelRankOneScreening. Extracted
once into ForMathlib/CondIndepSup as
ProbabilityTheory.CondIndepFun.congr_cond, with both copies replaced by
dot-notation calls; it handles the dependent comap_le proof by proof
irrelevance after substituting the sigma-algebra equality.

It is the lemma screening needs as its third step, alongside
comap_measurableEquiv_comp — established shared glue with three
consumers rather than speculative cleanup.
---
 Graphon/ForMathlib/CondIndepSup.lean | 12 ++++++++++++
 Graphon/RelRankOneCoupling.lean      | 13 ++-----------
 Graphon/RelRankOneScreening.lean     | 12 +-----------
 scripts/axiom_audit.lean             |  1 +
 scripts/check_census_and_axioms.py   |  1 +
 5 files changed, 17 insertions(+), 22 deletions(-)

diff --git a/Graphon/ForMathlib/CondIndepSup.lean b/Graphon/ForMathlib/CondIndepSup.lean
index 53aabba..9f28962 100644
--- a/Graphon/ForMathlib/CondIndepSup.lean
+++ b/Graphon/ForMathlib/CondIndepSup.lean
@@ -106,4 +106,16 @@ theorem CondIndepFun.congr {β β' : Type*} {mβ : MeasurableSpace β} {mβ' : M
     _ =ᵐ[μ] fun ω => (μ⟦f' ⁻¹' s | m'⟧) ω * (μ⟦g' ⁻¹' t | m'⟧) ω :=
         ((hsets h1).symm.mul (hsets h2).symm)
 
+/-- **The conditioning σ-algebra may be replaced by an equal one.** The dependent `≤` proof is
+handled by proof irrelevance once the σ-algebra equality is substituted. Shared glue: the rank-one
+coupling and screening arguments both need it, and so does any transport of a conditional
+independence statement whose conditioning map has been reindexed. -/
+theorem CondIndepFun.congr_cond {Ω β γ : Type*} [mΩ : MeasurableSpace Ω]
+    [StandardBorelSpace Ω] {μ : Measure Ω} [IsFiniteMeasure μ]
+    [MeasurableSpace β] [MeasurableSpace γ] {f : Ω → β} {g : Ω → γ}
+    {m₁ m₂ : MeasurableSpace Ω} {h1 : m₁ ≤ mΩ} (h : CondIndepFun m₁ h1 f g μ)
+    (h12 : m₁ = m₂) (h2 : m₂ ≤ mΩ) : CondIndepFun m₂ h2 f g μ := by
+  subst h12
+  exact h
+
 end ProbabilityTheory
diff --git a/Graphon/RelRankOneCoupling.lean b/Graphon/RelRankOneCoupling.lean
index d4d8d2f..15121ed 100644
--- a/Graphon/RelRankOneCoupling.lean
+++ b/Graphon/RelRankOneCoupling.lean
@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Cameron Freer
 -/
 import Graphon.RelRankOneTransfer
+import Graphon.ForMathlib.CondIndepSup
 import Graphon.RelRankLatents
 import Graphon.ForMathlib.CondExpComap
 
@@ -73,16 +74,6 @@ instance [Countable S.Srt] [Countable S.Rel] (f : ℝ → B.LowerFactorSpace 1)
   rw [rankOneLatentCoupling]
   exact Measure.isFiniteMeasure_map _ _
 
-/-- Conditional independence is insensitive to replacing the conditioning σ-algebra by an equal
-one; the inclusion proofs move by proof irrelevance. -/
-private theorem condIndepFun_congr_cond {Ω β γ : Type*} [mΩ : MeasurableSpace Ω]
-    [StandardBorelSpace Ω] {μ : Measure Ω} [IsFiniteMeasure μ]
-    [MeasurableSpace β] [MeasurableSpace γ] {f : Ω → β} {g : Ω → γ}
-    {m₁ m₂ : MeasurableSpace Ω} (h12 : m₁ = m₂) {h1 : m₁ ≤ mΩ} (h2 : m₂ ≤ mΩ)
-    (h : CondIndepFun m₁ h1 f g μ) : CondIndepFun m₂ h2 f g μ := by
-  subst h12
-  exact h
-
 open scoped Classical in
 /-- **The transported clauses.** There are a coding `f` and a measurable latent read `g` for
 which the rank-one latent coupling is a probability measure with the law and the latent
@@ -172,7 +163,7 @@ theorem exists_rankOneLatentCoupling [Countable S.Srt] [Countable S.Rel] :
     rw [show id ∘ (h ∘ Prod.fst) ∘ ⇑(rankOneLatentEquiv S).symm = h ∘ Prod.fst from rfl,
       show ⇑e.symm ∘ Prod.snd ∘ ⇑(rankOneLatentEquiv S).symm = Prod.snd from
         funext fun p => e.symm_apply_apply _] at hstraight
-    exact condIndepFun_congr_cond (by rw [MeasurableSpace.comap_comp]; rfl) _ hstraight
+    exact hstraight.congr_cond (by rw [MeasurableSpace.comap_comp]; rfl) _
 
 end CoherentBasis
 
diff --git a/Graphon/RelRankOneScreening.lean b/Graphon/RelRankOneScreening.lean
index ba1b0dd..1b6ef1f 100644
--- a/Graphon/RelRankOneScreening.lean
+++ b/Graphon/RelRankOneScreening.lean
@@ -88,16 +88,6 @@ theorem comap_localLatents_one_snd {S : RelSignature.{u}} [Countable S.Srt]
       _ ≤ MeasurableSpace.comap (localLatents A 1 ∘ Prod.snd) inferInstance :=
             MeasurableSpace.comap_mono (measurable_iff_comap_le.mp hρmeas)
 
-/-- Conditional independence is insensitive to replacing the conditioning σ-algebra by an equal
-one; the inclusion proofs move by proof irrelevance. -/
-private theorem condIndepFun_congr_cond {Ω β γ : Type*} [mΩ : MeasurableSpace Ω]
-    [StandardBorelSpace Ω] {μ : Measure Ω} [IsFiniteMeasure μ]
-    [MeasurableSpace β] [MeasurableSpace γ] {f : Ω → β} {g : Ω → γ}
-    {m₁ m₂ : MeasurableSpace Ω} (h12 : m₁ = m₂) {h1 : m₁ ≤ mΩ} (h2 : m₂ ≤ mΩ)
-    (h : CondIndepFun m₁ h1 f g μ) : CondIndepFun m₂ h2 f g μ := by
-  subst h12
-  exact h
-
 open scoped Classical in
 /-- **Per-support screening at rank one.** Given the ladder's conclusion — mutual conditional
 independence of the singleton blocks given the full latent σ-algebra — and the nullary
@@ -197,7 +187,7 @@ theorem condIndepFun_blockMap_restObservation_one {S : RelSignature.{u}}
   have h5 := h4.congr (measurable_singletonBlockRead v₀) hR'amb
     (measurable_singletonBlockRead v₀) (measurable_restObservation 1 _)
     Filter.EventuallyEq.rfl hae.symm
-  exact condIndepFun_congr_cond (comap_localLatents_one_snd _).symm _ h5
+  exact h5.congr_cond (comap_localLatents_one_snd _).symm _
 
 namespace CoherentBasis
 
diff --git a/scripts/axiom_audit.lean b/scripts/axiom_audit.lean
index bf0a057..4ee439b 100644
--- a/scripts/axiom_audit.lean
+++ b/scripts/axiom_audit.lean
@@ -319,6 +319,7 @@ custom axioms. Target list and policy: `scripts/check_census_and_axioms.py`
 #print axioms RelSignature.latentCongrOver
 #print axioms RelSignature.InfiniteRelExchangeableLaw.PooledRankExtension.law_eq
 #print axioms RelSignature.RelCoord.support_congrCarrier
+#print axioms ProbabilityTheory.CondIndepFun.congr_cond
 #print axioms RelSignature.comap_measurableEquiv_comp
 #print axioms RelSignature.localLatentSpaceCongr
 #print axioms RelSignature.localLatentsOver_latentRestrictOver
diff --git a/scripts/check_census_and_axioms.py b/scripts/check_census_and_axioms.py
index 8e72f49..f8ca8ee 100644
--- a/scripts/check_census_and_axioms.py
+++ b/scripts/check_census_and_axioms.py
@@ -284,6 +284,7 @@
     "RelSignature.latentCongrOver",
     "RelSignature.InfiniteRelExchangeableLaw.PooledRankExtension.law_eq",
     "RelSignature.RelCoord.support_congrCarrier",
+    "ProbabilityTheory.CondIndepFun.congr_cond",
     "RelSignature.comap_measurableEquiv_comp",
     "RelSignature.localLatentSpaceCongr",
     "RelSignature.localLatentsOver_latentRestrictOver",

From 36883f0f8d34403db22a959f39d4b0cadb3f4db7 Mon Sep 17 00:00:00 2001
From: Cameron Freer <cameronfreer@gmail.com>
Date: Sun, 16 Aug 2026 13:35:26 +0000
Subject: [PATCH 11/13] =?UTF-8?q?feat:=20consequence=203=20=E2=80=94=20loc?=
 =?UTF-8?q?al=20recovery=20on=20pooled=20supports=20(#195=20stage=203)?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

PooledRankExtension.lower_recovers: recovery holds on every pooled
support below rank n, mixed supports included. C.lower_recovers is pulled
back through measurePreserving_pooledJointEquiv's quasiMeasurePreserving
ae_eq_comp, and the decoder is conjugated through the local and block
measurable equivalences — the only a.e. step is the transported identity
itself, with no manual null-set rewriting.

The pooled support is presented once as the image of an original one
(supportImage_symm_supportImage, card_supportImage) via an obtain with
rfl, which avoids dependent ▸ transports entirely.
---
 Graphon/RelObservationGeometry.lean | 17 ++++++++++
 Graphon/RelPooledAcceptance.lean    | 48 +++++++++++++++++++++++++++++
 scripts/axiom_audit.lean            |  1 +
 scripts/check_census_and_axioms.py  |  1 +
 4 files changed, 67 insertions(+)

diff --git a/Graphon/RelObservationGeometry.lean b/Graphon/RelObservationGeometry.lean
index 6309ae6..44768ba 100644
--- a/Graphon/RelObservationGeometry.lean
+++ b/Graphon/RelObservationGeometry.lean
@@ -285,6 +285,23 @@ theorem localLatentsOver_latentRestrictOver (e : ∀ s, V s ↪ W s)
   funext ω B
   rfl
 
+open scoped Classical in
+/-- Transporting a support along a carrier equivalence and back is the identity. -/
+theorem supportImage_symm_supportImage (e : ∀ s, V s ≃ W s) (A : Finset (Σ s : S.Srt, V s)) :
+    supportImage (fun s => (e s).symm.toEmbedding) (supportImage (fun s => (e s).toEmbedding) A)
+      = A := by
+  rw [supportImage, supportImage, Finset.image_image]
+  refine (Finset.image_congr fun v _ => ?_).trans A.image_id
+  obtain ⟨s, x⟩ := v
+  show (⟨s, (e s).symm ((e s) x)⟩ : Σ s : S.Srt, V s) = ⟨s, x⟩
+  rw [(e s).symm_apply_apply]
+
+open scoped Classical in
+/-- The transported support has the same cardinality. -/
+theorem card_supportImage (e : ∀ s, V s ↪ W s) (A : Finset (Σ s : S.Srt, V s)) :
+    (supportImage e A).card = A.card :=
+  Finset.card_image_of_injective _ (injective_sigmaMap e)
+
 /-! ### Blocks transport along an embedding
 
 The inverse is the delicate point and is kept **local to the exact-support subtype**: a coordinate
diff --git a/Graphon/RelPooledAcceptance.lean b/Graphon/RelPooledAcceptance.lean
index d000432..54f9d3a 100644
--- a/Graphon/RelPooledAcceptance.lean
+++ b/Graphon/RelPooledAcceptance.lean
@@ -208,11 +208,13 @@ noncomputable def pooledJointEquiv :
   (RelStructure.congrCarrier fun s => poolVertexEquiv S s).prodCongr
     (latentCongrOver (fun s => (poolVertexEquiv S s).symm) n)
 
+omit [Countable S.Srt] [Countable S.Rel] in
 theorem pooledJointEquiv_coe :
     ((pooledJointEquiv S n : _ ≃ᵐ _) : _ → _) =
       Prod.map (RelStructure.restrict fun s => (poolVertexEquiv S s).symm.toEmbedding)
         (latentRestrictOver (fun s => (poolVertexEquiv S s).symm.toEmbedding) n) := rfl
 
+omit [Countable S.Srt] [Countable S.Rel] in
 theorem pooledJointEquiv_symm_coe :
     (((pooledJointEquiv S n : _ ≃ᵐ _).symm : _ ≃ᵐ _) : _ → _) =
       RankRepresentation.pooledTransport (S := S) (n := n) := rfl
@@ -302,6 +304,52 @@ noncomputable def PooledRankExtension.toStationaryExtension {C : M.RankRepresent
         ((measurable_relabel ρ).prodMap (pooledRankLatentRelabel ρ n).measurable),
       Q.invariant ρ]
 
+/-! ### Consequence 3: local recovery on pooled supports -/
+
+open scoped Classical in
+/-- **Local recovery holds on every pooled support below rank `n`** — mixed supports included.
+`C.lower_recovers` is pulled back along the canonical identification, and the decoder is conjugated
+through the local and block measurable equivalences. The only almost-everywhere step is the
+transported identity itself. -/
+theorem PooledRankExtension.lower_recovers {C : M.RankRepresentation n}
+    (Q : PooledRankExtension C) (A : Finset (Σ s : S.Srt, PoolVertex S s)) (hA : A.card < n) :
+    ∃ g : LocalLatentSpaceOver (PoolVertex S) A n → BlockSpaceOver (PoolVertex S) A,
+      Measurable g ∧
+      blockMapOver A ∘ Prod.fst =ᵐ[(Q.law :
+          Measure (RelStructure S (PoolVertex S) × PooledRankLatentSpace S n))]
+        g ∘ localLatentsOver A n ∘ Prod.snd := by
+  haveI := C.isProbabilityMeasure_P
+  classical
+  set e : ∀ s, Vinfinite S s ↪ PoolVertex S s :=
+    fun s => (poolVertexEquiv S s).symm.toEmbedding with he
+  -- present the pooled support as the image of an original one, once and for all
+  obtain ⟨A₀, hA₀card, rfl⟩ :
+      ∃ A₀ : Finset (Σ s : S.Srt, Vinfinite S s), A₀.card < n ∧ supportImage e A₀ = A := by
+    refine ⟨supportImage (fun s => (poolVertexEquiv S s).toEmbedding) A, ?_, ?_⟩
+    · rw [card_supportImage]; exact hA
+    · rw [he]; exact supportImage_symm_supportImage (fun s => poolVertexEquiv S s) A
+  obtain ⟨g₀, hg₀meas, hg₀⟩ := C.lower_recovers A₀ hA₀card
+  have hpull := (Q.measurePreserving_pooledJointEquiv).quasiMeasurePreserving.ae_eq_comp hg₀
+  refine ⟨(blockSpaceCongr e A₀).symm ∘ g₀ ∘ localLatentSpaceCongr e A₀ n, ?_, ?_⟩
+  · exact ((blockSpaceCongr e A₀).symm.measurable.comp hg₀meas).comp
+      (localLatentSpaceCongr e A₀ n).measurable
+  · filter_upwards [hpull] with p hp
+    have hb : blockMap A₀ (RelStructure.restrict e p.1)
+        = blockSpaceCongr e A₀ (blockMapOver (supportImage e A₀) p.1) :=
+      congrFun (blockMapOver_restrict e A₀) p.1
+    have hl : localLatents A₀ n (latentRestrictOver e n p.2)
+        = localLatentSpaceCongr e A₀ n (localLatentsOver (supportImage e A₀) n p.2) :=
+      congrFun (localLatentsOver_latentRestrictOver e A₀ n) p.2
+    have hp' : blockSpaceCongr e A₀ (blockMapOver (supportImage e A₀) p.1)
+        = g₀ (localLatentSpaceCongr e A₀ n (localLatentsOver (supportImage e A₀) n p.2)) := by
+      rw [← hb, ← hl]; exact hp
+    show blockMapOver (supportImage e A₀) p.1 = _
+    calc blockMapOver (supportImage e A₀) p.1
+        = (blockSpaceCongr e A₀).symm
+            (blockSpaceCongr e A₀ (blockMapOver (supportImage e A₀) p.1)) :=
+          ((blockSpaceCongr e A₀).symm_apply_apply _).symm
+      _ = _ := by rw [hp']; rfl
+
 end InfiniteRelExchangeableLaw
 
 end RelSignature
diff --git a/scripts/axiom_audit.lean b/scripts/axiom_audit.lean
index 4ee439b..c0a1d78 100644
--- a/scripts/axiom_audit.lean
+++ b/scripts/axiom_audit.lean
@@ -331,6 +331,7 @@ custom axioms. Target list and policy: `scripts/check_census_and_axioms.py`
 #print axioms RelSignature.latentSourceOver_map_latentCongrOver
 #print axioms RelSignature.InfiniteRelExchangeableLaw.PooledRankExtension.map_snd
 #print axioms RelSignature.InfiniteRelExchangeableLaw.PooledRankExtension.toStationaryExtension
+#print axioms RelSignature.InfiniteRelExchangeableLaw.PooledRankExtension.lower_recovers
 #print axioms MeasureTheory.condExp_comp_measurePreserving
 #print axioms ProbabilityTheory.condExp_set_comp_measurePreserving
 #print axioms ProbabilityTheory.condIndepFun_comp_measurePreserving
diff --git a/scripts/check_census_and_axioms.py b/scripts/check_census_and_axioms.py
index f8ca8ee..a9e6c7b 100644
--- a/scripts/check_census_and_axioms.py
+++ b/scripts/check_census_and_axioms.py
@@ -296,6 +296,7 @@
     "RelSignature.latentSourceOver_map_latentCongrOver",
     "RelSignature.InfiniteRelExchangeableLaw.PooledRankExtension.map_snd",
     "RelSignature.InfiniteRelExchangeableLaw.PooledRankExtension.toStationaryExtension",
+    "RelSignature.InfiniteRelExchangeableLaw.PooledRankExtension.lower_recovers",
     "MeasureTheory.condExp_comp_measurePreserving",
     "ProbabilityTheory.condExp_set_comp_measurePreserving",
     "ProbabilityTheory.condIndepFun_comp_measurePreserving",

From f8b2a108df625ba31c40ed78608972a51736f98e Mon Sep 17 00:00:00 2001
From: Cameron Freer <cameronfreer@gmail.com>
Date: Sun, 16 Aug 2026 14:32:38 +0000
Subject: [PATCH 12/13] =?UTF-8?q?feat:=20consequence=204=20=E2=80=94=20scr?=
 =?UTF-8?q?eening=20on=20pooled=20supports;=20stage=203=20complete=20(#195?=
 =?UTF-8?q?)?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

restObservationOver_congrCarrier is the missing naturality: observing
after transporting the joint object back from W to V equals observing on
W and reindexing both remainder outputs. Pointwise rfl after funext, as
expected, and equivalence-only throughout.

PooledRankExtension.screening is then pure assembly in the three named
steps: condIndepFun_comp_measurePreserving on
measurePreserving_pooledJointEquiv, CondIndepFun.comp with the inverse
output equivalences (post-composition never touches the dependent proof,
which is why the coercion cannot be rewritten inside the conditioning
algebra), and CondIndepFun.congr_cond with comap_measurableEquiv_comp.
No conditional-expectation or dependent-proof manipulation appears.

All four route-neutral consequences of the gate are now proved.
Audit 405 -> 407.
---
 Graphon.lean                        |  2 +-
 Graphon/RelObservationGeometry.lean | 14 ++++++
 Graphon/RelPooledAcceptance.lean    | 71 ++++++++++++++++++++++++++++-
 scripts/axiom_audit.lean            |  2 +
 scripts/check_census_and_axioms.py  |  2 +
 5 files changed, 89 insertions(+), 2 deletions(-)

diff --git a/Graphon.lean b/Graphon.lean
index a97ce3d..6ba995a 100644
--- a/Graphon.lean
+++ b/Graphon.lean
@@ -266,7 +266,7 @@ in Lean 4 using Mathlib.
 * `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. `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.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.RelRankInjectionInvariance` — R4 converse (#107), the isolated proof risk of the pooled-latent extension gate: **joint invariance under arbitrary sortwise self-injections**. `RankRepresentation.invariant` is stated for *finitely supported permutations*, but a pooled object built cheaply through `poolVertexEquiv` needs the joint law invariant under every self-injection; `RankRepresentation.map_prodMap_restrict_self` supplies exactly that, so full mixed pooled invariance later costs no additional mathematics. The route is finite-cylinder extensionality on the **joint** space, which had no machinery before — rank one's joint invariance goes through only because the rank-one latent action is trivial. `rankLatentIndexInj`/`rankLatentReindex` extend the latent action from permutations to injections (only injectivity is used — a support keeps its cardinality); `exists_finSuppPerm_agree_on_finset` matches an injection to a finitely supported permutation on any finite tagged-vertex support; `ext_of_prod_cylinders` is the joint extensionality, rectangles of coordinate cylinders on both factors. **No finiteness/`Fintype` hypothesis beyond `RankRepresentation`'s ambient countability.** Equality is tested on *coordinate* cylinders — finitely many `RelCoord`s and finitely many latent indices — whose combined vertex support is one finite `Finset (Σ s, Vinfinite S s)` and so touches only finitely many sorts; the injection is matched there by extending it on each active sort, taking the identity elsewhere, and maximizing finitely many support bounds. The coarser `restrictFin` cylinder family would instead force a uniform all-sort bound that no self-injection need admit
 * `Graphon.RelRankCoding` — R4 converse piece 3 (#107): factor-law coding of the lower-rank factor. **Not** the inductive hypothesis of a working recursion: `RankCoding n → ShellProperty n` is **false**, refuted by Austin's random complete bipartite graph `X_uv = z_u ⊕ z_v` (arXiv:0801.1698 §3.6), where `lowerRankAlgebra 2` is trivial modulo the law but every triangle satisfies `X₁₂ ⊕ X₁₃ ⊕ X₂₃ = 0`, so the exact layers are pairwise but not mutually independent — while a `RankCoding 2` exists because the rank-2 factor law is a point mass. The example separates the true two-set theorem from mutuality, and shows the gap is not closable by coupling: a relatively independent joining over `lowerFactorMap` attaches latents that are conditionally independent of the structure given a trivial factor, whereas a representation needs the hidden colours, correlated with the array yet not recoverable from it. `RankCoding n` represents the rank-`n` factor by latents — a measurable coding map carrying the latent source to the factor law and intertwining the two relabeling actions **almost everywhere**. The a.e. form is forced: `lowerFactorSpaceEquiv σ n` fixes the *image* of `lowerFactorMap n`, not the whole Bool-cube, since it permutes distinct basis indices that name the same event, so the strict version is false already at rank one. `ShellProperty n` is the conclusion the recursion consumes, bundling mutual conditional independence of the exact layers over the rank-`n` supports **with** per-support locality; neither half implies the other, since mutual independence given the whole lower-rank factor permits dependence on all of it rather than only through `boundaryMap A`. `RankCoding.rankOne` is the base case, built from the #140 randomization adapter transported along `rankLatentOneEquiv`; its equivariance clause is genuinely exercised rather than vacuous, because at rank one the latent relabeling is the identity while the factor equivalence is not
 * `Graphon.RelFixingAlgebra` — R4 converse piece 2a (#107): the **law-independent** factor-algebra layer — `SortwiseFixing` (the `A`-fixing stabilizer of finitely supported sortwise permutations, closed under `1`/`*`/`⁻¹`/conjugation), the raw `RelStructure.fixingAlgebra` (events invariant under the `A`-fixing group; deliberately *not* "generated by relations inside `A`", which loses hidden vertex information), monotonicity, `fixingAlgebra_empty = invariantAlgebra` (near-definitional), and the **transport equality** `fixingAlgebra_comap_relabel : comap (relabel σ) (fixingAlgebra A) = fixingAlgebra (image σ A)` via stabilizer conjugation — no completions, no law; the conditional-independence theorem is its own later PR
diff --git a/Graphon/RelObservationGeometry.lean b/Graphon/RelObservationGeometry.lean
index 44768ba..3487db8 100644
--- a/Graphon/RelObservationGeometry.lean
+++ b/Graphon/RelObservationGeometry.lean
@@ -436,4 +436,18 @@ open scoped Classical in
     (c : RestIndexOver V n A) :
     restSpaceCongr e n A x c = x (restIndexCongr e n A c) := rfl
 
+open scoped Classical in
+/-- **Exact naturality of the remainder against a carrier equivalence.** Observing after
+transporting the whole joint object from `W` back to `V` is observing on `W` and reindexing both
+remainder outputs. An equivalence throughout — the remainder is global. -/
+theorem restObservationOver_congrCarrier (e : ∀ s, V s ≃ W s) (n : ℕ)
+    (A : Finset (Σ s : S.Srt, V s)) :
+    restObservationOver (S := S) n A ∘
+        Prod.map (RelStructure.restrict fun s => (e s).toEmbedding)
+          (latentRestrictOver (fun s => (e s).toEmbedding) n) =
+      Prod.map (restSpaceCongr e n A) (latentCongrOver e n) ∘
+        restObservationOver n (supportImage (fun s => (e s).toEmbedding) A) := by
+  funext p
+  rfl
+
 end RelSignature
diff --git a/Graphon/RelPooledAcceptance.lean b/Graphon/RelPooledAcceptance.lean
index 54f9d3a..086b5a5 100644
--- a/Graphon/RelPooledAcceptance.lean
+++ b/Graphon/RelPooledAcceptance.lean
@@ -5,6 +5,8 @@ Authors: Cameron Freer
 -/
 import Graphon.RelPooledExtension
 import Graphon.RelStationaryExtension
+import Graphon.ForMathlib.CondExpComap
+import Graphon.ForMathlib.CondIndepSup
 
 /-!
 # The joint restriction theorem for a pooled rank extension (R4 converse, #107)
@@ -32,7 +34,7 @@ extension absorbs `ρ`. Choosing `ρ` separately on each sort is exactly what th
 permits — no finite-support or uniform-bound issue arises.
 -/
 
-open MeasureTheory
+open MeasureTheory ProbabilityTheory
 
 namespace RelSignature
 
@@ -350,6 +352,73 @@ theorem PooledRankExtension.lower_recovers {C : M.RankRepresentation n}
           ((blockSpaceCongr e A₀).symm_apply_apply _).symm
       _ = _ := by rw [hp']; rfl
 
+/-! ### Consequence 4: screening on pooled supports -/
+
+open scoped Classical in
+/-- **Screening holds on every pooled support of rank `n`** — mixed supports included. Pure
+assembly: pull `C.screening` back through the canonical identification, strip the output
+equivalences with `CondIndepFun.comp`, and straighten the conditioning algebra with
+`CondIndepFun.congr_cond`. No conditional-expectation reasoning appears. -/
+theorem PooledRankExtension.screening {C : M.RankRepresentation n}
+    (Q : PooledRankExtension C) (A : Finset (Σ s : S.Srt, PoolVertex S s)) (hA : A.card = n) :
+    CondIndepFun (MeasurableSpace.comap (localLatentsOver A n ∘ Prod.snd) inferInstance)
+      (((measurable_localLatentsOver A n).comp measurable_snd).comap_le)
+      (blockMapOver A ∘ Prod.fst) (restObservationOver n A)
+      (Q.law : Measure (RelStructure S (PoolVertex S) × PooledRankLatentSpace S n)) := by
+  haveI := C.isProbabilityMeasure_P
+  classical
+  set eqv : ∀ s, Vinfinite S s ≃ PoolVertex S s := fun s => (poolVertexEquiv S s).symm with heqv
+  set e : ∀ s, Vinfinite S s ↪ PoolVertex S s := fun s => (eqv s).toEmbedding with he
+  obtain ⟨A₀, hA₀card, rfl⟩ :
+      ∃ A₀ : Finset (Σ s : S.Srt, Vinfinite S s), A₀.card = n ∧ supportImage e A₀ = A := by
+    refine ⟨supportImage (fun s => (poolVertexEquiv S s).toEmbedding) A, ?_, ?_⟩
+    · rw [card_supportImage]; exact hA
+    · rw [he, heqv]; exact supportImage_symm_supportImage (fun s => poolVertexEquiv S s) A
+  -- step 1: pull the representation's screening back along the canonical identification
+  have hpull := condIndepFun_comp_measurePreserving Q.measurePreserving_pooledJointEquiv
+    ((measurable_localLatents A₀ n).comp measurable_snd).comap_le
+    ((measurable_blockMap A₀).comp measurable_fst) (measurable_restObservation n A₀)
+    (C.screening A₀ hA₀card)
+  -- step 2: strip the output equivalences (post-composition never touches the dependent proof)
+  have hstrip := hpull.comp (blockSpaceCongr e A₀).symm.measurable
+    ((restSpaceCongr eqv n A₀).prodCongr (latentCongrOver eqv n)).symm.measurable
+  have hf : ⇑(blockSpaceCongr e A₀).symm ∘
+      ((blockMap A₀ ∘ Prod.fst) ∘ ⇑(pooledJointEquiv S n)) =
+      blockMapOver (supportImage e A₀) ∘ Prod.fst := by
+    rw [pooledJointEquiv_coe]
+    funext p
+    show (blockSpaceCongr e A₀).symm (blockMapOver A₀ (RelStructure.restrict e p.1)) = _
+    have hnat := congrFun (blockMapOver_restrict e A₀) p.1
+    simp only [Function.comp_apply] at hnat
+    rw [hnat]
+    simp
+  have hg : ⇑((restSpaceCongr eqv n A₀).prodCongr (latentCongrOver eqv n)).symm ∘
+      (restObservation n A₀ ∘ ⇑(pooledJointEquiv S n)) =
+      restObservationOver n (supportImage e A₀) := by
+    rw [pooledJointEquiv_coe]
+    funext p
+    show ((restSpaceCongr eqv n A₀).prodCongr (latentCongrOver eqv n)).symm
+      (restObservationOver n A₀ (Prod.map (RelStructure.restrict e)
+        (latentRestrictOver (S := S) e n) p)) = _
+    have hnat := congrFun (restObservationOver_congrCarrier eqv n A₀) p
+    simp only [Function.comp_apply] at hnat
+    rw [hnat, show Prod.map (⇑(restSpaceCongr eqv n A₀)) (⇑(latentCongrOver eqv n)) =
+        ⇑((restSpaceCongr eqv n A₀).prodCongr (latentCongrOver eqv n)) from rfl,
+      MeasurableEquiv.symm_apply_apply]
+  rw [hf, hg] at hstrip
+  -- step 3: straighten the conditioning algebra
+  refine hstrip.congr_cond ?_ _
+  rw [MeasurableSpace.comap_comp,
+    show (localLatents A₀ n ∘ Prod.snd) ∘ ⇑(pooledJointEquiv S n) =
+      ⇑(localLatentSpaceCongr e A₀ n) ∘
+        (localLatentsOver (supportImage e A₀) n ∘ Prod.snd) from by
+      rw [pooledJointEquiv_coe]
+      funext p
+      have hnat := congrFun (localLatentsOver_latentRestrictOver e A₀ n) p.2
+      simp only [Function.comp_apply] at hnat ⊢
+      exact hnat]
+  exact comap_measurableEquiv_comp (localLatentSpaceCongr e A₀ n) _
+
 end InfiniteRelExchangeableLaw
 
 end RelSignature
diff --git a/scripts/axiom_audit.lean b/scripts/axiom_audit.lean
index c0a1d78..a5bb63e 100644
--- a/scripts/axiom_audit.lean
+++ b/scripts/axiom_audit.lean
@@ -332,6 +332,8 @@ custom axioms. Target list and policy: `scripts/check_census_and_axioms.py`
 #print axioms RelSignature.InfiniteRelExchangeableLaw.PooledRankExtension.map_snd
 #print axioms RelSignature.InfiniteRelExchangeableLaw.PooledRankExtension.toStationaryExtension
 #print axioms RelSignature.InfiniteRelExchangeableLaw.PooledRankExtension.lower_recovers
+#print axioms RelSignature.restObservationOver_congrCarrier
+#print axioms RelSignature.InfiniteRelExchangeableLaw.PooledRankExtension.screening
 #print axioms MeasureTheory.condExp_comp_measurePreserving
 #print axioms ProbabilityTheory.condExp_set_comp_measurePreserving
 #print axioms ProbabilityTheory.condIndepFun_comp_measurePreserving
diff --git a/scripts/check_census_and_axioms.py b/scripts/check_census_and_axioms.py
index a9e6c7b..9e3af0f 100644
--- a/scripts/check_census_and_axioms.py
+++ b/scripts/check_census_and_axioms.py
@@ -297,6 +297,8 @@
     "RelSignature.InfiniteRelExchangeableLaw.PooledRankExtension.map_snd",
     "RelSignature.InfiniteRelExchangeableLaw.PooledRankExtension.toStationaryExtension",
     "RelSignature.InfiniteRelExchangeableLaw.PooledRankExtension.lower_recovers",
+    "RelSignature.restObservationOver_congrCarrier",
+    "RelSignature.InfiniteRelExchangeableLaw.PooledRankExtension.screening",
     "MeasureTheory.condExp_comp_measurePreserving",
     "ProbabilityTheory.condExp_set_comp_measurePreserving",
     "ProbabilityTheory.condIndepFun_comp_measurePreserving",

From a9c8e82522ccc0d8933997b8f66ad183918bf69d Mon Sep 17 00:00:00 2001
From: Cameron Freer <cameronfreer@gmail.com>
Date: Sun, 16 Aug 2026 15:52:02 +0000
Subject: [PATCH 13/13] =?UTF-8?q?docs:=20cleanup=20before=20merge=20?=
 =?UTF-8?q?=E2=80=94=20three=20closure=20properties,=20authoritative=20hea?=
 =?UTF-8?q?der,=20drop=20superseded=20restatements=20(#195)?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

CondIndepSup now says three closure properties and documents
CondIndepFun.congr_cond, in the module header and the Graphon.lean
bullet.

RelPooledAcceptance's module header names law_eq and all four
consequences, so it stays authoritative when the umbrella inventory is
trimmed (#167).

Removed two superseded restatements with no consumers:
map_poolVertexEquiv_congr (strictly weaker than law_eq) and
pooledExtension_map_restrict_embedding (identical to
(C.pooledExtension).map_restrict_embedding with no simpler hypotheses).
Neither was audited, so the audit count is unchanged.
---
 Graphon.lean                         |  2 +-
 Graphon/ForMathlib/CondIndepSup.lean | 10 ++++++--
 Graphon/RelPooledAcceptance.lean     | 38 ++++++++++++----------------
 3 files changed, 25 insertions(+), 25 deletions(-)

diff --git a/Graphon.lean b/Graphon.lean
index 6ba995a..752af38 100644
--- a/Graphon.lean
+++ b/Graphon.lean
@@ -248,7 +248,7 @@ in Lean 4 using Mathlib.
 * `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: two 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
+* `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
diff --git a/Graphon/ForMathlib/CondIndepSup.lean b/Graphon/ForMathlib/CondIndepSup.lean
index 9f28962..fcf17bc 100644
--- a/Graphon/ForMathlib/CondIndepSup.lean
+++ b/Graphon/ForMathlib/CondIndepSup.lean
@@ -6,9 +6,9 @@ Authors: Cameron Freer
 import Mathlib.Probability.Independence.Conditional
 
 /-!
-# Two closure properties of conditional independence
+# Three closure properties of conditional independence
 
-Both are glue Mathlib does not currently provide.
+All three are glue Mathlib does not currently provide.
 
 * **Joining the conditioning algebra to one side is free**: from `m₁ ⊥⊥ m₂ ∣ m'` conclude
   `m₁ ⊥⊥ (m' ⊔ m₂) ∣ m'`. Whatever the conditioning algebra already knows cannot carry new
@@ -24,6 +24,12 @@ Both are glue Mathlib does not currently provide.
 
 Neither statement mentions this repository's signatures. The `[StandardBorelSpace Ω]` hypotheses
 come with Mathlib's definition of `CondIndep`/`CondIndepFun` through `condExpKernel`.
+
+* **The conditioning σ-algebra may be replaced by an equal one** (`CondIndepFun.congr_cond`): the
+  dependent `≤` proof moves by proof irrelevance once the σ-algebra equality is substituted. Needed
+  wherever a conditioning map is reindexed — the rank-one coupling and screening arguments and the
+  pooled screening transport all consume it.
+
 -/
 
 open MeasureTheory
diff --git a/Graphon/RelPooledAcceptance.lean b/Graphon/RelPooledAcceptance.lean
index 086b5a5..bab314e 100644
--- a/Graphon/RelPooledAcceptance.lean
+++ b/Graphon/RelPooledAcceptance.lean
@@ -25,8 +25,22 @@ This is joint, not a structure marginal: the structure and the latents are restr
 same embedding, so it recovers the joint `(X, U_{<n})` law and says strictly more than a
 structure-only window theorem.
 
-The proof is joint-cylinder extensionality together with finite agreement by a mixed pooled
-permutation. On a joint cylinder the combined vertex support is finite; the partial assignment
+Cancelling that restriction at the canonical embedding gives `PooledRankExtension.law_eq`, a
+**uniqueness theorem**: every pooled rank extension is the cheap one, `(C.pooledExtension)`. The
+four route-neutral consequences of the gate are transports through that single identity:
+
+* `PooledRankExtension.map_snd` — the pooled latent marginal is the pooled i.i.d. source;
+* `PooledRankExtension.toStationaryExtension` — the structure marginal is a `StationaryExtension M`;
+* `PooledRankExtension.lower_recovers` — local recovery on every pooled support below rank `n`, the
+  decoder conjugated through the local and block measurable equivalences;
+* `PooledRankExtension.screening` — screening on every pooled support of rank `n`, assembled from
+  `condIndepFun_comp_measurePreserving`, `CondIndepFun.comp` on the codomains, and
+  `CondIndepFun.congr_cond` with `comap_measurableEquiv_comp` on the conditioning algebra.
+
+Nothing route-specific appears: no fresh rank-`n` latent extraction and nothing at rank `n + 1`.
+
+The joint restriction theorem is proved by joint-cylinder extensionality together with finite
+agreement by a mixed pooled permutation. On a joint cylinder the combined vertex support is finite; the partial assignment
 `originalVertex v ↦ e v` on it is a finite partial injection of the pooled carrier, since both
 embeddings are injective, so it extends to a pooled permutation `ρ` with `ρ (ov v) = e v` there.
 Both restrictions then read the same moved coordinates, and the full mixed invariance of the
@@ -185,18 +199,6 @@ theorem PooledRankExtension.map_poolVertexEquiv {C : M.RankRepresentation n}
           (latentRestrictOver (fun s => (poolVertexEquiv S s).symm.toEmbedding) n)) = C.P :=
   Q.map_restrict_embedding _
 
-/-- **Any two pooled rank extensions agree after the canonical identification.** Both are carried
-to the same representation, so the pooled object is unique as far as that identification sees. -/
-theorem PooledRankExtension.map_poolVertexEquiv_congr {C : M.RankRepresentation n}
-    (Q Q' : PooledRankExtension C) :
-    (Q.law : Measure (RelStructure S (PoolVertex S) × PooledRankLatentSpace S n)).map
-        (Prod.map (RelStructure.restrict fun s => (poolVertexEquiv S s).symm.toEmbedding)
-          (latentRestrictOver (fun s => (poolVertexEquiv S s).symm.toEmbedding) n)) =
-      (Q'.law : Measure (RelStructure S (PoolVertex S) × PooledRankLatentSpace S n)).map
-        (Prod.map (RelStructure.restrict fun s => (poolVertexEquiv S s).symm.toEmbedding)
-          (latentRestrictOver (fun s => (poolVertexEquiv S s).symm.toEmbedding) n)) := by
-  rw [Q.map_poolVertexEquiv, Q'.map_poolVertexEquiv]
-
 /-! ### The canonical law identity -/
 
 variable (S n) in
@@ -250,14 +252,6 @@ theorem PooledRankExtension.measurePreserving_pooledJointEquiv {C : M.RankRepres
   ⟨(pooledJointEquiv S n).measurable, by
     rw [pooledJointEquiv_coe]; exact Q.map_poolVertexEquiv⟩
 
-/-- The cheap extension satisfies the joint restriction theorem, for every embedding. -/
-theorem RankRepresentation.pooledExtension_map_restrict_embedding (C : M.RankRepresentation n)
-    (e : ∀ s, Vinfinite S s ↪ PoolVertex S s) :
-    ((C.pooledExtension).law :
-        Measure (RelStructure S (PoolVertex S) × PooledRankLatentSpace S n)).map
-      (Prod.map (RelStructure.restrict e) (latentRestrictOver e n)) = C.P :=
-  (C.pooledExtension).map_restrict_embedding e
-
 /-! ### Consequence 1: the pooled latent marginal -/
 
 /-- **The pooled latent marginal is the pooled i.i.d. source.** A transport of `C.map_snd` through