From 24cc10c13737de08dac5688985573bdd588b28a4 Mon Sep 17 00:00:00 2001
From: Cameron Freer <cameronfreer@gmail.com>
Date: Sat, 22 Aug 2026 03:01:03 +0000
Subject: [PATCH 01/13] =?UTF-8?q?feat:=20Austin=20route=20unit=201=20(#197?=
 =?UTF-8?q?)=20=E2=80=94=20pooled=20polling=20interface=20and=20its=20exac?=
 =?UTF-8?q?t=20export?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Route A only. No Kallenberg machinery, and nothing here asserts the two routes'
outputs agree.

**The conditioning is pinned, not quantified.** `pollingObs` is a concrete
observation: the whole pooled rank-`n` latent array — every index of which has
cardinality `< n`, so it is proper-subset data carrying no rank-`n` block — together
with the structure read on the **spare** copy of the carrier, which is the poll.
An existential conditioning factor would let a witness condition on the whole joint
object and make the conclusion vacuous.

**The conclusion is mutual.** `PooledPollingWitness.mutualCondIndep` is
`iCondIndepFun` over the *entire* rank-`n` block family, which is Austin's
Proposition 3.12 conclusion. Pairwise independence, or one block against the rest,
would be strictly weaker — the #196 battery is what keeps that distinction honest.

**The export is not a pullback along a restriction.** `map_restrict_embedding`
pushes the pooled law forward onto `C.P` and is not invertible. The transport
therefore runs along the canonical equivalence's **inverse** measure-preserving map,
whose law identity is `map_poolVertexEquiv` — literally `Q.map_restrict_embedding`
at the canonical embedding. Verified mechanically: the gate theorem is transitively
reachable in the compiled dependency graph of `iCondIndepFun_blockMap`, and a
control theorem is not.

The block family is read through `pooledJointEquiv` rather than `originalVertex` so
that the export is an exact identification: composing two restrictions restricts
along the composite embedding, which is not the identity and would leave an
irreducible reindexing. The spare copy still enters, through `pollingObs`.

Scope: carries `[Fintype S.Srt]` to match the polling/fixing-algebra stack, leaving
the pooled API countable-only; rank zero is left to `nonempty_rankRepresentation_one`
with `truncation_zero`, respecting `stepKernel`'s lack of an `A = ∅` realization.

`iCondIndepFun_congr_cond` is private — the `CondIndepFun` form is already shared
glue, and this counterpart has one consumer.

Audit 426 → 429. Gates: lake build clean (3409 jobs), census + axiom audit pass,
zero sorries.
---
 Graphon.lean                       |   2 +
 Graphon/RelAustinPolling.lean      | 186 +++++++++++++++++++++++++++++
 scripts/axiom_audit.lean           |   5 +
 scripts/check_census_and_axioms.py |   3 +
 4 files changed, 196 insertions(+)
 create mode 100644 Graphon/RelAustinPolling.lean

diff --git a/Graphon.lean b/Graphon.lean
index dc3fe40..129aa3c 100644
--- a/Graphon.lean
+++ b/Graphon.lean
@@ -48,6 +48,7 @@ import Graphon.RelObservationGeometry
 import Graphon.RelPooledLatents
 import Graphon.RelPooledExtension
 import Graphon.RelPooledAcceptance
+import Graphon.RelAustinPolling
 import Graphon.RelRankSuccessorContract
 import Graphon.DigraphCoordSupport
 import Graphon.RelBipartiteRegression
@@ -273,6 +274,7 @@ in Lean 4 using Mathlib.
 * `Graphon.RelPooledAcceptance` — R4 converse (#107), stage 3 of the pooled-latent extension gate, organizing result: **the joint restriction theorem**. For *every* sortwise embedding `e : ∀ s, Vinfinite S s ↪ PoolVertex S s`, restricting a pooled rank extension jointly — structure and latents along the same embedding — returns the representation exactly: `Q.law.map (Prod.map (RelStructure.restrict e) (latentRestrictOver e n)) = C.P`. Being **joint** is the point: it recovers the `(X, U_{<n})` law and says strictly more than a structure-only window theorem. Proved by joint-cylinder extensionality plus finite agreement with a mixed pooled permutation — on a cylinder the combined vertex support is finite, the assignment `originalVertex v ↦ e v` there is a finite partial injection of the pooled carrier, and `exists_perm_extend_of_injOn` extends it; the full mixed invariance then absorbs the permutation, which is also what lets it be chosen independently on each sort with no finite-support or uniform-bound issue. The four route-neutral consequences follow from it: `map_snd` (the pooled latent marginal is the pooled i.i.d. source), `toStationaryExtension` (the structure marginal is a `StationaryExtension M`), `lower_recovers` (local recovery on every pooled support below rank `n`, the decoder conjugated through the local and block measurable equivalences), and `screening` (screening on every pooled support of rank `n`, a pullback through `measurePreserving_pooledJointEquiv` followed by `CondIndepFun.comp` on the codomains and `CondIndepFun.congr_cond` with `comap_measurableEquiv_comp` on the conditioning algebra — no conditional-expectation reasoning). `PooledRankExtension.map_poolVertexEquiv` is the canonical specialization; bundling that restriction as the measurable equivalence `pooledJointEquiv` and cancelling it yields **`PooledRankExtension.law_eq`, a uniqueness theorem** — every pooled rank extension *is* the cheap one. Marginals, the `StationaryExtension` structure, recovery and screening therefore transport from `C.P` through one canonical law identity rather than requiring separate measure arguments
 * `Graphon.RelRankSuccessorContract` — R4 converse (#107), **interface only**: the shared witness both successor constructions must produce, and the two identically typed statements they target. `RankSuccessor C` carries the next representation together with **exact truncation compatibility**, `next.P.map (Prod.map id (rankLatentProjection (Nat.le_succ n))) = C.P` — the observable that makes the statement mention `C` at all. A theorem returning merely `Nonempty (RankRepresentation (n + 1))` could ignore `C` and produce an unrelated representation, which is the same underdetermination that sank the earlier shell attempt. The witness carries **no independence field** beyond `RankRepresentation`'s own, and **no equality between the two routes' outputs** is asserted — they prove one statement by different means and will not produce canonically equal representations. `AustinSuccessor` and `KallenbergSuccessor` are the same proposition by construction, so whichever lands first discharges the induction while the other remains an independent proof. Regression: `truncation_zero` shows the truncation equation is **automatic at rank zero** — the rank-zero latent cube is a single point, so both sides are determined by their structure marginals, which the representation axioms already pin, and the base case imposes nothing extra. The witness exposes no pooled carrier, so whether a construction genuinely used boundary-crossing permutations is observed by the pooled gate's `map_restrict_embedding` rather than by any final-output check here; each route's intermediate construction consumes that theorem. Adversarial examples are kept in route-independent regression modules, outside this interface
 * `Graphon.DigraphCoordSupport` — shared regression infrastructure: the support of a digraph coordinate is the pair of its endpoints, with the off-diagonal cardinality corollary, over an arbitrary vertex type. A bridge module so that the D1 carrier `Graphon.InfiniteDigraph` does not acquire a dependency on the equality-pattern layer where `RelCoord.support` lives — the same separation `Graphon.SimpleGraphDigraphBridge` maintains for `SimpleGraph`. Stated with `[DecidableEq V]` and proved by membership, because `RelCoord.support` is built classically and over a concrete carrier the natural instance is not definitionally the classical one, so an image-shaped statement would not apply at the sites that need it
+* `Graphon.RelAustinPolling` — R4 converse (#107/#197), **route A (Austin) unit 1**: pooled polling. Austin's Proposition 3.12 runs its polling with swaps into a *spare vertex set*, and the pooled carrier is exactly that — `originalVertex` and `poolVertex` are disjoint embeddings of the original carrier, and a `PooledRankExtension` is invariant under the **full** pooled permutation family, so the swaps need no finite-support side condition. `pollingObs` pins the conditioning **concretely** — the whole pooled rank-`n` latent array (every index of which has cardinality `< n`, hence carries no rank-`n` block) together with the structure read on the spare copy; an existential conditioning factor would make the conclusion vacuous. `PooledPollingWitness.mutualCondIndep` is `iCondIndepFun` over the **entire** rank-`n` block family — mutual, not pairwise and not one-block-against-the-rest, which is Austin's actual conclusion and what the #196 battery exists to keep honest. `iCondIndepFun_blockMap` exports the consequence to `C.P` along the canonical equivalence's **inverse** measure-preserving map: `map_restrict_embedding` pushes the pooled law forward and is not invertible, so this is not a pullback along a restriction, and that gate theorem is a compiled dependency of the export rather than a citation. Carries `[Fintype S.Srt]`, matching the polling/fixing-algebra stack; the pooled API stays countable-only. Rank zero is not handled here — it is supplied by `nonempty_rankRepresentation_one` with `truncation_zero`, which respects `stepKernel`'s deliberate lack of an `A = ∅` realization theorem
 * `Graphon.RelBipartiteRegression` — R4 converse (#107/#196): the **bipartite regression** for the successor contract, a hand-built rank `1 → 2` witness over `digraphSig` whose purpose is to test that `RankSuccessor` is an expressive specification *before* either route is attempted. Each vertex carries an i.i.d. colour on its own fresh singleton coordinate and the edge is the parity, so the diagonal is constantly `false` for free. Three independent things make it a regression rather than a construction: the array law is defined **from the fresh singleton layer alone** and the rank-one coupling as the independent product `bipartiteLaw × rankLatentSource 1`, so `rankTwoCoupling_truncation` compares two separately described couplings and genuinely consumes the source factorization; the rank-two block decoder recovers **both** directed coordinates `X_uv` and `X_vu` as the same parity, exhibiting symmetry as a property of this law rather than of the signature; and `not_indepFun_rankTwoCoupling` is **numerical** — the edge and colour-parity events coincide with probability `1/2` against a product of marginals `1/4`, which a constant edge could not achieve even though it too would be "a function of the colours". `bipartiteSuccessor : RankSuccessor rankOneRep` is the witness itself
 * `Graphon.RelIidEdgeRegression` — R4 converse (#107/#196): the **i.i.d.-edge regression** for the successor contract, a hand-built rank `2 → 3` witness over `digraphSig` that tests **staging and recovery** where the bipartite regression tested independence and symmetry. The array is keyed by a coordinate's *support*, which gives symmetry (`X_uv = X_vu`) and the empty diagonal by construction — each is still proved from a support computation, but neither requires a choice of orientation. Two things make it a regression rather than a construction. First, recovery is genuinely staged: at rank three a two-point block is decoded from the latent coordinate at its own support — carried by the rank-three array because `2 < 3` — while at rank two the same blocks are not latent-measurable at all, so the two ranks exercise opposite sides of `lower_recovers`. Second, rank-two screening is a genuine conditional-independence statement: the block reads one coordinate of the edge source and the remainder reads the others plus the whole latent array, so screening follows from **independence**, not from determinism as in the bipartite case. `iidEdgeLaw_edge_eq_half` pins the edge probability at exactly `1/2`, which rules out a *constant* block; that the block is not measurable from the old latents is a separate fact, supplied by the product independence built into the rank-two coupling. The private conditional-independence lemma is stated for abstract σ-algebras rather than for the two coordinates of a product because the ambient measure is a pushforward of a product and the current API only transports conditional independence **backward**: a source-level proof would require a new forward law-transport theorem, whereas transporting the unconditional independence needs no new theorem. `iidEdgeSuccessor : RankSuccessor rankTwoRep` is the witness itself
 * `Graphon.RelRankInjectionInvariance` — R4 converse (#107), the isolated proof risk of the pooled-latent extension gate: **joint invariance under arbitrary sortwise self-injections**. `RankRepresentation.invariant` is stated for *finitely supported permutations*, but a pooled object built cheaply through `poolVertexEquiv` needs the joint law invariant under every self-injection; `RankRepresentation.map_prodMap_restrict_self` supplies exactly that, so full mixed pooled invariance later costs no additional mathematics. The route is finite-cylinder extensionality on the **joint** space, which had no machinery before — rank one's joint invariance goes through only because the rank-one latent action is trivial. `rankLatentIndexInj`/`rankLatentReindex` extend the latent action from permutations to injections (only injectivity is used — a support keeps its cardinality); `exists_finSuppPerm_agree_on_finset` matches an injection to a finitely supported permutation on any finite tagged-vertex support; `ext_of_prod_cylinders` is the joint extensionality, rectangles of coordinate cylinders on both factors. **No finiteness/`Fintype` hypothesis beyond `RankRepresentation`'s ambient countability.** Equality is tested on *coordinate* cylinders — finitely many `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
diff --git a/Graphon/RelAustinPolling.lean b/Graphon/RelAustinPolling.lean
new file mode 100644
index 0000000..a403442
--- /dev/null
+++ b/Graphon/RelAustinPolling.lean
@@ -0,0 +1,186 @@
+/-
+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.RelPooledAcceptance
+import Graphon.RelPollingInfrastructure
+import Graphon.ForMathlib.CondExpComap
+
+/-!
+# Pooled polling: the Austin route, unit 1 (R4 converse, #107, #197)
+
+Route **A** (Austin) only. Nothing from the Kallenberg spine appears here, and nothing in this
+module asserts that the two routes' outputs agree — they prove the same statement by different
+means and will not produce canonically equal representations.
+
+Austin's Proposition 3.12 (arXiv:0801.1698) runs its polling argument with finitely supported
+swaps into a **spare vertex set**. The pooled carrier is exactly that spare set: `originalVertex`
+and `poolVertex` are two disjoint embeddings of the original carrier into `PoolVertex`, and a
+`PooledRankExtension` is invariant under the *full* pooled permutation family, so the swaps are
+available without a finite-support or uniform-bound side condition.
+
+## What this unit fixes
+
+* `pollingObs` — the **concrete** polling observation, not an existential factor: the whole pooled
+  rank-`n` latent array together with the structure read on the spare copy. Every latent index of
+  `RankLatentIndex S n` has cardinality `< n`, so this is proper-subset data by construction and
+  carries no rank-`n` block; the spare-copy structure is the poll. Conditioning on the whole joint
+  object would make the conclusion vacuous, which is why the observation is pinned here rather
+  than quantified over.
+* `pooledBlock` — the rank-`n` block family, read through the canonical identification
+  `pooledJointEquiv`. Reading it through `originalVertex` instead would be equally meaningful but
+  would not transport *exactly*: composing two restrictions restricts along the composite
+  embedding, which is not the identity, and the export below would acquire an irreducible
+  reindexing. The spare copy still enters — through `pollingObs`, which is where the poll belongs.
+* `PooledPollingWitness` — the obligations a polling argument must discharge, with the mutual
+  conclusion as the load-bearing field.
+
+## The mutual conclusion, and why pairwise would not do
+
+The field is `iCondIndepFun` over the **entire** rank-`n` block family — mutual conditional
+independence, not pairwise and not one-block-against-the-rest. That is Austin's actual conclusion,
+and the weaker forms are genuinely weaker: the bipartite regression of #196 exhibits blocks that
+are pairwise related in ways a family-level statement rules out, which is exactly why the battery
+was built before either route was attempted.
+
+## Transport
+
+`PooledPollingWitness.iCondIndepFun_blockMap` moves the conclusion from `Q.law` to `C.P`. The
+direction matters. `map_restrict_embedding` maps the pooled law *forward* onto `C.P` and is not
+invertible, so this is **not** a pullback along a restriction; the transport runs along the
+canonical measurable equivalence `pooledJointEquiv` and its **inverse** measure-preserving map,
+whose law identity is `PooledRankExtension.map_poolVertexEquiv` — which is
+`Q.map_restrict_embedding` at the canonical embedding. The gate theorem is therefore a compiled
+proof dependency of the export, not a citation.
+
+## Scope
+
+* `[Fintype S.Srt]` is carried by this module, matching the polling/fixing-algebra stack it builds
+  on. The pooled API itself remains countable-only; removing the hypothesis is a separate
+  generalization and deliberately not attempted here.
+* Rank zero is not this module's business. The successor at `n = 0` is supplied by
+  `nonempty_rankRepresentation_one` together with `truncation_zero`, which is also what respects
+  `stepKernel`'s deliberate lack of an `A = ∅` realization theorem.
+-/
+
+open MeasureTheory ProbabilityTheory
+
+namespace RelSignature
+
+namespace InfiniteRelExchangeableLaw
+
+variable {S : RelSignature} [Countable S.Srt] [Countable S.Rel]
+  {M : InfiniteRelExchangeableLaw S} {n : ℕ}
+
+attribute [local instance] RankRepresentation.isProbabilityMeasure_P
+
+/-- **The conditioning σ-algebra may be replaced by an equal one**, for a family. The `CondIndepFun`
+form is shared glue in `ForMathlib/CondIndepSup.lean`; this is its `iCondIndepFun` counterpart, kept
+private until a second consumer appears. Needed because the conditioning algebra occurs in a
+dependent position — the `≤` proof mentions it — so `rw` cannot reach it. -/
+private theorem iCondIndepFun_congr_cond {Ω : Type*} [mΩ : MeasurableSpace Ω]
+    [StandardBorelSpace Ω] {μ : Measure Ω} [IsFiniteMeasure μ]
+    {ι : Type*} {γ : ι → Type*} [∀ i, MeasurableSpace (γ i)] {Y : ∀ i, Ω → γ i}
+    {m₁ m₂ : MeasurableSpace Ω} {h1 : m₁ ≤ mΩ} (h : iCondIndepFun m₁ h1 Y μ)
+    (h12 : m₁ = m₂) (h2 : m₂ ≤ mΩ) : iCondIndepFun m₂ h2 Y μ := by
+  subst h12
+  exact h
+
+/-! ### The polling observation -/
+
+variable (S n) in
+/-- The codomain of the polling observation: the pooled rank-`n` latent array together with a
+structure on the spare copy. -/
+abbrev PollingSpace :=
+  PooledRankLatentSpace S n × RelStructure S (Vinfinite S)
+
+variable (S n) in
+/-- **The polling observation.** The whole pooled rank-`n` latent array — every index of which has
+cardinality `< n`, hence is proper-subset data carrying no rank-`n` block — together with the
+structure read on the **spare** copy of the carrier, which is the poll. Pinned concretely: an
+arbitrary conditioning factor would make the mutual conclusion vacuous. -/
+noncomputable def pollingObs :
+    RelStructure S (PoolVertex S) × PooledRankLatentSpace S n → PollingSpace S n :=
+  fun p => (p.2, RelStructure.restrict (poolVertex S) p.1)
+
+variable (S n) in
+theorem measurable_pollingObs : Measurable (pollingObs S n) :=
+  measurable_snd.prodMk ((measurable_restrict _).comp measurable_fst)
+
+/-! ### The rank-`n` block family -/
+
+/-- **The rank-`n` block family on the pooled space**, read through the canonical identification.
+Indexed by the original rank-`n` supports, with a fixed codomain per index, which is what lets the
+export below be an exact identification rather than a reindexing. -/
+noncomputable def pooledBlock (A : RankSupport S n) :
+    RelStructure S (PoolVertex S) × PooledRankLatentSpace S n → BlockSpace (S := S) A.1 :=
+  fun p => blockMap A.1 (pooledJointEquiv S n p).1
+
+theorem measurable_pooledBlock (A : RankSupport S n) : Measurable (pooledBlock (S := S) (n := n) A) :=
+  (measurable_blockMap A.1).comp ((pooledJointEquiv S n).measurable.fst)
+
+omit [Countable S.Srt] [Countable S.Rel] in
+/-- Composing the pooled block family with the inverse identification returns the block of the
+original structure, on the nose. -/
+theorem pooledBlock_comp_symm (A : RankSupport S n) :
+    pooledBlock (S := S) (n := n) A ∘ (pooledJointEquiv S n).symm =
+      blockMap A.1 ∘ Prod.fst := by
+  funext p
+  show blockMap A.1 (pooledJointEquiv S n ((pooledJointEquiv S n).symm p)).1 = _
+  rw [MeasurableEquiv.apply_symm_apply]
+  rfl
+
+/-! ### The witness -/
+
+variable [Fintype S.Srt]
+
+/-- **What a polling argument must supply.** The mutual conditional independence of the *entire*
+rank-`n` block family given the polling observation — Austin's Proposition 3.12 conclusion in this
+setting. The observation is not a field: it is pinned by `pollingObs`, so that a witness cannot
+discharge the obligation by conditioning on more than proper-subset and spare-pool data. -/
+structure PooledPollingWitness (C : M.RankRepresentation n) (Q : PooledRankExtension C) where
+  /-- **Mutual** conditional independence of the whole rank-`n` block family, given the polling
+  observation. Pairwise independence, or one block against the rest, would not suffice. -/
+  mutualCondIndep :
+    iCondIndepFun (MeasurableSpace.comap (pollingObs S n) inferInstance)
+      (measurable_pollingObs S n).comap_le
+      (fun A : RankSupport S n => pooledBlock (S := S) (n := n) A)
+      (Q.law : Measure (RelStructure S (PoolVertex S) × PooledRankLatentSpace S n))
+
+namespace PooledPollingWitness
+
+variable {C : M.RankRepresentation n} {Q : PooledRankExtension C}
+
+/-- **The exact consequence under `C.P`.** The rank-`n` blocks of the representation are mutually
+conditionally independent given the polling observation transported to the original carrier.
+
+The transport is along the canonical equivalence's **inverse** measure-preserving map, not along
+the non-invertible restriction: `map_restrict_embedding` pushes the pooled law forward onto `C.P`,
+and it is exactly that identity — through `map_poolVertexEquiv` and
+`measurePreserving_pooledJointEquiv` — which makes the inverse measure preserving. The gate
+theorem is a compiled dependency of this proof. -/
+theorem iCondIndepFun_blockMap (W : PooledPollingWitness C Q) :
+    iCondIndepFun
+      (MeasurableSpace.comap (pollingObs S n ∘ (pooledJointEquiv S n).symm) inferInstance)
+      ((measurable_pollingObs S n).comp (pooledJointEquiv S n).symm.measurable).comap_le
+      (fun A : RankSupport S n => blockMap A.1 ∘ Prod.fst) C.P := by
+  haveI := C.isProbabilityMeasure_P
+  have hsymm : MeasurePreserving ((pooledJointEquiv S n).symm) C.P
+      (Q.law : Measure (RelStructure S (PoolVertex S) × PooledRankLatentSpace S n)) :=
+    MeasurePreserving.symm _ Q.measurePreserving_pooledJointEquiv
+  have h := iCondIndepFun_comp_measurePreserving hsymm
+    (measurable_pollingObs S n).comap_le
+    (fun A : RankSupport S n => measurable_pooledBlock A) W.mutualCondIndep
+  have hfam : (fun A : RankSupport S n =>
+        pooledBlock (S := S) (n := n) A ∘ (pooledJointEquiv S n).symm) =
+      fun A : RankSupport S n => blockMap A.1 ∘ Prod.fst :=
+    funext fun A => pooledBlock_comp_symm A
+  rw [hfam] at h
+  exact iCondIndepFun_congr_cond h MeasurableSpace.comap_comp _
+
+end PooledPollingWitness
+
+end InfiniteRelExchangeableLaw
+
+end RelSignature
diff --git a/scripts/axiom_audit.lean b/scripts/axiom_audit.lean
index 874c88c..cb435b0 100644
--- a/scripts/axiom_audit.lean
+++ b/scripts/axiom_audit.lean
@@ -347,6 +347,11 @@ custom axioms. Target list and policy: `scripts/check_census_and_axioms.py`
 #print axioms RelSignature.BipartiteRegression.ae_edge_xor
 #print axioms RelSignature.BipartiteRegression.not_indepFun_rankTwoCoupling
 
+-- R4 converse route A (#197): pooled polling, unit 1.
+#print axioms RelSignature.InfiniteRelExchangeableLaw.pollingObs
+#print axioms RelSignature.InfiniteRelExchangeableLaw.pooledBlock
+#print axioms RelSignature.InfiniteRelExchangeableLaw.PooledPollingWitness.iCondIndepFun_blockMap
+
 -- Shared digraph-coordinate support geometry (two regression consumers).
 #print axioms support_digraphCoord
 #print axioms card_support_digraphCoord
diff --git a/scripts/check_census_and_axioms.py b/scripts/check_census_and_axioms.py
index 280b7b4..ab1f650 100644
--- a/scripts/check_census_and_axioms.py
+++ b/scripts/check_census_and_axioms.py
@@ -307,6 +307,9 @@
     "RelSignature.BipartiteRegression.bipartiteSuccessor",
     "RelSignature.BipartiteRegression.ae_edge_xor",
     "RelSignature.BipartiteRegression.not_indepFun_rankTwoCoupling",
+    "RelSignature.InfiniteRelExchangeableLaw.pollingObs",
+    "RelSignature.InfiniteRelExchangeableLaw.pooledBlock",
+    "RelSignature.InfiniteRelExchangeableLaw.PooledPollingWitness.iCondIndepFun_blockMap",
     "support_digraphCoord",
     "card_support_digraphCoord",
     "RelSignature.mem_rankSupportPerm",

From 1c3dfe402bc01a633e944e16bdea9145fdbbbecb Mon Sep 17 00:00:00 2001
From: Cameron Freer <cameronfreer@gmail.com>
Date: Sat, 22 Aug 2026 22:45:22 +0000
Subject: [PATCH 02/13] fix: correct the original/spare geometry and move the
 seam to an enriched law (#197)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Two corrections to the unit-1 spike, both substantive.

**The geometry was wrong.** Reading the block family through `pooledJointEquiv` made
the export to `C.P` an exact identification, and that convenience is what broke it:
`poolVertexEquiv` is a bijection `PoolVertex ≃ Vinfinite`, so blocks read through it
range across *both* summands rather than being confined to the original half, while
the poll read the spare half — observed blocks and poll were not disjoint, and a
block that can itself lie in the poll makes the conditional independence say nothing.
Blocks are now confined to `supportImage (originalVertex S)` (all `Sum.inl`) and the
poll to supports containing at least one `Sum.inr`, so the two families are disjoint
by construction.

**The seam is an enriched law, not bare `C.P`.** Austin's polling data is the family
of *mixed* clusters straddling the two halves — not merely the induced structure on
the spare half — and it must survive into the next law rather than being forgotten.
`enrichedPollingLaw` retains the clusters alongside the original structure and old
latents; `enrichedPollingLaw_map_fst` recovers `C.P` exactly, proved through
`Q.map_restrict_embedding (originalVertex S)`. Verified mechanically that the gate
theorem is transitively reachable in the compiled dependency graph, with a control
theorem that is not.

`MixedClusterIndex` makes the "indexed by proper original subsets" reading precise:
a rank-`n` support carrying a spare vertex has a proper original part.

Audit names updated to the surviving declarations. Gates: lake build clean (3409
jobs), census + axiom audit pass, zero sorries.

Unit 1 is **not** complete: no witness is constructed yet, so the polling engine in
`RelPollingInfrastructure` is still unconsumed. No PR until it is.
---
 Graphon.lean                       |   2 +-
 Graphon/RelAustinPolling.lean      | 286 +++++++++++++++--------------
 scripts/axiom_audit.lean           |   6 +-
 scripts/check_census_and_axioms.py |   6 +-
 4 files changed, 160 insertions(+), 140 deletions(-)

diff --git a/Graphon.lean b/Graphon.lean
index 129aa3c..c402581 100644
--- a/Graphon.lean
+++ b/Graphon.lean
@@ -274,7 +274,7 @@ in Lean 4 using Mathlib.
 * `Graphon.RelPooledAcceptance` — R4 converse (#107), stage 3 of the pooled-latent extension gate, organizing result: **the joint restriction theorem**. For *every* sortwise embedding `e : ∀ s, Vinfinite S s ↪ PoolVertex S s`, restricting a pooled rank extension jointly — structure and latents along the same embedding — returns the representation exactly: `Q.law.map (Prod.map (RelStructure.restrict e) (latentRestrictOver e n)) = C.P`. Being **joint** is the point: it recovers the `(X, U_{<n})` law and says strictly more than a structure-only window theorem. Proved by joint-cylinder extensionality plus finite agreement with a mixed pooled permutation — on a cylinder the combined vertex support is finite, the assignment `originalVertex v ↦ e v` there is a finite partial injection of the pooled carrier, and `exists_perm_extend_of_injOn` extends it; the full mixed invariance then absorbs the permutation, which is also what lets it be chosen independently on each sort with no finite-support or uniform-bound issue. The four route-neutral consequences follow from it: `map_snd` (the pooled latent marginal is the pooled i.i.d. source), `toStationaryExtension` (the structure marginal is a `StationaryExtension M`), `lower_recovers` (local recovery on every pooled support below rank `n`, the decoder conjugated through the local and block measurable equivalences), and `screening` (screening on every pooled support of rank `n`, a pullback through `measurePreserving_pooledJointEquiv` followed by `CondIndepFun.comp` on the codomains and `CondIndepFun.congr_cond` with `comap_measurableEquiv_comp` on the conditioning algebra — no conditional-expectation reasoning). `PooledRankExtension.map_poolVertexEquiv` is the canonical specialization; bundling that restriction as the measurable equivalence `pooledJointEquiv` and cancelling it yields **`PooledRankExtension.law_eq`, a uniqueness theorem** — every pooled rank extension *is* the cheap one. Marginals, the `StationaryExtension` structure, recovery and screening therefore transport from `C.P` through one canonical law identity rather than requiring separate measure arguments
 * `Graphon.RelRankSuccessorContract` — R4 converse (#107), **interface only**: the shared witness both successor constructions must produce, and the two identically typed statements they target. `RankSuccessor C` carries the next representation together with **exact truncation compatibility**, `next.P.map (Prod.map id (rankLatentProjection (Nat.le_succ n))) = C.P` — the observable that makes the statement mention `C` at all. A theorem returning merely `Nonempty (RankRepresentation (n + 1))` could ignore `C` and produce an unrelated representation, which is the same underdetermination that sank the earlier shell attempt. The witness carries **no independence field** beyond `RankRepresentation`'s own, and **no equality between the two routes' outputs** is asserted — they prove one statement by different means and will not produce canonically equal representations. `AustinSuccessor` and `KallenbergSuccessor` are the same proposition by construction, so whichever lands first discharges the induction while the other remains an independent proof. Regression: `truncation_zero` shows the truncation equation is **automatic at rank zero** — the rank-zero latent cube is a single point, so both sides are determined by their structure marginals, which the representation axioms already pin, and the base case imposes nothing extra. The witness exposes no pooled carrier, so whether a construction genuinely used boundary-crossing permutations is observed by the pooled gate's `map_restrict_embedding` rather than by any final-output check here; each route's intermediate construction consumes that theorem. Adversarial examples are kept in route-independent regression modules, outside this interface
 * `Graphon.DigraphCoordSupport` — shared regression infrastructure: the support of a digraph coordinate is the pair of its endpoints, with the off-diagonal cardinality corollary, over an arbitrary vertex type. A bridge module so that the D1 carrier `Graphon.InfiniteDigraph` does not acquire a dependency on the equality-pattern layer where `RelCoord.support` lives — the same separation `Graphon.SimpleGraphDigraphBridge` maintains for `SimpleGraph`. Stated with `[DecidableEq V]` and proved by membership, because `RelCoord.support` is built classically and over a concrete carrier the natural instance is not definitionally the classical one, so an image-shaped statement would not apply at the sites that need it
-* `Graphon.RelAustinPolling` — R4 converse (#107/#197), **route A (Austin) unit 1**: pooled polling. Austin's Proposition 3.12 runs its polling with swaps into a *spare vertex set*, and the pooled carrier is exactly that — `originalVertex` and `poolVertex` are disjoint embeddings of the original carrier, and a `PooledRankExtension` is invariant under the **full** pooled permutation family, so the swaps need no finite-support side condition. `pollingObs` pins the conditioning **concretely** — the whole pooled rank-`n` latent array (every index of which has cardinality `< n`, hence carries no rank-`n` block) together with the structure read on the spare copy; an existential conditioning factor would make the conclusion vacuous. `PooledPollingWitness.mutualCondIndep` is `iCondIndepFun` over the **entire** rank-`n` block family — mutual, not pairwise and not one-block-against-the-rest, which is Austin's actual conclusion and what the #196 battery exists to keep honest. `iCondIndepFun_blockMap` exports the consequence to `C.P` along the canonical equivalence's **inverse** measure-preserving map: `map_restrict_embedding` pushes the pooled law forward and is not invertible, so this is not a pullback along a restriction, and that gate theorem is a compiled dependency of the export rather than a citation. Carries `[Fintype S.Srt]`, matching the polling/fixing-algebra stack; the pooled API stays countable-only. Rank zero is not handled here — it is supplied by `nonempty_rankRepresentation_one` with `truncation_zero`, which respects `stepKernel`'s deliberate lack of an `A = ∅` realization theorem
+* `Graphon.RelAustinPolling` — R4 converse (#107/#197), **route A (Austin) unit 1**: pooled polling. Austin's Proposition 3.12 polls with swaps into a *spare vertex set*, and the pooled carrier is exactly that — `PoolVertex` is `Vinfinite ⊕ Vinfinite` with `originalVertex = Sum.inl` and `poolVertex = Sum.inr`, so the halves are disjoint definitionally, and the extension's invariance under the **full** pooled permutation family means the swaps carry no finite-support side condition. **The geometry is the delicate part**: the observed blocks are confined to the original half and the poll to supports containing a spare vertex, so the two families are disjoint by construction — reading the blocks through the canonical `pooledJointEquiv` instead is tempting, since it makes the transport to `C.P` exact, but it is wrong, because that bijection sends blocks across *both* summands and they would then overlap the poll. **The seam is an enriched law, not `C.P`**: Austin's polling data is the family of *mixed* clusters straddling the two halves, and forgetting it into a bare `C.P` statement would discard what the successor construction consumes, so `enrichedPollingLaw` retains the clusters alongside the original structure and old latents, with `enrichedPollingLaw_map_fst` recovering `C.P` exactly through `map_restrict_embedding` at the original-vertex embedding. `pollingCond` pins the conditioning concretely — old latents plus clusters — since an existential factor could be the whole joint object and make the conclusion vacuous. `PooledPollingWitness.mutualCondIndep` is `iCondIndepFun` over the **entire** rank-`n` block family: mutual, not pairwise, which is Austin's actual conclusion and what the #196 battery keeps honest. Carries `[Fintype S.Srt]` to match the polling/fixing-algebra stack, leaving the pooled API countable-only; rank zero is routed to `nonempty_rankRepresentation_one` with `truncation_zero`, respecting `stepKernel`'s deliberate lack of an `A = ∅` realization theorem
 * `Graphon.RelBipartiteRegression` — R4 converse (#107/#196): the **bipartite regression** for the successor contract, a hand-built rank `1 → 2` witness over `digraphSig` whose purpose is to test that `RankSuccessor` is an expressive specification *before* either route is attempted. Each vertex carries an i.i.d. colour on its own fresh singleton coordinate and the edge is the parity, so the diagonal is constantly `false` for free. Three independent things make it a regression rather than a construction: the array law is defined **from the fresh singleton layer alone** and the rank-one coupling as the independent product `bipartiteLaw × rankLatentSource 1`, so `rankTwoCoupling_truncation` compares two separately described couplings and genuinely consumes the source factorization; the rank-two block decoder recovers **both** directed coordinates `X_uv` and `X_vu` as the same parity, exhibiting symmetry as a property of this law rather than of the signature; and `not_indepFun_rankTwoCoupling` is **numerical** — the edge and colour-parity events coincide with probability `1/2` against a product of marginals `1/4`, which a constant edge could not achieve even though it too would be "a function of the colours". `bipartiteSuccessor : RankSuccessor rankOneRep` is the witness itself
 * `Graphon.RelIidEdgeRegression` — R4 converse (#107/#196): the **i.i.d.-edge regression** for the successor contract, a hand-built rank `2 → 3` witness over `digraphSig` that tests **staging and recovery** where the bipartite regression tested independence and symmetry. The array is keyed by a coordinate's *support*, which gives symmetry (`X_uv = X_vu`) and the empty diagonal by construction — each is still proved from a support computation, but neither requires a choice of orientation. Two things make it a regression rather than a construction. First, recovery is genuinely staged: at rank three a two-point block is decoded from the latent coordinate at its own support — carried by the rank-three array because `2 < 3` — while at rank two the same blocks are not latent-measurable at all, so the two ranks exercise opposite sides of `lower_recovers`. Second, rank-two screening is a genuine conditional-independence statement: the block reads one coordinate of the edge source and the remainder reads the others plus the whole latent array, so screening follows from **independence**, not from determinism as in the bipartite case. `iidEdgeLaw_edge_eq_half` pins the edge probability at exactly `1/2`, which rules out a *constant* block; that the block is not measurable from the old latents is a separate fact, supplied by the product independence built into the rank-two coupling. The private conditional-independence lemma is stated for abstract σ-algebras rather than for the two coordinates of a product because the ambient measure is a pushforward of a product and the current API only transports conditional independence **backward**: a source-level proof would require a new forward law-transport theorem, whereas transporting the unconditional independence needs no new theorem. `iidEdgeSuccessor : RankSuccessor rankTwoRep` is the witness itself
 * `Graphon.RelRankInjectionInvariance` — R4 converse (#107), the isolated proof risk of the pooled-latent extension gate: **joint invariance under arbitrary sortwise self-injections**. `RankRepresentation.invariant` is stated for *finitely supported permutations*, but a pooled object built cheaply through `poolVertexEquiv` needs the joint law invariant under every self-injection; `RankRepresentation.map_prodMap_restrict_self` supplies exactly that, so full mixed pooled invariance later costs no additional mathematics. The route is finite-cylinder extensionality on the **joint** space, which had no machinery before — rank one's joint invariance goes through only because the rank-one latent action is trivial. `rankLatentIndexInj`/`rankLatentReindex` extend the latent action from permutations to injections (only injectivity is used — a support keeps its cardinality); `exists_finSuppPerm_agree_on_finset` matches an injection to a finitely supported permutation on any finite tagged-vertex support; `ext_of_prod_cylinders` is the joint extensionality, rectangles of coordinate cylinders on both factors. **No finiteness/`Fintype` hypothesis beyond `RankRepresentation`'s ambient countability.** Equality is tested on *coordinate* cylinders — finitely many `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
diff --git a/Graphon/RelAustinPolling.lean b/Graphon/RelAustinPolling.lean
index a403442..c69b577 100644
--- a/Graphon/RelAustinPolling.lean
+++ b/Graphon/RelAustinPolling.lean
@@ -15,50 +15,52 @@ module asserts that the two routes' outputs agree — they prove the same statem
 means and will not produce canonically equal representations.
 
 Austin's Proposition 3.12 (arXiv:0801.1698) runs its polling argument with finitely supported
-swaps into a **spare vertex set**. The pooled carrier is exactly that spare set: `originalVertex`
-and `poolVertex` are two disjoint embeddings of the original carrier into `PoolVertex`, and a
-`PooledRankExtension` is invariant under the *full* pooled permutation family, so the swaps are
-available without a finite-support or uniform-bound side condition.
-
-## What this unit fixes
-
-* `pollingObs` — the **concrete** polling observation, not an existential factor: the whole pooled
-  rank-`n` latent array together with the structure read on the spare copy. Every latent index of
-  `RankLatentIndex S n` has cardinality `< n`, so this is proper-subset data by construction and
-  carries no rank-`n` block; the spare-copy structure is the poll. Conditioning on the whole joint
-  object would make the conclusion vacuous, which is why the observation is pinned here rather
-  than quantified over.
-* `pooledBlock` — the rank-`n` block family, read through the canonical identification
-  `pooledJointEquiv`. Reading it through `originalVertex` instead would be equally meaningful but
-  would not transport *exactly*: composing two restrictions restricts along the composite
-  embedding, which is not the identity, and the export below would acquire an irreducible
-  reindexing. The spare copy still enters — through `pollingObs`, which is where the poll belongs.
-* `PooledPollingWitness` — the obligations a polling argument must discharge, with the mutual
-  conclusion as the load-bearing field.
-
-## The mutual conclusion, and why pairwise would not do
-
-The field is `iCondIndepFun` over the **entire** rank-`n` block family — mutual conditional
-independence, not pairwise and not one-block-against-the-rest. That is Austin's actual conclusion,
-and the weaker forms are genuinely weaker: the bipartite regression of #196 exhibits blocks that
-are pairwise related in ways a family-level statement rules out, which is exactly why the battery
-was built before either route was attempted.
-
-## Transport
-
-`PooledPollingWitness.iCondIndepFun_blockMap` moves the conclusion from `Q.law` to `C.P`. The
-direction matters. `map_restrict_embedding` maps the pooled law *forward* onto `C.P` and is not
-invertible, so this is **not** a pullback along a restriction; the transport runs along the
-canonical measurable equivalence `pooledJointEquiv` and its **inverse** measure-preserving map,
-whose law identity is `PooledRankExtension.map_poolVertexEquiv` — which is
-`Q.map_restrict_embedding` at the canonical embedding. The gate theorem is therefore a compiled
-proof dependency of the export, not a citation.
+swaps into a **spare vertex set**. The pooled carrier is exactly that: `PoolVertex S s` is
+`Vinfinite S s ⊕ Vinfinite S s`, with `originalVertex = Sum.inl` and `poolVertex = Sum.inr`, so the
+two halves are disjoint definitionally; and a `PooledRankExtension` is invariant under the *full*
+pooled permutation family, so the swaps carry no finite-support or uniform-bound side condition.
+
+## The geometry, and a trap it sets
+
+The observed blocks are confined to the **original** half: `originalBlock A` reads the block at
+`supportImage (originalVertex S) A`, every vertex of which is a `Sum.inl`. The poll is confined to
+supports containing at least one `Sum.inr`. The two families are therefore disjoint by
+construction, which is the whole point — a block that could itself lie in the poll would make the
+conditional independence say nothing.
+
+Reading the blocks instead through the canonical identification `pooledJointEquiv` is tempting,
+because it makes the transport to `C.P` an exact identification. It is **wrong here**:
+`poolVertexEquiv` is a bijection `PoolVertex ≃ Vinfinite`, so blocks read through it range across
+*both* summands rather than being confined to the original half, while the poll reads the spare
+half — the two would overlap.
+
+## The seam is an enriched law, not `C.P`
+
+Austin's polling data must survive into the next law; forgetting it into a bare `C.P` statement
+would discard exactly what the successor construction consumes. That data is the family of
+**mixed** clusters — pooled rank-`n` blocks straddling the two halves — and not merely the induced
+structure on the spare half.
+
+* `pollingClusters` — the mixed cluster observation, indexed by `MixedClusterIndex`: pooled
+  rank-`n` supports containing at least one spare vertex. Each such support has a *proper* original
+  part, since one of its `n` vertices is spare.
+* `enrichedPollingLaw` — the pushforward of `Q.law` retaining the original structure and old
+  latents together with the clusters.
+* `enrichedPollingLaw_map_fst` — the first marginal is `C.P` exactly, proved through
+  `Q.map_restrict_embedding (originalVertex S)`. The gate theorem is a compiled dependency here,
+  not a citation.
+
+The conditioning is pinned by `pollingCond`: the old latents together with the clusters. It is a
+definition rather than a witness field, because an existential conditioning factor could be taken
+to be the whole joint object and would make the conclusion vacuous. Every index of
+`RankLatentIndex S n` has cardinality `< n`, so the latent half of the conditioning is
+proper-subset data carrying no rank-`n` block.
 
 ## Scope
 
-* `[Fintype S.Srt]` is carried by this module, matching the polling/fixing-algebra stack it builds
-  on. The pooled API itself remains countable-only; removing the hypothesis is a separate
-  generalization and deliberately not attempted here.
+* `[Fintype S.Srt]` is carried by the witness, matching the polling/fixing-algebra stack it is to
+  be built from. The pooled API itself remains countable-only; removing the hypothesis is a
+  separate generalization and deliberately not attempted here.
 * Rank zero is not this module's business. The successor at `n = 0` is supplied by
   `nonempty_rankRepresentation_one` together with `truncation_zero`, which is also what respects
   `stepKernel`'s deliberate lack of an `A = ∅` realization theorem.
@@ -75,111 +77,129 @@ variable {S : RelSignature} [Countable S.Srt] [Countable S.Rel]
 
 attribute [local instance] RankRepresentation.isProbabilityMeasure_P
 
-/-- **The conditioning σ-algebra may be replaced by an equal one**, for a family. The `CondIndepFun`
-form is shared glue in `ForMathlib/CondIndepSup.lean`; this is its `iCondIndepFun` counterpart, kept
-private until a second consumer appears. Needed because the conditioning algebra occurs in a
-dependent position — the `≤` proof mentions it — so `rw` cannot reach it. -/
-private theorem iCondIndepFun_congr_cond {Ω : Type*} [mΩ : MeasurableSpace Ω]
-    [StandardBorelSpace Ω] {μ : Measure Ω} [IsFiniteMeasure μ]
-    {ι : Type*} {γ : ι → Type*} [∀ i, MeasurableSpace (γ i)] {Y : ∀ i, Ω → γ i}
-    {m₁ m₂ : MeasurableSpace Ω} {h1 : m₁ ≤ mΩ} (h : iCondIndepFun m₁ h1 Y μ)
-    (h12 : m₁ = m₂) (h2 : m₂ ≤ mΩ) : iCondIndepFun m₂ h2 Y μ := by
-  subst h12
-  exact h
-
-/-! ### The polling observation -/
+/-! ### Blocks on the original half -/
+
+open scoped Classical in
+/-- **The rank-`n` block family on the original half.** Every vertex of
+`supportImage (originalVertex S) A` is a `Sum.inl`, so this family is disjoint from the poll below
+by construction. -/
+noncomputable def originalBlock (A : RankSupport S n) :
+    RelStructure S (PoolVertex S) × PooledRankLatentSpace S n →
+      BlockSpaceOver (PoolVertex S) (supportImage (originalVertex S) A.1) :=
+  fun p => blockMapOver _ p.1
+
+open scoped Classical in
+theorem measurable_originalBlock (A : RankSupport S n) :
+    Measurable (originalBlock (S := S) (n := n) A) :=
+  (measurable_blockMapOver _).comp measurable_fst
+
+/-! ### The mixed clusters -/
+
+open scoped Classical in
+/-- **Mixed cluster indices**: pooled rank-`n` supports containing at least one spare vertex. The
+original part of such a support is a *proper* subset of it, since one of its `n` vertices is spare
+— this is the sense in which the clusters are indexed by proper original subsets. -/
+def MixedClusterIndex (S : RelSignature) (n : ℕ) :=
+  {A : Finset (Σ s : S.Srt, PoolVertex S s) // A.card = n ∧ ∃ v ∈ A, Sum.isRight v.2}
+
+open scoped Classical in
+instance : Countable (MixedClusterIndex S n) := Subtype.countable
+
+open scoped Classical in
+/-- The cluster observation space. -/
+abbrev ClusterSpace (S : RelSignature) (n : ℕ) :=
+  (A : MixedClusterIndex S n) → BlockSpaceOver (PoolVertex S) A.1
+
+open scoped Classical in
+/-- **The mixed cluster observation** — the poll. Each coordinate is a pooled rank-`n` block
+straddling the two halves; no coordinate is an original-half block, since every index carries a
+spare vertex. -/
+noncomputable def pollingClusters :
+    RelStructure S (PoolVertex S) × PooledRankLatentSpace S n → ClusterSpace S n :=
+  fun p A => blockMapOver A.1 p.1
+
+open scoped Classical in
+theorem measurable_pollingClusters : Measurable (pollingClusters (S := S) (n := n)) :=
+  measurable_pi_lambda _ fun A => (measurable_blockMapOver A.1).comp measurable_fst
+
+/-! ### The enriched law -/
 
 variable (S n) in
-/-- The codomain of the polling observation: the pooled rank-`n` latent array together with a
-structure on the spare copy. -/
-abbrev PollingSpace :=
-  PooledRankLatentSpace S n × RelStructure S (Vinfinite S)
+/-- The enriched observation space: the original structure and old latents, together with the
+clusters. -/
+abbrev EnrichedSpace :=
+  (RelStructure S (Vinfinite S) × RankLatentSpace S n) × ClusterSpace S n
+
+open scoped Classical in
+/-- **The enriched polling map**: restrict to the original half, and retain the poll. -/
+noncomputable def enrichedPollingMap :
+    RelStructure S (PoolVertex S) × PooledRankLatentSpace S n → EnrichedSpace S n :=
+  fun p => (Prod.map (restrictOriginal S) (restrictOriginalLatents S n) p, pollingClusters p)
+
+open scoped Classical in
+theorem measurable_enrichedPollingMap : Measurable (enrichedPollingMap (S := S) (n := n)) :=
+  (((measurable_restrict _).comp measurable_fst).prodMk
+    ((measurable_restrictOriginalLatents n).comp measurable_snd)).prodMk measurable_pollingClusters
+
+open scoped Classical in
+/-- **The enriched polling law.** Austin's polling data survives here: the clusters are retained
+alongside the original structure and old latents, rather than being forgotten into a bare `C.P`
+statement. -/
+noncomputable def enrichedPollingLaw {C : M.RankRepresentation n} (Q : PooledRankExtension C) :
+    Measure (EnrichedSpace S n) :=
+  (Q.law : Measure (RelStructure S (PoolVertex S) × PooledRankLatentSpace S n)).map
+    enrichedPollingMap
+
+open scoped Classical in
+instance {C : M.RankRepresentation n} (Q : PooledRankExtension C) :
+    IsProbabilityMeasure (enrichedPollingLaw Q) := by
+  rw [enrichedPollingLaw]
+  exact Measure.isProbabilityMeasure_map measurable_enrichedPollingMap.aemeasurable
+
+open scoped Classical in
+/-- **The enriched law refines the representation**: forgetting the clusters returns `C.P` exactly.
+Proved through `Q.map_restrict_embedding` at the **original-vertex** embedding, so the pooled gate
+theorem is a compiled dependency of everything downstream. -/
+theorem enrichedPollingLaw_map_fst {C : M.RankRepresentation n} (Q : PooledRankExtension C) :
+    (enrichedPollingLaw Q).map Prod.fst = C.P := by
+  rw [enrichedPollingLaw, Measure.map_map measurable_fst measurable_enrichedPollingMap,
+    show (Prod.fst ∘ enrichedPollingMap (S := S) (n := n)) =
+      Prod.map (RelStructure.restrict (originalVertex S))
+        (latentRestrictOver (fun s => originalVertex S s) n) from rfl]
+  exact Q.map_restrict_embedding (originalVertex S)
+
+/-! ### The conditioning -/
 
 variable (S n) in
-/-- **The polling observation.** The whole pooled rank-`n` latent array — every index of which has
-cardinality `< n`, hence is proper-subset data carrying no rank-`n` block — together with the
-structure read on the **spare** copy of the carrier, which is the poll. Pinned concretely: an
-arbitrary conditioning factor would make the mutual conclusion vacuous. -/
-noncomputable def pollingObs :
-    RelStructure S (PoolVertex S) × PooledRankLatentSpace S n → PollingSpace S n :=
-  fun p => (p.2, RelStructure.restrict (poolVertex S) p.1)
+/-- **The polling conditioning**, pinned concretely: the old latents together with the mixed
+clusters. Not a witness field — an existential factor could be taken to be the whole joint object,
+which would make the mutual conclusion vacuous. -/
+noncomputable def pollingCond :
+    EnrichedSpace S n → RankLatentSpace S n × ClusterSpace S n :=
+  fun q => (q.1.2, q.2)
 
 variable (S n) in
-theorem measurable_pollingObs : Measurable (pollingObs S n) :=
-  measurable_snd.prodMk ((measurable_restrict _).comp measurable_fst)
-
-/-! ### The rank-`n` block family -/
-
-/-- **The rank-`n` block family on the pooled space**, read through the canonical identification.
-Indexed by the original rank-`n` supports, with a fixed codomain per index, which is what lets the
-export below be an exact identification rather than a reindexing. -/
-noncomputable def pooledBlock (A : RankSupport S n) :
-    RelStructure S (PoolVertex S) × PooledRankLatentSpace S n → BlockSpace (S := S) A.1 :=
-  fun p => blockMap A.1 (pooledJointEquiv S n p).1
-
-theorem measurable_pooledBlock (A : RankSupport S n) : Measurable (pooledBlock (S := S) (n := n) A) :=
-  (measurable_blockMap A.1).comp ((pooledJointEquiv S n).measurable.fst)
-
-omit [Countable S.Srt] [Countable S.Rel] in
-/-- Composing the pooled block family with the inverse identification returns the block of the
-original structure, on the nose. -/
-theorem pooledBlock_comp_symm (A : RankSupport S n) :
-    pooledBlock (S := S) (n := n) A ∘ (pooledJointEquiv S n).symm =
-      blockMap A.1 ∘ Prod.fst := by
-  funext p
-  show blockMap A.1 (pooledJointEquiv S n ((pooledJointEquiv S n).symm p)).1 = _
-  rw [MeasurableEquiv.apply_symm_apply]
-  rfl
+theorem measurable_pollingCond : Measurable (pollingCond S n) :=
+  (measurable_fst.snd).prodMk measurable_snd
 
 /-! ### The witness -/
 
 variable [Fintype S.Srt]
 
-/-- **What a polling argument must supply.** The mutual conditional independence of the *entire*
-rank-`n` block family given the polling observation — Austin's Proposition 3.12 conclusion in this
-setting. The observation is not a field: it is pinned by `pollingObs`, so that a witness cannot
-discharge the obligation by conditioning on more than proper-subset and spare-pool data. -/
+/-- **What the polling argument must supply**: mutual conditional independence of the *entire*
+rank-`n` block family of the original structure, given the old latents and the mixed clusters,
+under the enriched law.
+
+`iCondIndepFun` over the whole family is Austin's Proposition 3.12 conclusion. Pairwise
+independence, or one block against the rest, would be strictly weaker, and the adversarial battery
+of #196 exists to keep that distinction honest. -/
 structure PooledPollingWitness (C : M.RankRepresentation n) (Q : PooledRankExtension C) where
-  /-- **Mutual** conditional independence of the whole rank-`n` block family, given the polling
-  observation. Pairwise independence, or one block against the rest, would not suffice. -/
+  /-- **Mutual** conditional independence of the whole rank-`n` block family. -/
   mutualCondIndep :
-    iCondIndepFun (MeasurableSpace.comap (pollingObs S n) inferInstance)
-      (measurable_pollingObs S n).comap_le
-      (fun A : RankSupport S n => pooledBlock (S := S) (n := n) A)
-      (Q.law : Measure (RelStructure S (PoolVertex S) × PooledRankLatentSpace S n))
-
-namespace PooledPollingWitness
-
-variable {C : M.RankRepresentation n} {Q : PooledRankExtension C}
-
-/-- **The exact consequence under `C.P`.** The rank-`n` blocks of the representation are mutually
-conditionally independent given the polling observation transported to the original carrier.
-
-The transport is along the canonical equivalence's **inverse** measure-preserving map, not along
-the non-invertible restriction: `map_restrict_embedding` pushes the pooled law forward onto `C.P`,
-and it is exactly that identity — through `map_poolVertexEquiv` and
-`measurePreserving_pooledJointEquiv` — which makes the inverse measure preserving. The gate
-theorem is a compiled dependency of this proof. -/
-theorem iCondIndepFun_blockMap (W : PooledPollingWitness C Q) :
-    iCondIndepFun
-      (MeasurableSpace.comap (pollingObs S n ∘ (pooledJointEquiv S n).symm) inferInstance)
-      ((measurable_pollingObs S n).comp (pooledJointEquiv S n).symm.measurable).comap_le
-      (fun A : RankSupport S n => blockMap A.1 ∘ Prod.fst) C.P := by
-  haveI := C.isProbabilityMeasure_P
-  have hsymm : MeasurePreserving ((pooledJointEquiv S n).symm) C.P
-      (Q.law : Measure (RelStructure S (PoolVertex S) × PooledRankLatentSpace S n)) :=
-    MeasurePreserving.symm _ Q.measurePreserving_pooledJointEquiv
-  have h := iCondIndepFun_comp_measurePreserving hsymm
-    (measurable_pollingObs S n).comap_le
-    (fun A : RankSupport S n => measurable_pooledBlock A) W.mutualCondIndep
-  have hfam : (fun A : RankSupport S n =>
-        pooledBlock (S := S) (n := n) A ∘ (pooledJointEquiv S n).symm) =
-      fun A : RankSupport S n => blockMap A.1 ∘ Prod.fst :=
-    funext fun A => pooledBlock_comp_symm A
-  rw [hfam] at h
-  exact iCondIndepFun_congr_cond h MeasurableSpace.comap_comp _
-
-end PooledPollingWitness
+    iCondIndepFun (MeasurableSpace.comap (pollingCond S n) inferInstance)
+      (measurable_pollingCond S n).comap_le
+      (fun A : RankSupport S n => blockMap A.1 ∘ Prod.fst ∘ Prod.fst)
+      (enrichedPollingLaw Q)
 
 end InfiniteRelExchangeableLaw
 
diff --git a/scripts/axiom_audit.lean b/scripts/axiom_audit.lean
index cb435b0..a144f76 100644
--- a/scripts/axiom_audit.lean
+++ b/scripts/axiom_audit.lean
@@ -348,9 +348,9 @@ custom axioms. Target list and policy: `scripts/check_census_and_axioms.py`
 #print axioms RelSignature.BipartiteRegression.not_indepFun_rankTwoCoupling
 
 -- R4 converse route A (#197): pooled polling, unit 1.
-#print axioms RelSignature.InfiniteRelExchangeableLaw.pollingObs
-#print axioms RelSignature.InfiniteRelExchangeableLaw.pooledBlock
-#print axioms RelSignature.InfiniteRelExchangeableLaw.PooledPollingWitness.iCondIndepFun_blockMap
+#print axioms RelSignature.InfiniteRelExchangeableLaw.pollingClusters
+#print axioms RelSignature.InfiniteRelExchangeableLaw.enrichedPollingLaw
+#print axioms RelSignature.InfiniteRelExchangeableLaw.enrichedPollingLaw_map_fst
 
 -- Shared digraph-coordinate support geometry (two regression consumers).
 #print axioms support_digraphCoord
diff --git a/scripts/check_census_and_axioms.py b/scripts/check_census_and_axioms.py
index ab1f650..06b66a9 100644
--- a/scripts/check_census_and_axioms.py
+++ b/scripts/check_census_and_axioms.py
@@ -307,9 +307,9 @@
     "RelSignature.BipartiteRegression.bipartiteSuccessor",
     "RelSignature.BipartiteRegression.ae_edge_xor",
     "RelSignature.BipartiteRegression.not_indepFun_rankTwoCoupling",
-    "RelSignature.InfiniteRelExchangeableLaw.pollingObs",
-    "RelSignature.InfiniteRelExchangeableLaw.pooledBlock",
-    "RelSignature.InfiniteRelExchangeableLaw.PooledPollingWitness.iCondIndepFun_blockMap",
+    "RelSignature.InfiniteRelExchangeableLaw.pollingClusters",
+    "RelSignature.InfiniteRelExchangeableLaw.enrichedPollingLaw",
+    "RelSignature.InfiniteRelExchangeableLaw.enrichedPollingLaw_map_fst",
     "support_digraphCoord",
     "card_support_digraphCoord",
     "RelSignature.mem_rankSupportPerm",

From 8be53f0fb2f4b0d3b94f5c2504b24f81ddde6ed3 Mon Sep 17 00:00:00 2001
From: Cameron Freer <cameronfreer@gmail.com>
Date: Sun, 23 Aug 2026 17:40:46 +0000
Subject: [PATCH 03/13] docs: correct the sense of "mixed" in the cluster index
 (#197)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

`MixedClusterIndex` means **not wholly original**, not literally straddling both
halves: an all-spare support qualifies, its original part being empty and therefore
proper. The prose claimed the stronger reading in four places, which would have
suggested the all-spare clusters are excluded when the definition includes them —
and they are exactly the clusters carrying no original data at all.

No statement or proof changes.
---
 Graphon/RelAustinPolling.lean | 25 +++++++++++++++----------
 1 file changed, 15 insertions(+), 10 deletions(-)

diff --git a/Graphon/RelAustinPolling.lean b/Graphon/RelAustinPolling.lean
index c69b577..a5bd2a8 100644
--- a/Graphon/RelAustinPolling.lean
+++ b/Graphon/RelAustinPolling.lean
@@ -38,12 +38,14 @@ half — the two would overlap.
 
 Austin's polling data must survive into the next law; forgetting it into a bare `C.P` statement
 would discard exactly what the successor construction consumes. That data is the family of
-**mixed** clusters — pooled rank-`n` blocks straddling the two halves — and not merely the induced
-structure on the spare half.
+**mixed** clusters — pooled rank-`n` blocks that are *not wholly original* — and not merely the
+induced structure on the spare half. "Mixed" is exactly that negation: an all-spare support
+qualifies, its original part being empty and therefore proper.
 
 * `pollingClusters` — the mixed cluster observation, indexed by `MixedClusterIndex`: pooled
-  rank-`n` supports containing at least one spare vertex. Each such support has a *proper* original
-  part, since one of its `n` vertices is spare.
+  rank-`n` supports containing at least one spare vertex, all-spare supports included. Each such
+  support has a *proper* original part, since at least one of its `n` vertices is spare; for an
+  all-spare support that part is empty, which is proper as well.
 * `enrichedPollingLaw` — the pushforward of `Q.law` retaining the original structure and old
   latents together with the clusters.
 * `enrichedPollingLaw_map_fst` — the first marginal is `C.P` exactly, proved through
@@ -96,9 +98,12 @@ theorem measurable_originalBlock (A : RankSupport S n) :
 /-! ### The mixed clusters -/
 
 open scoped Classical in
-/-- **Mixed cluster indices**: pooled rank-`n` supports containing at least one spare vertex. The
-original part of such a support is a *proper* subset of it, since one of its `n` vertices is spare
-— this is the sense in which the clusters are indexed by proper original subsets. -/
+/-- **Mixed cluster indices**: pooled rank-`n` supports that are **not wholly original**, i.e.
+containing at least one spare vertex. All-spare supports are included — "mixed" is the negation of
+"wholly original", not a demand that both halves be met. The original part of such a support is a
+*proper* subset of it, since at least one of its `n` vertices is spare, and for an all-spare
+support that part is empty; this is the sense in which the clusters are indexed by proper original
+subsets. -/
 def MixedClusterIndex (S : RelSignature) (n : ℕ) :=
   {A : Finset (Σ s : S.Srt, PoolVertex S s) // A.card = n ∧ ∃ v ∈ A, Sum.isRight v.2}
 
@@ -111,9 +116,9 @@ abbrev ClusterSpace (S : RelSignature) (n : ℕ) :=
   (A : MixedClusterIndex S n) → BlockSpaceOver (PoolVertex S) A.1
 
 open scoped Classical in
-/-- **The mixed cluster observation** — the poll. Each coordinate is a pooled rank-`n` block
-straddling the two halves; no coordinate is an original-half block, since every index carries a
-spare vertex. -/
+/-- **The mixed cluster observation** — the poll. Each coordinate is a pooled rank-`n` block that
+is not wholly original; no coordinate is an original-half block, since every index carries a spare
+vertex. -/
 noncomputable def pollingClusters :
     RelStructure S (PoolVertex S) × PooledRankLatentSpace S n → ClusterSpace S n :=
   fun p A => blockMapOver A.1 p.1

From 356f17144d822f17fa51b6bc7bdb56280d3d6ebe Mon Sep 17 00:00:00 2001
From: Cameron Freer <cameronfreer@gmail.com>
Date: Sun, 23 Aug 2026 21:43:00 +0000
Subject: [PATCH 04/13] feat: carry the full pooled latent array as auxiliary
 polling data (#197)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

The peel permutations move original vertices into the spare half, which sends an
original latent index to a mixed one. The **original** latent array is therefore not
stable under those permutations, and any conditioning built from it cannot satisfy
the exact `comap ρ m₁ = m₂` identity the tail engine needs. The **pooled** array is
stable — such a permutation merely permutes pooled indices among themselves.

The pooled array is carried *alongside* the original marginal rather than replacing
it, so the first component of `enrichedPollingMap` is untouched and
`enrichedPollingLaw_map_fst` is literally unchanged. Every pooled index still has
cardinality `< n`, so the widened conditioning reveals no rank-`n` block and nothing
becomes vacuous.

Gates: lake build clean, census + axiom audit pass, zero sorries.
---
 Graphon/RelAustinPolling.lean | 35 ++++++++++++++++++++++++-----------
 1 file changed, 24 insertions(+), 11 deletions(-)

diff --git a/Graphon/RelAustinPolling.lean b/Graphon/RelAustinPolling.lean
index a5bd2a8..194af0d 100644
--- a/Graphon/RelAustinPolling.lean
+++ b/Graphon/RelAustinPolling.lean
@@ -131,20 +131,29 @@ theorem measurable_pollingClusters : Measurable (pollingClusters (S := S) (n :=
 
 variable (S n) in
 /-- The enriched observation space: the original structure and old latents, together with the
-clusters. -/
+**auxiliary** polling data — the whole pooled rank-`n` latent array and the clusters.
+
+The pooled latent array is carried *alongside* the original marginal rather than replacing it, so
+the first component is untouched and `enrichedPollingLaw_map_fst` stays literally what it was. It
+is needed because the peel permutations move original vertices into the spare half: an original
+latent index is then sent to a mixed one, so the original latent array is **not** stable under
+those permutations, while the pooled array is — they merely permute pooled indices among
+themselves. Every pooled index still has cardinality `< n`, so no rank-`n` block is revealed. -/
 abbrev EnrichedSpace :=
-  (RelStructure S (Vinfinite S) × RankLatentSpace S n) × ClusterSpace S n
+  (RelStructure S (Vinfinite S) × RankLatentSpace S n) ×
+    (PooledRankLatentSpace S n × ClusterSpace S n)
 
 open scoped Classical in
 /-- **The enriched polling map**: restrict to the original half, and retain the poll. -/
 noncomputable def enrichedPollingMap :
     RelStructure S (PoolVertex S) × PooledRankLatentSpace S n → EnrichedSpace S n :=
-  fun p => (Prod.map (restrictOriginal S) (restrictOriginalLatents S n) p, pollingClusters p)
+  fun p => (Prod.map (restrictOriginal S) (restrictOriginalLatents S n) p, (p.2, pollingClusters p))
 
 open scoped Classical in
 theorem measurable_enrichedPollingMap : Measurable (enrichedPollingMap (S := S) (n := n)) :=
   (((measurable_restrict _).comp measurable_fst).prodMk
-    ((measurable_restrictOriginalLatents n).comp measurable_snd)).prodMk measurable_pollingClusters
+    ((measurable_restrictOriginalLatents n).comp measurable_snd)).prodMk
+      (measurable_snd.prodMk measurable_pollingClusters)
 
 open scoped Classical in
 /-- **The enriched polling law.** Austin's polling data survives here: the clusters are retained
@@ -176,16 +185,20 @@ theorem enrichedPollingLaw_map_fst {C : M.RankRepresentation n} (Q : PooledRankE
 /-! ### The conditioning -/
 
 variable (S n) in
-/-- **The polling conditioning**, pinned concretely: the old latents together with the mixed
-clusters. Not a witness field — an existential factor could be taken to be the whole joint object,
-which would make the mutual conclusion vacuous. -/
+/-- **The polling conditioning**, pinned concretely: the whole pooled rank-`n` latent array
+together with the mixed clusters — that is, the auxiliary component. Not a witness field: an
+existential factor could be taken to be the whole joint object and would make the conclusion
+vacuous.
+
+Reading the *pooled* array rather than its original part is what makes the conditioning stable
+under the permutations the peel uses; every index still has cardinality `< n`, so the latent half
+carries no rank-`n` block. -/
 noncomputable def pollingCond :
-    EnrichedSpace S n → RankLatentSpace S n × ClusterSpace S n :=
-  fun q => (q.1.2, q.2)
+    EnrichedSpace S n → PooledRankLatentSpace S n × ClusterSpace S n :=
+  fun q => q.2
 
 variable (S n) in
-theorem measurable_pollingCond : Measurable (pollingCond S n) :=
-  (measurable_fst.snd).prodMk measurable_snd
+theorem measurable_pollingCond : Measurable (pollingCond S n) := measurable_snd
 
 /-! ### The witness -/
 

From 4b86c1f014421dfff450fb89db388b7305d29906 Mon Sep 17 00:00:00 2001
From: Cameron Freer <cameronfreer@gmail.com>
Date: Sun, 23 Aug 2026 21:56:26 +0000
Subject: [PATCH 05/13] feat: weak union for conditional independence (#197,
 acceptance step 1)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

The graphoid axiom this route turns on, and which neither Mathlib nor this
repository had: **if X ⊥ (Y, Z) | W and W ≤ Z, then X ⊥ Y | Z.** The containment
W ≤ Z is a hypothesis rather than a conclusion shape, so the result conditions on
exactly Z and not on an unsimplified W ⊔ Z — which is what lets the peel keep one
fixed conditioning algebra across every stage.

This is what makes the tail engine unnecessary at the inductive stage.
`Q.screening` already holds at every pooled rank-n support, and its remainder is
(all other rank-≤n blocks, the whole pooled latent array) — which contains the
accumulated blocks, the clusters, and the latents. Weak union converts that
directly into the one-block statement, with the local conditioning absorbed
because it is measurable from the pooled-latent component.

Proof: enlarging the conditioning from W to any algebra between W and Y ⊔ Z leaves
the conditional probability of an X-event unchanged, by conditional-expectation
uniqueness with the product identity supplying the set integrals. Applying that at
Y ⊔ Z and at Z and peeling with the tower property gives the result.

Private, one consumer; it moves to ForMathlib when #198 needs it.

Two Lean notes worth keeping: abstract `MeasurableSpace Ω` binders shadow the
ambient instance, so ambient measurability is annotated `MeasurableSet[mΩ]` and the
cross-call instance is passed by name; and `f * S.indicator 1` is better handled as
`S.indicator f`, which makes integrability immediate instead of a bounded-mul
argument in the wrong factor order.

Gates: lake build clean (3409 jobs), census + axiom audit pass, zero sorries, no
warnings.
---
 Graphon/RelAustinPolling.lean | 98 +++++++++++++++++++++++++++++++++++
 1 file changed, 98 insertions(+)

diff --git a/Graphon/RelAustinPolling.lean b/Graphon/RelAustinPolling.lean
index 194af0d..deb2fe2 100644
--- a/Graphon/RelAustinPolling.lean
+++ b/Graphon/RelAustinPolling.lean
@@ -79,6 +79,102 @@ variable {S : RelSignature} [Countable S.Srt] [Countable S.Rel]
 
 attribute [local instance] RankRepresentation.isProbabilityMeasure_P
 
+/-! ### Weak union for conditional independence
+
+The graphoid axiom this development turns on, and which neither Mathlib nor this repository has:
+**if `X` is conditionally independent of `(Y, Z)` given `W`, and `W` is contained in `Z`, then `X`
+is conditionally independent of `Y` given `Z` alone.** The containment `W ≤ Z` is what lets the
+conclusion condition on exactly `Z` rather than on an unsimplified `W ⊔ Z`.
+
+Kept **private**: one consumer. When #198 needs the same axiom it should move to `ForMathlib/`.
+
+The proof is the standard one. The key step is that enlarging the conditioning from `W` to any
+algebra between `W` and `Y ⊔ Z` does not change the conditional probability of an `X`-event —
+proved by conditional-expectation uniqueness, with the product identity supplying the set
+integrals. Applying that at `Y ⊔ Z` and at `Z`, and then peeling with the tower property, gives the
+result. -/
+
+private theorem condExp_eq_of_between {Ω : Type*} [mΩ : MeasurableSpace Ω]
+    {μ : Measure Ω} [IsFiniteMeasure μ] {mW mX mYZ m : MeasurableSpace Ω}
+    (hW : mW ≤ mΩ) (hm : m ≤ mΩ) (hWm : mW ≤ m) (hmYZ : m ≤ mYZ)
+    {A : Set Ω} (hAX : MeasurableSet[mX] A) (hA : MeasurableSet[mΩ] A)
+    (h : ∀ t1 t2, MeasurableSet[mX] t1 → MeasurableSet[mYZ] t2 →
+      (μ⟦t1 ∩ t2 | mW⟧) =ᵐ[μ] (μ⟦t1 | mW⟧) * (μ⟦t2 | mW⟧)) :
+    (μ⟦A | m⟧) =ᵐ[μ] (μ⟦A | mW⟧) := by
+  refine (ae_eq_condExp_of_forall_setIntegral_eq hm
+    ((integrable_const (1 : ℝ)).indicator hA)
+    (fun S _ _ => integrable_condExp.integrableOn)
+    (fun S hSm _ => ?_)
+    ((stronglyMeasurable_condExp.mono hWm).aestronglyMeasurable)).symm
+  have hSamb : MeasurableSet[mΩ] S := hm _ hSm
+  have hprod := h A S hAX (hmYZ _ hSm)
+  -- the pull-out identity, integrated
+  have hmulind : (μ⟦A | mW⟧) * S.indicator (fun _ => (1 : ℝ)) = S.indicator (μ⟦A | mW⟧) := by
+    funext x
+    by_cases hx : x ∈ S <;> simp [hx, Set.indicator_of_mem, Set.indicator_of_notMem]
+  have hpull : μ[(μ⟦A | mW⟧) * S.indicator (fun _ => (1 : ℝ)) | mW]
+      =ᵐ[μ] (μ⟦A | mW⟧) * (μ⟦S | mW⟧) :=
+    condExp_mul_of_stronglyMeasurable_left stronglyMeasurable_condExp
+      (by rw [hmulind]; exact integrable_condExp.indicator hSamb)
+      ((integrable_const (1 : ℝ)).indicator hSamb)
+  calc ∫ x in S, (μ⟦A | mW⟧) x ∂μ
+      = ∫ x, ((μ⟦A | mW⟧) * S.indicator fun _ => (1 : ℝ)) x ∂μ := by
+        rw [← integral_indicator hSamb]
+        refine integral_congr_ae (Filter.Eventually.of_forall fun x => ?_)
+        by_cases hx : x ∈ S <;> simp [hx, Set.indicator_of_mem, Set.indicator_of_notMem]
+    _ = ∫ x, (μ[(μ⟦A | mW⟧) * S.indicator fun _ => (1 : ℝ) | mW]) x ∂μ :=
+        (integral_condExp hW).symm
+    _ = ∫ x, ((μ⟦A | mW⟧) * (μ⟦S | mW⟧)) x ∂μ := integral_congr_ae hpull
+    _ = ∫ x, (μ⟦A ∩ S | mW⟧) x ∂μ := (integral_congr_ae hprod).symm
+    _ = ∫ x, (A ∩ S).indicator (fun _ => (1 : ℝ)) x ∂μ := integral_condExp hW
+    _ = ∫ x in S, A.indicator (fun _ => (1 : ℝ)) x ∂μ := by
+        rw [integral_indicator (hA.inter hSamb), setIntegral_indicator hA, Set.inter_comm]
+
+private theorem condIndep_weak_union {Ω : Type*} [mΩ : MeasurableSpace Ω] [StandardBorelSpace Ω]
+    {μ : Measure Ω} [IsFiniteMeasure μ] {mW mX mY mZ : MeasurableSpace Ω}
+    (hW : mW ≤ mΩ) (hX : mX ≤ mΩ) (hY : mY ≤ mΩ) (hZ : mZ ≤ mΩ) (hWZ : mW ≤ mZ)
+    (h : CondIndep mW mX (mY ⊔ mZ) hW μ) :
+    CondIndep mZ mX mY hZ μ := by
+  have hYZ : mY ⊔ mZ ≤ mΩ := sup_le hY hZ
+  rw [condIndep_iff _ _ _ hW hX hYZ] at h
+  rw [condIndep_iff _ _ _ hZ hX hY]
+  intro A B hA hB
+  have hAamb : MeasurableSet[mΩ] A := hX _ hA
+  have hBamb : MeasurableSet[mΩ] B := hY _ hB
+  have hBYZ : MeasurableSet[mY ⊔ mZ] B := (le_sup_left : mY ≤ mY ⊔ mZ) _ hB
+  -- the conditional probability of an `X`-event is the same at `W`, at `Z`, and at `Y ⊔ Z`
+  have hZeq : (μ⟦A | mZ⟧) =ᵐ[μ] (μ⟦A | mW⟧) :=
+    condExp_eq_of_between (mΩ := mΩ) hW hZ hWZ le_sup_right hA hAamb h
+  have hYZeq : (μ⟦A | mY ⊔ mZ⟧) =ᵐ[μ] (μ⟦A | mW⟧) :=
+    condExp_eq_of_between (mΩ := mΩ) hW hYZ (hWZ.trans le_sup_right) le_rfl hA hAamb h
+  -- peel `B` off inside the larger algebra, then descend by the tower property
+  have hpull : μ[(A ∩ B).indicator (fun _ => (1 : ℝ)) | mY ⊔ mZ]
+      =ᵐ[μ] (μ⟦A | mW⟧) * B.indicator fun _ => (1 : ℝ) := by
+    have hmul : ((A ∩ B).indicator fun _ => (1 : ℝ)) =
+        (A.indicator fun _ => (1 : ℝ)) * B.indicator fun _ => (1 : ℝ) := by
+      funext x
+      by_cases hx : x ∈ A <;> by_cases hy : x ∈ B <;>
+        simp [hx, hy, Set.indicator_of_mem, Set.indicator_of_notMem, Set.mem_inter_iff]
+    rw [hmul]
+    refine (condExp_mul_of_stronglyMeasurable_right
+      (stronglyMeasurable_const.indicator hBYZ)
+      ?_ ((integrable_const (1 : ℝ)).indicator hAamb)).trans ?_
+    · rw [← hmul]; exact (integrable_const (1 : ℝ)).indicator (hAamb.inter hBamb)
+    · exact Filter.EventuallyEq.mul hYZeq Filter.EventuallyEq.rfl
+  have htower : (μ⟦A ∩ B | mZ⟧) =ᵐ[μ] μ[μ[(A ∩ B).indicator (fun _ => (1 : ℝ)) | mY ⊔ mZ] | mZ] :=
+    (condExp_condExp_of_le le_sup_right hYZ).symm
+  refine htower.trans ?_
+  refine ((condExp_congr_ae hpull).trans ?_)
+  refine (condExp_mul_of_stronglyMeasurable_left
+    (stronglyMeasurable_condExp.mono hWZ)
+    ?_ ((integrable_const (1 : ℝ)).indicator hBamb)).trans ?_
+  · have hmulB : (μ⟦A | mW⟧) * B.indicator (fun _ => (1 : ℝ)) = B.indicator (μ⟦A | mW⟧) := by
+      funext x
+      by_cases hx : x ∈ B <;> simp [hx, Set.indicator_of_mem, Set.indicator_of_notMem]
+    rw [hmulB]
+    exact integrable_condExp.indicator hBamb
+  · exact (Filter.EventuallyEq.mul hZeq.symm Filter.EventuallyEq.rfl)
+
 /-! ### Blocks on the original half -/
 
 open scoped Classical in
@@ -91,6 +187,7 @@ noncomputable def originalBlock (A : RankSupport S n) :
   fun p => blockMapOver _ p.1
 
 open scoped Classical in
+omit [Countable S.Srt] in
 theorem measurable_originalBlock (A : RankSupport S n) :
     Measurable (originalBlock (S := S) (n := n) A) :=
   (measurable_blockMapOver _).comp measurable_fst
@@ -124,6 +221,7 @@ noncomputable def pollingClusters :
   fun p A => blockMapOver A.1 p.1
 
 open scoped Classical in
+omit [Countable S.Srt] in
 theorem measurable_pollingClusters : Measurable (pollingClusters (S := S) (n := n)) :=
   measurable_pi_lambda _ fun A => (measurable_blockMapOver A.1).comp measurable_fst
 

From 542c5239ca946e32f712f8871bd2f6e2a75db0f2 Mon Sep 17 00:00:00 2001
From: Cameron Freer <cameronfreer@gmail.com>
Date: Mon, 24 Aug 2026 03:53:24 +0000
Subject: [PATCH 06/13] =?UTF-8?q?feat:=20source-level=20polling=20conditio?=
 =?UTF-8?q?ning=20and=20the=20W=20=E2=89=A4=20Z=20check=20(#197,=20accepta?=
 =?UTF-8?q?nce=20step=202a)?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Three pieces, all about the *conditioning factor* rather than about what the
screening remainder supplies — deliberately committed before that more intricate
argument, so the two are separable if either needs rework.

* `sourcePollingCond` reads the polling conditioning directly on the pooled space,
  where steps 1–4 of the construction run.
* `pollingCond ∘ enrichedPollingMap = sourcePollingCond` holds by `rfl`: the
  source-level and enriched-level statements are the same observation, so relating
  them needs no transport.
* `comap_localLatents_le_sourcePollingCond` discharges weak union's `W ≤ Z`
  hypothesis concretely — the local conditioning at any pooled support is a
  coordinate projection of the pooled latent component, not an assumption.

Prose: the promotion note is now the standing rule (private at one consumer,
extracted after a second independent one) with no forward reference; and the
latent-widening justification rests on the durable reason — `Q.screening`'s
remainder contains the entire pooled latent array and weak union conditions on
exactly that lower-rank factor — rather than on peel-permutation stability, which
was true but is no longer the operative reason now that the tail engine is out of
the inductive stage.

Gates: lake build clean (3409 jobs), census + axiom audit pass, zero sorries, no
warnings.
---
 Graphon/RelAustinPolling.lean | 56 +++++++++++++++++++++++++++++++----
 1 file changed, 50 insertions(+), 6 deletions(-)

diff --git a/Graphon/RelAustinPolling.lean b/Graphon/RelAustinPolling.lean
index deb2fe2..e11a87b 100644
--- a/Graphon/RelAustinPolling.lean
+++ b/Graphon/RelAustinPolling.lean
@@ -86,7 +86,8 @@ The graphoid axiom this development turns on, and which neither Mathlib nor this
 is conditionally independent of `Y` given `Z` alone.** The containment `W ≤ Z` is what lets the
 conclusion condition on exactly `Z` rather than on an unsimplified `W ⊔ Z`.
 
-Kept **private**: one consumer. When #198 needs the same axiom it should move to `ForMathlib/`.
+Kept **private** under the standing promotion rule: private at one consumer, extracted to
+`ForMathlib/` once a second independent consumer exists.
 
 The proof is the standard one. The key step is that enlarging the conditioning from `W` to any
 algebra between `W` and `Y ⊔ Z` does not change the conditional probability of an `X`-event —
@@ -232,11 +233,9 @@ variable (S n) in
 **auxiliary** polling data — the whole pooled rank-`n` latent array and the clusters.
 
 The pooled latent array is carried *alongside* the original marginal rather than replacing it, so
-the first component is untouched and `enrichedPollingLaw_map_fst` stays literally what it was. It
-is needed because the peel permutations move original vertices into the spare half: an original
-latent index is then sent to a mixed one, so the original latent array is **not** stable under
-those permutations, while the pooled array is — they merely permute pooled indices among
-themselves. Every pooled index still has cardinality `< n`, so no rank-`n` block is revealed. -/
+the first component is untouched and `enrichedPollingLaw_map_fst` stays literally what it was. The pooled array is the right lower-rank factor because `Q.screening`'s remainder
+`restObservationOver n A` already contains it in full, and weak union conditions on exactly that
+factor. Every pooled index has cardinality `< n`, so no rank-`n` block is revealed. -/
 abbrev EnrichedSpace :=
   (RelStructure S (Vinfinite S) × RankLatentSpace S n) ×
     (PooledRankLatentSpace S n × ClusterSpace S n)
@@ -248,6 +247,7 @@ noncomputable def enrichedPollingMap :
   fun p => (Prod.map (restrictOriginal S) (restrictOriginalLatents S n) p, (p.2, pollingClusters p))
 
 open scoped Classical in
+omit [Countable S.Srt] in
 theorem measurable_enrichedPollingMap : Measurable (enrichedPollingMap (S := S) (n := n)) :=
   (((measurable_restrict _).comp measurable_fst).prodMk
     ((measurable_restrictOriginalLatents n).comp measurable_snd)).prodMk
@@ -296,8 +296,52 @@ noncomputable def pollingCond :
   fun q => q.2
 
 variable (S n) in
+omit [Countable S.Srt] [Countable S.Rel] in
 theorem measurable_pollingCond : Measurable (pollingCond S n) := measurable_snd
 
+/-! ### The source-level conditioning
+
+Steps 1–4 of the construction run under `Q.law`, on the pooled space, and only the final descent
+moves to the enriched law. `sourcePollingCond` is the conditioning read there, and it is the
+*same* observation: `pollingCond ∘ enrichedPollingMap` is definitionally `sourcePollingCond`, so
+no transport is needed to relate the two statements. -/
+
+open scoped Classical in
+/-- The polling conditioning read directly on the pooled space. -/
+noncomputable def sourcePollingCond :
+    RelStructure S (PoolVertex S) × PooledRankLatentSpace S n →
+      PooledRankLatentSpace S n × ClusterSpace S n :=
+  fun p => (p.2, pollingClusters p)
+
+open scoped Classical in
+omit [Countable S.Srt] in
+theorem measurable_sourcePollingCond : Measurable (sourcePollingCond (S := S) (n := n)) :=
+  measurable_snd.prodMk measurable_pollingClusters
+
+open scoped Classical in
+omit [Countable S.Srt] [Countable S.Rel] in
+/-- **The two conditionings agree**, definitionally: conditioning on the enriched law and
+conditioning on the pooled law are the same observation composed with the enriching map. -/
+theorem pollingCond_comp_enrichedPollingMap :
+    pollingCond S n ∘ enrichedPollingMap = sourcePollingCond (S := S) (n := n) := rfl
+
+open scoped Classical in
+omit [Countable S.Srt] [Countable S.Rel] in
+/-- **Check 1**: the local conditioning at any pooled support is measurable from the source polling
+conditioning — it is a coordinate projection of the pooled latent component. This is the `W ≤ Z`
+hypothesis of weak union, discharged concretely rather than assumed. -/
+theorem comap_localLatents_le_sourcePollingCond (A : Finset (Σ s : S.Srt, PoolVertex S s)) :
+    MeasurableSpace.comap
+        (localLatentsOver A n ∘ (Prod.snd :
+          RelStructure S (PoolVertex S) × PooledRankLatentSpace S n → _)) inferInstance ≤
+      MeasurableSpace.comap (sourcePollingCond (S := S) (n := n)) inferInstance := by
+  rw [show (localLatentsOver A n ∘ (Prod.snd :
+        RelStructure S (PoolVertex S) × PooledRankLatentSpace S n → _)) =
+      (localLatentsOver A n ∘ Prod.fst) ∘ sourcePollingCond from rfl,
+    ← MeasurableSpace.comap_comp]
+  exact MeasurableSpace.comap_mono
+    ((measurable_localLatentsOver A n).comp measurable_fst).comap_le
+
 /-! ### The witness -/
 
 variable [Fintype S.Srt]

From 1a3e14ad26dd1d8ea8210036c51de1fc3bfbd872 Mon Sep 17 00:00:00 2001
From: Cameron Freer <cameronfreer@gmail.com>
Date: Mon, 24 Aug 2026 04:02:46 +0000
Subject: [PATCH 07/13] feat: the screening remainder computes the weak-union
 hypothesis (#197, acceptance steps 2b and 3)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

**Check 2**, packaged as a measurable factorization rather than a bare algebra
inequality. `restToPollingData e F heF` sends the screening remainder to the
accumulated `F`-blocks paired with the entire polling conditioning, and
`restToPollingData_comp` proves the identity on the nose. This records exactly what
information `restObservationOver n A` supplies — the fact the induction depends on —
and lets `CondIndepFun.comp` consume `Q.screening` directly instead of rebuilding
measurability coordinate by coordinate and discarding the assembled map.

The two separations: `supportImage_ne_of_ne` reduces original-block-versus-`A`
equality to `B = e` by injectivity of `supportImage`, contradicting `e ∉ F`; and
`mixedCluster_ne_supportImage` uses that a cluster carries a spare vertex while the
image of an original support is wholly original.

**Check 3** is the named identity `comap_pollingCond_comp_enrichedPollingMap`, kept
explicit rather than left for `simp` to rediscover, so the forward descent at the end
of the construction is visibly exact.

`mem_supportImage_iff` is added to `RelObservationGeometry`: this is the third site
where a classical `DecidableEq` used to form an image is not definitionally the
natural instance available over a concrete carrier — here `PoolVertex`, whose `Sum`
supplies one — so image-shaped rewriting is unusable and the membership form, which
carries no instance in its type, is stated once alongside the geometry instead of
being worked around again locally.

Gates: lake build clean (3409 jobs), census + axiom audit pass, zero sorries, no
warnings.
---
 Graphon/RelAustinPolling.lean       | 91 +++++++++++++++++++++++++++++
 Graphon/RelObservationGeometry.lean | 10 ++++
 2 files changed, 101 insertions(+)

diff --git a/Graphon/RelAustinPolling.lean b/Graphon/RelAustinPolling.lean
index e11a87b..f2fc632 100644
--- a/Graphon/RelAustinPolling.lean
+++ b/Graphon/RelAustinPolling.lean
@@ -342,6 +342,97 @@ theorem comap_localLatents_le_sourcePollingCond (A : Finset (Σ s : S.Srt, PoolV
   exact MeasurableSpace.comap_mono
     ((measurable_localLatentsOver A n).comp measurable_fst).comap_le
 
+/-! ### What the screening remainder supplies
+
+`Q.screening` gives conditional independence of the block at a pooled support `A` from
+`restObservationOver n A` — the other rank-`≤ n` blocks together with the whole pooled latent
+array. Weak union needs that remainder to dominate *both* the accumulated `F`-blocks and the whole
+polling conditioning. `restToPollingData` exhibits that as a single measurable factorization rather
+than as a bare algebra inequality, so it records exactly which information the remainder supplies
+and lets `CondIndepFun.comp` consume the screening statement directly. -/
+
+open scoped Classical in
+omit [Countable S.Rel] in
+/-- A support in the image of the original half carries no spare vertex. -/
+theorem isRight_eq_false_of_mem_supportImage_original
+    {X : Finset (Σ s : S.Srt, Vinfinite S s)} {v : Σ s : S.Srt, PoolVertex S s}
+    (hv : v ∈ supportImage (originalVertex S) X) : Sum.isRight v.2 = false := by
+  obtain ⟨w, -, rfl⟩ := (mem_supportImage_iff _ _ _).mp hv
+  rfl
+
+open scoped Classical in
+omit [Countable S.Rel] in
+/-- **Separation, original against original**: distinct rank-`n` supports have distinct images,
+since `supportImage` is injective. -/
+theorem supportImage_ne_of_ne {B e : RankSupport S n} (h : B ≠ e) :
+    supportImage (originalVertex S) B.1 ≠ supportImage (originalVertex S) e.1 :=
+  fun heq => h (Subtype.ext (supportImage_injective _ heq))
+
+open scoped Classical in
+/-- **Separation, cluster against original**: a mixed cluster carries a spare vertex, while the
+image of an original support is wholly original. -/
+theorem mixedCluster_ne_supportImage (Ac : MixedClusterIndex S n) (e : RankSupport S n) :
+    Ac.1 ≠ supportImage (originalVertex S) e.1 := by
+  obtain ⟨v, hv, hvr⟩ := Ac.2.2
+  intro heq
+  rw [heq] at hv
+  rw [isRight_eq_false_of_mem_supportImage_original hv] at hvr
+  exact absurd hvr (by simp)
+
+open scoped Classical in
+/-- The accumulated block observation space, indexed by a finite family of rank-`n` supports. -/
+abbrev FBlockSpace (F : Finset (RankSupport S n)) :=
+  (B : {x : RankSupport S n // x ∈ F}) →
+    BlockSpaceOver (PoolVertex S) (supportImage (originalVertex S) B.1.1)
+
+open scoped Classical in
+/-- **The screening remainder computes both sides of the weak-union hypothesis**: the accumulated
+`F`-blocks and the entire polling conditioning are read off `restObservationOver n A` alone. -/
+noncomputable def restToPollingData (e : RankSupport S n) (F : Finset (RankSupport S n))
+    (heF : e ∉ F) :
+    RestSpaceOver (PoolVertex S) n (supportImage (originalVertex S) e.1) ×
+        PooledRankLatentSpace S n →
+      FBlockSpace F × (PooledRankLatentSpace S n × ClusterSpace S n) :=
+  fun q =>
+    (fun B c => q.1 ⟨c.1, by
+        refine ⟨?_, ?_⟩
+        · rw [c.2, card_supportImage]; exact le_of_eq B.1.2
+        · rw [c.2]; exact supportImage_ne_of_ne fun h => heF (h ▸ B.2)⟩,
+      (q.2, fun Ac c => q.1 ⟨c.1, by
+        refine ⟨?_, ?_⟩
+        · rw [c.2]; exact le_of_eq Ac.2.1
+        · rw [c.2]; exact mixedCluster_ne_supportImage Ac e⟩))
+
+open scoped Classical in
+theorem measurable_restToPollingData (e : RankSupport S n) (F : Finset (RankSupport S n))
+    (heF : e ∉ F) : Measurable (restToPollingData e F heF) :=
+  (measurable_pi_lambda _ fun _ => measurable_pi_lambda _ fun _ => measurable_fst.eval).prodMk
+    (measurable_snd.prodMk
+      (measurable_pi_lambda _ fun _ => measurable_pi_lambda _ fun _ => measurable_fst.eval))
+
+open scoped Classical in
+/-- **The exact factorization.** Both the accumulated blocks and the polling conditioning are
+functions of the screening remainder, on the nose. -/
+theorem restToPollingData_comp (e : RankSupport S n) (F : Finset (RankSupport S n)) (heF : e ∉ F) :
+    (fun p : RelStructure S (PoolVertex S) × PooledRankLatentSpace S n =>
+        ((fun B : {x : RankSupport S n // x ∈ F} => originalBlock B.1 p), sourcePollingCond p)) =
+      restToPollingData e F heF ∘ restObservationOver n (supportImage (originalVertex S) e.1) :=
+  rfl
+
+/-! ### The conditioning algebra is the fixed one
+
+Named rather than left to `simp`: the forward descent at the end of the construction has to be
+visibly exact, and that requires an explicit identity between the algebra the source statement
+conditions on and the pullback of `pollingCond`. -/
+
+open scoped Classical in
+omit [Countable S.Srt] [Countable S.Rel] in
+/-- **Check 3**: the source conditioning algebra *is* the pullback of the enriched conditioning. -/
+theorem comap_pollingCond_comp_enrichedPollingMap :
+    MeasurableSpace.comap (pollingCond S n ∘ enrichedPollingMap) inferInstance =
+      MeasurableSpace.comap (sourcePollingCond (S := S) (n := n)) inferInstance :=
+  congrArg (fun f => MeasurableSpace.comap f inferInstance) pollingCond_comp_enrichedPollingMap
+
 /-! ### The witness -/
 
 variable [Fintype S.Srt]
diff --git a/Graphon/RelObservationGeometry.lean b/Graphon/RelObservationGeometry.lean
index 3487db8..46a340b 100644
--- a/Graphon/RelObservationGeometry.lean
+++ b/Graphon/RelObservationGeometry.lean
@@ -167,6 +167,16 @@ noncomputable def supportImage (e : ∀ s, V s ↪ W s) (A : Finset (Σ s : S.Sr
     Finset (Σ s : S.Srt, W s) :=
   A.image (Sigma.map id fun s => ⇑(e s))
 
+open scoped Classical in
+/-- **Membership in a support image**, stated without an image in the type so that no `DecidableEq`
+instance appears in it. Over a carrier with a natural instance — `PoolVertex`, whose `Sum` gives
+one — that instance is not definitionally the classical one used to form the image, which makes
+image-shaped rewriting unusable there; this form is not. -/
+theorem mem_supportImage_iff (e : ∀ s, V s ↪ W s) (A : Finset (Σ s : S.Srt, V s))
+    (v : Σ s : S.Srt, W s) :
+    v ∈ supportImage e A ↔ ∃ w ∈ A, Sigma.map id (fun s => ⇑(e s)) w = v :=
+  Finset.mem_image
+
 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

From 4f53f4839083c4b850955cca8ce8cb5a4265e761 Mon Sep 17 00:00:00 2001
From: Cameron Freer <cameronfreer@gmail.com>
Date: Mon, 24 Aug 2026 22:16:07 +0000
Subject: [PATCH 08/13] feat: the polling insertion identity (#197, acceptance
 step 4 prerequisite)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

`polling_condExp_insert`: the peel step, as a direct conditional-expectation
identity rather than a packaged conditional-independence statement, so that it drops
into `Finset.induction_on` with `Set.biInter_insert` and `Finset.prod_insert` and no
dependent tuple reindexing happens inside the induction.

Assembled from the pieces already banked: `Q.screening` at the original image of
`e`; its remainder composed with `restToPollingData`; `comap_prodMk` splitting the
resulting algebra into the accumulated blocks joined with the polling conditioning;
and `condIndep_weak_union` dropping back to the polling conditioning alone, with
check 1 supplying `W ≤ Z`.

The conclusion conditions on exactly `comap sourcePollingCond` — literally the same
term at every stage — which is what keeps the induction free of any accumulating
conditioning.

Lean note: `comap_prodMk` is stated against `MeasurableSpace.prod` while the goal
carries `Prod.instMeasurableSpace`; they are definitionally equal but not
syntactically, so the rewrite needs an explicit `rfl` bridge.

Gates: lake build clean (3409 jobs), census + axiom audit pass, zero sorries, no
warnings.
---
 Graphon/RelAustinPolling.lean | 60 +++++++++++++++++++++++++++++++++++
 1 file changed, 60 insertions(+)

diff --git a/Graphon/RelAustinPolling.lean b/Graphon/RelAustinPolling.lean
index f2fc632..16e2b0c 100644
--- a/Graphon/RelAustinPolling.lean
+++ b/Graphon/RelAustinPolling.lean
@@ -433,6 +433,66 @@ theorem comap_pollingCond_comp_enrichedPollingMap :
       MeasurableSpace.comap (sourcePollingCond (S := S) (n := n)) inferInstance :=
   congrArg (fun f => MeasurableSpace.comap f inferInstance) pollingCond_comp_enrichedPollingMap
 
+/-! ### The insertion identity
+
+The peel step, assembled from the pieces above: `Q.screening` at the original image of `e`, its
+remainder pushed through `restToPollingData`, `comap_prodMk` to split the resulting algebra into
+the accumulated blocks joined with the polling conditioning, and weak union to drop back to the
+polling conditioning alone. Stated as a direct conditional-expectation identity so that it feeds
+`Finset.induction_on` with `Set.biInter_insert` and `Finset.prod_insert`, without any dependent
+tuple reindexing inside the induction. -/
+
+open scoped Classical in
+private theorem polling_condExp_insert {C : M.RankRepresentation n} (Q : PooledRankExtension C)
+    (e : RankSupport S n) (F : Finset (RankSupport S n)) (heF : e ∉ F)
+    (sets : ∀ A : RankSupport S n,
+      Set (BlockSpaceOver (PoolVertex S) (supportImage (originalVertex S) A.1)))
+    (hsets : ∀ A, A ∈ insert e F → MeasurableSet (sets A)) :
+    ((Q.law : Measure (RelStructure S (PoolVertex S) × PooledRankLatentSpace S n))⟦
+        originalBlock e ⁻¹' sets e ∩ ⋂ A ∈ F, originalBlock A ⁻¹' sets A |
+        MeasurableSpace.comap (sourcePollingCond (S := S) (n := n)) inferInstance⟧)
+      =ᵐ[(Q.law : Measure (RelStructure S (PoolVertex S) × PooledRankLatentSpace S n))]
+    ((Q.law : Measure (RelStructure S (PoolVertex S) × PooledRankLatentSpace S n))⟦
+        originalBlock e ⁻¹' sets e |
+        MeasurableSpace.comap (sourcePollingCond (S := S) (n := n)) inferInstance⟧) *
+      ((Q.law : Measure (RelStructure S (PoolVertex S) × PooledRankLatentSpace S n))⟦
+        ⋂ A ∈ F, originalBlock A ⁻¹' sets A |
+        MeasurableSpace.comap (sourcePollingCond (S := S) (n := n)) inferInstance⟧) := by
+  haveI := C.isProbabilityMeasure_P
+  have hA₀ : (supportImage (originalVertex S) e.1).card = n := by
+    rw [card_supportImage]; exact e.2
+  -- the paired observation: accumulated blocks against the polling conditioning
+  set Y : RelStructure S (PoolVertex S) × PooledRankLatentSpace S n → FBlockSpace F :=
+    fun p B => originalBlock B.1 p with hY
+  have hYmeas : Measurable Y :=
+    measurable_pi_lambda _ fun B => measurable_originalBlock B.1
+  -- screening, with its remainder pushed through the factorization
+  have hcomp := (Q.screening (supportImage (originalVertex S) e.1) hA₀).comp
+    (measurable_id (α := BlockSpaceOver (PoolVertex S) (supportImage (originalVertex S) e.1)))
+    (measurable_restToPollingData e F heF)
+  rw [condIndepFun_iff_condIndep] at hcomp
+  have hpair : (restToPollingData e F heF ∘
+      restObservationOver n (supportImage (originalVertex S) e.1)) =
+      fun p => (Y p, sourcePollingCond p) := (restToPollingData_comp e F heF).symm
+  rw [hpair, show (Prod.instMeasurableSpace :
+      MeasurableSpace (FBlockSpace F × (PooledRankLatentSpace S n × ClusterSpace S n))) =
+        MeasurableSpace.prod _ _ from rfl,
+    MeasurableSpace.comap_prodMk] at hcomp
+  -- weak union: drop the accumulated blocks out of the conditioning
+  have hwu := condIndep_weak_union
+    (((measurable_localLatentsOver (supportImage (originalVertex S) e.1) n).comp
+      measurable_snd).comap_le)
+    ((measurable_id.comp (measurable_originalBlock e)).comap_le)
+    hYmeas.comap_le (measurable_sourcePollingCond (S := S) (n := n)).comap_le
+    (comap_localLatents_le_sourcePollingCond (supportImage (originalVertex S) e.1)) hcomp
+  -- read off the event identity
+  rw [condIndep_iff _ _ _ (measurable_sourcePollingCond (S := S) (n := n)).comap_le
+    ((measurable_id.comp (measurable_originalBlock e)).comap_le) hYmeas.comap_le] at hwu
+  refine hwu _ _ ⟨sets e, hsets e (Finset.mem_insert_self _ _), rfl⟩ ?_
+  refine MeasurableSet.biInter F.countable_toSet fun A hA => ?_
+  exact ⟨(fun x : FBlockSpace F => x ⟨A, hA⟩) ⁻¹' sets A,
+    (measurable_pi_apply _) (hsets A (Finset.mem_insert_of_mem hA)), rfl⟩
+
 /-! ### The witness -/
 
 variable [Fintype S.Srt]

From 97903674bee54a5b61147feba079b4680da021b6 Mon Sep 17 00:00:00 2001
From: Cameron Freer <cameronfreer@gmail.com>
Date: Mon, 24 Aug 2026 22:32:20 +0000
Subject: [PATCH 09/13] feat: source-level mutual conditional independence
 (#197, acceptance step 4)

`PooledRankExtension.iCondIndepFun_originalBlock_sourcePollingCond`: the whole
rank-`n` block family is mutually conditionally independent under `Q.law` given the
polling conditioning.

Named at top level rather than inlined into the witness, because it is the
load-bearing consumer of `polling_condExp_insert` and the direct input to the
forward descent. Keeping it separate makes it independently reviewable and leaves
the eventual witness constructor carrying no probability argument of its own.

The proof is structurally the singleton peel: rewrite by
`iCondIndepFun_iff_condExp_inter_preimage_eq_mul`, induct with `Finset.induction_on`,
discharge the empty stage by `condExp_const`, and discharge each insertion by
`polling_condExp_insert` against the induction hypothesis. Nothing accumulates in
the conditioning, since the insertion identity already conditions on exactly
`comap sourcePollingCond`.

Lean note: the index is a `Finset`, so the insert step needs
`Finset.set_biInter_insert`, not `Set.biInter_insert`.

Gates: lake build clean (3409 jobs), census + axiom audit pass, zero sorries, no
warnings.
---
 Graphon/RelAustinPolling.lean | 36 +++++++++++++++++++++++++++++++++++
 1 file changed, 36 insertions(+)

diff --git a/Graphon/RelAustinPolling.lean b/Graphon/RelAustinPolling.lean
index 16e2b0c..a20eab5 100644
--- a/Graphon/RelAustinPolling.lean
+++ b/Graphon/RelAustinPolling.lean
@@ -493,6 +493,42 @@ private theorem polling_condExp_insert {C : M.RankRepresentation n} (Q : PooledR
   exact ⟨(fun x : FBlockSpace F => x ⟨A, hA⟩) ⁻¹' sets A,
     (measurable_pi_apply _) (hsets A (Finset.mem_insert_of_mem hA)), rfl⟩
 
+/-! ### The source-level mutual theorem
+
+Named rather than inlined into the witness: it is the load-bearing consumer of
+`polling_condExp_insert` and the direct input to the forward descent, so keeping it separate makes
+it independently reviewable and leaves the final constructor carrying no probability argument of
+its own. -/
+
+open scoped Classical in
+/-- **Mutual conditional independence of the whole rank-`n` block family under `Q.law`**, given the
+polling conditioning. The peel is structurally the singleton peel: the empty stage is a constant,
+and each insertion is discharged by `polling_condExp_insert` against the induction hypothesis, with
+the conditioning algebra fixed throughout. -/
+theorem PooledRankExtension.iCondIndepFun_originalBlock_sourcePollingCond
+    {C : M.RankRepresentation n} (Q : PooledRankExtension C) :
+    iCondIndepFun (MeasurableSpace.comap (sourcePollingCond (S := S) (n := n)) inferInstance)
+      (measurable_sourcePollingCond (S := S) (n := n)).comap_le
+      (fun A : RankSupport S n => originalBlock (S := S) (n := n) A)
+      (Q.law : Measure (RelStructure S (PoolVertex S) × PooledRankLatentSpace S n)) := by
+  haveI := C.isProbabilityMeasure_P
+  rw [iCondIndepFun_iff_condExp_inter_preimage_eq_mul _ _
+    fun A => measurable_originalBlock (S := S) (n := n) A]
+  intro T sets
+  induction T using Finset.induction_on with
+  | empty =>
+      intro _
+      simp only [Finset.notMem_empty, Set.iInter_of_empty, Set.iInter_univ, Finset.prod_empty,
+        Set.indicator_univ]
+      rw [condExp_const (measurable_sourcePollingCond (S := S) (n := n)).comap_le (1 : ℝ)]
+      rfl
+  | insert e F heF ih =>
+      intro hsets
+      have ihs := ih fun A hA => hsets A (Finset.mem_insert_of_mem hA)
+      rw [Finset.set_biInter_insert, Finset.prod_insert heF]
+      exact (polling_condExp_insert Q e F heF sets hsets).trans
+        (Filter.EventuallyEq.mul Filter.EventuallyEq.rfl ihs)
+
 /-! ### The witness -/
 
 variable [Fintype S.Srt]

From 273f2f7c16c8b02114b1a432fef5f8b49ff0d35b Mon Sep 17 00:00:00 2001
From: Cameron Freer <cameronfreer@gmail.com>
Date: Tue, 25 Aug 2026 01:19:04 +0000
Subject: [PATCH 10/13] =?UTF-8?q?feat:=20the=20polling=20witness=20exists?=
 =?UTF-8?q?=20=E2=80=94=20Austin=20unit=201=20complete=20(#197,=20acceptan?=
 =?UTF-8?q?ce=20step=205)?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

`pooledPollingWitness` constructs a `PooledPollingWitness` for every pooled rank
extension. The constructor is **pure transport**: all probability content lives in
`iCondIndepFun_originalBlock_sourcePollingCond`, and step 5 only moves it along
`enrichedPollingMap`.

Two obligations, both discharged by named identities rather than coerced ad hoc:
the conditioning algebra, via `comap_pollingCond_comp_enrichedPollingMap`; and the
block **codomains**, which genuinely differ — the source family lands in
`BlockSpaceOver (PoolVertex S) (supportImage (originalVertex S) A)` while the witness
reads `blockMap A` on the restricted original structure. `blockSpaceCongr` is the
equivalence and `enrichedBlock_comp_enrichedPollingMap` the exact identity.

`iCondIndepFun_of_map` is brought in privately, adjacent to its one consumer, and
consumed immediately; the general form stays proved and preserved on its own branch
until a second independent consumer exists. `iCondIndepFun_comp` is the familywise
codomain composition Mathlib lacks, built from `Kernel.iIndepFun.comp` exactly as
`CondIndepFun.comp` is.

Closing items: the `RelPollingInfrastructure` import is **dropped**, since weak union
replaced the tail engine at this stage and manufacturing a dependency would be
dishonest; and the prose is recalibrated. The construction is Austin's — spare
reservoir, mixed clusters, enriched law — but the conditional-independence engine is
not: `screening` is a field assumed at rank `n`, weak union converts it, and
Proposition 3.12 is **not** reproved here. The witness docstring had claimed the
conclusion was Proposition 3.12 and is corrected.

Audit 429 → 433. Gates: lake build clean (3409 jobs), census + axiom audit pass, zero
sorries, no warnings.
---
 Graphon/RelAustinPolling.lean      | 160 +++++++++++++++++++++++++++--
 scripts/axiom_audit.lean           |   4 +
 scripts/check_census_and_axioms.py |   4 +
 3 files changed, 157 insertions(+), 11 deletions(-)

diff --git a/Graphon/RelAustinPolling.lean b/Graphon/RelAustinPolling.lean
index a20eab5..960ad0e 100644
--- a/Graphon/RelAustinPolling.lean
+++ b/Graphon/RelAustinPolling.lean
@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Cameron Freer
 -/
 import Graphon.RelPooledAcceptance
-import Graphon.RelPollingInfrastructure
 import Graphon.ForMathlib.CondExpComap
 
 /-!
@@ -14,11 +13,20 @@ Route **A** (Austin) only. Nothing from the Kallenberg spine appears here, and n
 module asserts that the two routes' outputs agree — they prove the same statement by different
 means and will not produce canonically equal representations.
 
-Austin's Proposition 3.12 (arXiv:0801.1698) runs its polling argument with finitely supported
-swaps into a **spare vertex set**. The pooled carrier is exactly that: `PoolVertex S s` is
+## What is Austin's here, and what is not
+
+The **construction** follows Austin (arXiv:0801.1698): a spare vertex reservoir, mixed clusters
+straddling it, and an enriched law that carries the polling data forward. `PoolVertex S s` is
 `Vinfinite S s ⊕ Vinfinite S s`, with `originalVertex = Sum.inl` and `poolVertex = Sum.inr`, so the
-two halves are disjoint definitionally; and a `PooledRankExtension` is invariant under the *full*
-pooled permutation family, so the swaps carry no finite-support or uniform-bound side condition.
+two halves are disjoint definitionally, and a `PooledRankExtension` is invariant under the *full*
+pooled permutation family.
+
+The **conditional-independence engine is not Austin's**, and this module does not reprove his
+Proposition 3.12. `RankRepresentation.screening` is a field — an inductive hypothesis assumed at
+rank `n` — and its remainder already contains every other rank-`≤ n` block together with the whole
+pooled latent array. Weak union converts that directly into the mutual statement, so the
+tail-polling argument is not needed at this inductive stage and no tail machinery appears here.
+Stating otherwise would credit this file with a theorem it does not contain.
 
 ## The geometry, and a trap it sets
 
@@ -79,6 +87,18 @@ variable {S : RelSignature} [Countable S.Srt] [Countable S.Rel]
 
 attribute [local instance] RankRepresentation.isProbabilityMeasure_P
 
+/-- **The conditioning σ-algebra may be replaced by an equal one**, for a family. The
+`CondIndepFun` form is shared glue in `ForMathlib/CondIndepSup.lean`; this is its `iCondIndepFun`
+counterpart, private under the standing promotion rule. Needed because the conditioning algebra
+occurs in a dependent position — the `≤` proof mentions it — so `rw` cannot reach it. -/
+private theorem iCondIndepFun_congr_cond {Ω : Type*} [mΩ : MeasurableSpace Ω]
+    [StandardBorelSpace Ω] {μ : Measure Ω} [IsFiniteMeasure μ]
+    {ι : Type*} {γ : ι → Type*} [∀ i, MeasurableSpace (γ i)] {Y : ∀ i, Ω → γ i}
+    {m₁ m₂ : MeasurableSpace Ω} {h1 : m₁ ≤ mΩ} (h : iCondIndepFun m₁ h1 Y μ)
+    (h12 : m₁ = m₂) (h2 : m₂ ≤ mΩ) : iCondIndepFun m₂ h2 Y μ := by
+  subst h12
+  exact h
+
 /-! ### Weak union for conditional independence
 
 The graphoid axiom this development turns on, and which neither Mathlib nor this repository has:
@@ -529,17 +549,102 @@ theorem PooledRankExtension.iCondIndepFun_originalBlock_sourcePollingCond
       exact (polling_condExp_insert Q e F heF sets hsets).trans
         (Filter.EventuallyEq.mul Filter.EventuallyEq.rfl ihs)
 
+/-! ### Transport to the enriched law
+
+Two obligations, both discharged by named identities so that nothing is coerced ad hoc inside the
+witness constructor: the conditioning algebra (check 3) and the block **codomains**. The source
+family lands in `BlockSpaceOver (PoolVertex S) (supportImage (originalVertex S) A)`, whereas the
+witness reads `blockMap A` on the restricted original structure; `blockSpaceCongr` is the
+measurable equivalence between them and `blockMapOver_restrict` is the naturality that relates the
+two readings exactly. -/
+
+/-- Familywise composition on the codomain, the `iCondIndepFun` counterpart of `CondIndepFun.comp`
+and built the same way, from the kernel-level lemma. Private under the standing promotion rule. -/
+private theorem iCondIndepFun_comp {Ω : Type*} [mΩ : MeasurableSpace Ω] [StandardBorelSpace Ω]
+    {μ : Measure Ω} [IsFiniteMeasure μ] {m' : MeasurableSpace Ω} {hm' : m' ≤ mΩ}
+    {ι : Type*} {β γ : ι → Type*} [∀ i, MeasurableSpace (β i)] [∀ i, MeasurableSpace (γ i)]
+    {f : ∀ i, Ω → β i} (h : iCondIndepFun m' hm' f μ)
+    (φ : ∀ i, β i → γ i) (hφ : ∀ i, Measurable (φ i)) :
+    iCondIndepFun m' hm' (fun i => φ i ∘ f i) μ :=
+  Kernel.iIndepFun.comp h φ hφ
+
+open scoped Classical in
+omit [Countable S.Srt] in
+/-- **The block codomains agree, exactly.** Reading a block of the restricted original structure is
+reading the pooled block at the image support and transporting along `blockSpaceCongr`. -/
+theorem enrichedBlock_comp_enrichedPollingMap (A : RankSupport S n) :
+    ((blockMap A.1 ∘ Prod.fst ∘ Prod.fst) ∘ enrichedPollingMap :
+      RelStructure S (PoolVertex S) × PooledRankLatentSpace S n → BlockSpace (S := S) A.1) =
+      blockSpaceCongr (originalVertex S) A.1 ∘ originalBlock (S := S) (n := n) A := by
+  funext p
+  exact congrFun (blockMapOver_restrict (originalVertex S) A.1) p.1
+
+/-- **Forward transport of mutual conditional independence along a measurable map.** Brought in
+privately, adjacent to its one consumer, under the standing promotion rule; the general form is
+proved and preserved on its own branch and moves to `ForMathlib/` when a second independent
+consumer exists. No injectivity is needed — `enrichedPollingMap` forgets the spare half of the
+structure — which is exactly why neither direction of the existing transport API applies. -/
+private theorem iCondIndepFun_of_map {α β : Type*} {m' : MeasurableSpace β}
+    [mα : MeasurableSpace α] [mβ : MeasurableSpace β]
+    [StandardBorelSpace α] [StandardBorelSpace β]
+    {P : Measure α} [IsFiniteMeasure P] {T : α → β}
+    (hT : Measurable T) (hm' : m' ≤ mβ)
+    {ι : Type*} {γ : ι → Type*} [mγ : ∀ i, MeasurableSpace (γ i)] {Y : ∀ i, β → γ i}
+    (hY : ∀ i, Measurable (Y i))
+    (h : iCondIndepFun (m'.comap T)
+      ((MeasurableSpace.comap_mono hm').trans (measurable_iff_comap_le.mp hT))
+      (fun i => Y i ∘ T) P) :
+    iCondIndepFun m' hm' Y (P.map T) := by
+  haveI : IsFiniteMeasure (P.map T) := Measure.isFiniteMeasure_map P T
+  have hTmp : MeasurePreserving T P (P.map T) := ⟨hT, rfl⟩
+  have key : ∀ E : Set β, MeasurableSet E →
+      (P⟦T ⁻¹' E | m'.comap T⟧) =ᵐ[P] ((P.map T)⟦E | m'⟧) ∘ T :=
+    fun _ hE => condExp_set_comp_measurePreserving hTmp hm' hE
+  rw [iCondIndepFun_iff_condExp_inter_preimage_eq_mul _ _ hY]
+  rw [iCondIndepFun_iff_condExp_inter_preimage_eq_mul _ _ fun i => (hY i).comp hT] at h
+  intro S sets hsets
+  have hsrc := h S hsets
+  have hinter : MeasurableSet (⋂ i ∈ S, Y i ⁻¹' sets i) :=
+    MeasurableSet.biInter S.countable_toSet fun i hi => (hY i) (hsets i hi)
+  have hpre : ⋂ i ∈ S, (Y i ∘ T) ⁻¹' sets i = T ⁻¹' ⋂ i ∈ S, Y i ⁻¹' sets i := by
+    simp [Set.preimage_comp, Set.preimage_iInter]
+  rw [hpre] at hsrc
+  have h₁ := key _ hinter
+  have hfac : ∀ᵐ x ∂P, ∀ i ∈ S, (P⟦(Y i ∘ T) ⁻¹' sets i | m'.comap T⟧) x
+      = (((P.map T)⟦Y i ⁻¹' sets i | m'⟧) ∘ T) x := by
+    refine (ae_ball_iff S.countable_toSet).2 fun i hi => ?_
+    rw [Set.preimage_comp]
+    exact key _ ((hY i) (hsets i hi))
+  have hcomp : ((P.map T)⟦⋂ i ∈ S, Y i ⁻¹' sets i | m'⟧) ∘ T
+      =ᵐ[P] (∏ i ∈ S, ((P.map T)⟦Y i ⁻¹' sets i | m'⟧)) ∘ T := by
+    filter_upwards [h₁, hsrc, hfac] with x e₁ esrc efac
+    simp only [Function.comp_apply] at e₁ ⊢
+    rw [← e₁, esrc]
+    show (∏ i ∈ S, (P⟦(Y i ∘ T) ⁻¹' sets i | m'.comap T⟧)) x = _
+    simp only [Finset.prod_apply]
+    exact Finset.prod_congr rfl fun i hi => efac i hi
+  have hmeas : MeasurableSet {y : β | ((P.map T)⟦⋂ i ∈ S, Y i ⁻¹' sets i | m'⟧) y =
+      (∏ i ∈ S, ((P.map T)⟦Y i ⁻¹' sets i | m'⟧)) y} := by
+    refine measurableSet_eq_fun (stronglyMeasurable_condExp.mono hm').measurable ?_
+    have heq : (∏ i ∈ S, ((P.map T)⟦Y i ⁻¹' sets i | m'⟧)) =
+        fun y : β => ∏ i ∈ S, ((P.map T)⟦Y i ⁻¹' sets i | m'⟧) y :=
+      funext fun y => Finset.prod_apply y S _
+    rw [heq]
+    exact Finset.measurable_prod S fun i _ => (stronglyMeasurable_condExp.mono hm').measurable
+  exact (ae_map_iff hT.aemeasurable hmeas).mpr hcomp
+
 /-! ### The witness -/
 
 variable [Fintype S.Srt]
 
-/-- **What the polling argument must supply**: mutual conditional independence of the *entire*
-rank-`n` block family of the original structure, given the old latents and the mixed clusters,
-under the enriched law.
+/-- **The polling conclusion**: mutual conditional independence of the *entire* rank-`n` block
+family of the original structure, given the pooled latents and the mixed clusters, under the
+enriched law.
 
-`iCondIndepFun` over the whole family is Austin's Proposition 3.12 conclusion. Pairwise
-independence, or one block against the rest, would be strictly weaker, and the adversarial battery
-of #196 exists to keep that distinction honest. -/
+`iCondIndepFun` over the whole family is the shape Austin's Proposition 3.12 delivers, but here it
+is obtained from the assumed rank-`n` screening contract by weak union rather than by a tail-polling
+argument. Pairwise independence, or one block against the rest, would be strictly weaker, and the
+adversarial battery of #196 exists to keep that distinction honest. -/
 structure PooledPollingWitness (C : M.RankRepresentation n) (Q : PooledRankExtension C) where
   /-- **Mutual** conditional independence of the whole rank-`n` block family. -/
   mutualCondIndep :
@@ -548,6 +653,39 @@ structure PooledPollingWitness (C : M.RankRepresentation n) (Q : PooledRankExten
       (fun A : RankSupport S n => blockMap A.1 ∘ Prod.fst ∘ Prod.fst)
       (enrichedPollingLaw Q)
 
+open scoped Classical in
+/-- **The polling witness exists**, for every pooled rank extension. Pure transport: the
+probability content is `iCondIndepFun_originalBlock_sourcePollingCond`, and this constructor only
+moves it along `enrichedPollingMap`, matching the block codomains by `blockSpaceCongr` and the
+conditioning algebra by the named identity. -/
+noncomputable def pooledPollingWitness {C : M.RankRepresentation n} (Q : PooledRankExtension C) :
+    PooledPollingWitness C Q where
+  mutualCondIndep := by
+    haveI := C.isProbabilityMeasure_P
+    -- step 1: transport the codomains
+    have h1 := iCondIndepFun_comp Q.iCondIndepFun_originalBlock_sourcePollingCond
+      (fun A : RankSupport S n => (blockSpaceCongr (originalVertex S) A.1 : _ → _))
+      fun A => (blockSpaceCongr (originalVertex S) A.1).measurable
+    -- step 2: read the transported family as the enriched blocks precomposed with the map
+    have h2 : (fun A : RankSupport S n =>
+        (blockSpaceCongr (originalVertex S) A.1 : _ → _) ∘ originalBlock (S := S) (n := n) A) =
+        fun A : RankSupport S n =>
+          (blockMap A.1 ∘ Prod.fst ∘ Prod.fst) ∘ enrichedPollingMap :=
+      funext fun A => (enrichedBlock_comp_enrichedPollingMap A).symm
+    rw [h2] at h1
+    -- step 3: match the conditioning algebra to the pullback of the enriched one
+    have halg : MeasurableSpace.comap (sourcePollingCond (S := S) (n := n)) inferInstance =
+        (MeasurableSpace.comap (pollingCond S n) inferInstance).comap enrichedPollingMap :=
+      (MeasurableSpace.comap_comp.trans comap_pollingCond_comp_enrichedPollingMap).symm
+    have h3 := iCondIndepFun_congr_cond h1 halg
+      ((MeasurableSpace.comap_mono (measurable_pollingCond S n).comap_le).trans
+        (measurable_iff_comap_le.mp measurable_enrichedPollingMap))
+    -- step 4: push forward
+    exact iCondIndepFun_of_map measurable_enrichedPollingMap
+      (measurable_pollingCond S n).comap_le
+      (fun A : RankSupport S n =>
+        (measurable_blockMap A.1).comp (measurable_fst.comp measurable_fst)) h3
+
 end InfiniteRelExchangeableLaw
 
 end RelSignature
diff --git a/scripts/axiom_audit.lean b/scripts/axiom_audit.lean
index a144f76..ae31984 100644
--- a/scripts/axiom_audit.lean
+++ b/scripts/axiom_audit.lean
@@ -348,6 +348,10 @@ custom axioms. Target list and policy: `scripts/check_census_and_axioms.py`
 #print axioms RelSignature.BipartiteRegression.not_indepFun_rankTwoCoupling
 
 -- R4 converse route A (#197): pooled polling, unit 1.
+#print axioms RelSignature.InfiniteRelExchangeableLaw.PooledRankExtension.iCondIndepFun_originalBlock_sourcePollingCond
+#print axioms RelSignature.InfiniteRelExchangeableLaw.pooledPollingWitness
+#print axioms RelSignature.InfiniteRelExchangeableLaw.enrichedBlock_comp_enrichedPollingMap
+#print axioms RelSignature.mem_supportImage_iff
 #print axioms RelSignature.InfiniteRelExchangeableLaw.pollingClusters
 #print axioms RelSignature.InfiniteRelExchangeableLaw.enrichedPollingLaw
 #print axioms RelSignature.InfiniteRelExchangeableLaw.enrichedPollingLaw_map_fst
diff --git a/scripts/check_census_and_axioms.py b/scripts/check_census_and_axioms.py
index 06b66a9..8806974 100644
--- a/scripts/check_census_and_axioms.py
+++ b/scripts/check_census_and_axioms.py
@@ -308,6 +308,10 @@
     "RelSignature.BipartiteRegression.ae_edge_xor",
     "RelSignature.BipartiteRegression.not_indepFun_rankTwoCoupling",
     "RelSignature.InfiniteRelExchangeableLaw.pollingClusters",
+    "RelSignature.InfiniteRelExchangeableLaw.PooledRankExtension.iCondIndepFun_originalBlock_sourcePollingCond",
+    "RelSignature.InfiniteRelExchangeableLaw.pooledPollingWitness",
+    "RelSignature.InfiniteRelExchangeableLaw.enrichedBlock_comp_enrichedPollingMap",
+    "RelSignature.mem_supportImage_iff",
     "RelSignature.InfiniteRelExchangeableLaw.enrichedPollingLaw",
     "RelSignature.InfiniteRelExchangeableLaw.enrichedPollingLaw_map_fst",
     "support_digraphCoord",

From 81aac7fe657fd20fd02412c7525546263beb954f Mon Sep 17 00:00:00 2001
From: Cameron Freer <cameronfreer@gmail.com>
Date: Tue, 25 Aug 2026 15:54:12 +0000
Subject: [PATCH 11/13] docs: state the promotion rule timelessly on the
 private transport (#197)

The docstring referenced an unmerged branch as the home of the general form. An
unmerged branch is not part of the repository's API or provenance, and citing one is
the stale development-history prose we have been removing elsewhere. Replaced by the
timeless rule: private while it has one consumer, extract a general transport theorem
after a second independent consumer appears.

No statement or proof changes.
---
 Graphon/RelAustinPolling.lean | 9 ++++-----
 1 file changed, 4 insertions(+), 5 deletions(-)

diff --git a/Graphon/RelAustinPolling.lean b/Graphon/RelAustinPolling.lean
index 960ad0e..ea4782b 100644
--- a/Graphon/RelAustinPolling.lean
+++ b/Graphon/RelAustinPolling.lean
@@ -579,11 +579,10 @@ theorem enrichedBlock_comp_enrichedPollingMap (A : RankSupport S n) :
   funext p
   exact congrFun (blockMapOver_restrict (originalVertex S) A.1) p.1
 
-/-- **Forward transport of mutual conditional independence along a measurable map.** Brought in
-privately, adjacent to its one consumer, under the standing promotion rule; the general form is
-proved and preserved on its own branch and moves to `ForMathlib/` when a second independent
-consumer exists. No injectivity is needed — `enrichedPollingMap` forgets the spare half of the
-structure — which is exactly why neither direction of the existing transport API applies. -/
+/-- **Forward transport of mutual conditional independence along a measurable map.** Kept private
+while it has one consumer; extract a general transport theorem after a second independent consumer
+appears. No injectivity is needed — `enrichedPollingMap` forgets the spare half of the structure —
+which is exactly why neither direction of the existing transport API applies. -/
 private theorem iCondIndepFun_of_map {α β : Type*} {m' : MeasurableSpace β}
     [mα : MeasurableSpace α] [mβ : MeasurableSpace β]
     [StandardBorelSpace α] [StandardBorelSpace β]

From b3e4035dcb3cd5c07cbc82547f424995707c0187 Mon Sep 17 00:00:00 2001
From: Cameron Freer <cameronfreer@gmail.com>
Date: Tue, 25 Aug 2026 18:00:57 +0000
Subject: [PATCH 12/13] refactor: drop the unused Fintype hypothesis and clear
 stale prose (#197)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

* **`[Fintype S.Srt]` removed.** It was inherited from the fixing-algebra stack this
  unit was originally planned to build on; once weak union replaced the tail engine
  nothing needed it, and `pooledPollingWitness` carries only the ambient `Countable`
  assumptions. The module scope note and the `Graphon.lean` entry now say so, with
  the reason rather than a bare correction.

* **Stale geometry.** "Straddling" is gone from both files: "mixed" is the negation
  of "wholly original", so all-spare clusters are included. `pollingCond` is
  described as the whole pooled rank-`n` latent array plus the mixed clusters, not
  old or original latents. The permutation-stability rationale on `pollingCond` is
  replaced by the durable one — `Q.screening`'s remainder contains the pooled array
  in full and weak union conditions on exactly that lower-rank factor. That rationale
  had been corrected once at the header; this was a second copy on the definition.

* **Warnings cleared.** `pooledPollingWitness` is a `theorem`, not a Prop-valued
  `def`; six theorems gained `omit` clauses — four flagged plus two that surfaced
  once the `Fintype` variable was gone. `omit ... in` must precede the doc comment.

No statement or proof changes beyond the removed hypothesis, which strictly
generalizes the public signature.

Gates: lake build clean (3409 jobs), census + axiom audit pass, zero sorries, no
warnings.
---
 Graphon.lean                  |  2 +-
 Graphon/RelAustinPolling.lean | 34 ++++++++++++++++++----------------
 2 files changed, 19 insertions(+), 17 deletions(-)

diff --git a/Graphon.lean b/Graphon.lean
index c402581..65363e1 100644
--- a/Graphon.lean
+++ b/Graphon.lean
@@ -274,7 +274,7 @@ in Lean 4 using Mathlib.
 * `Graphon.RelPooledAcceptance` — R4 converse (#107), stage 3 of the pooled-latent extension gate, organizing result: **the joint restriction theorem**. For *every* sortwise embedding `e : ∀ s, Vinfinite S s ↪ PoolVertex S s`, restricting a pooled rank extension jointly — structure and latents along the same embedding — returns the representation exactly: `Q.law.map (Prod.map (RelStructure.restrict e) (latentRestrictOver e n)) = C.P`. Being **joint** is the point: it recovers the `(X, U_{<n})` law and says strictly more than a structure-only window theorem. Proved by joint-cylinder extensionality plus finite agreement with a mixed pooled permutation — on a cylinder the combined vertex support is finite, the assignment `originalVertex v ↦ e v` there is a finite partial injection of the pooled carrier, and `exists_perm_extend_of_injOn` extends it; the full mixed invariance then absorbs the permutation, which is also what lets it be chosen independently on each sort with no finite-support or uniform-bound issue. The four route-neutral consequences follow from it: `map_snd` (the pooled latent marginal is the pooled i.i.d. source), `toStationaryExtension` (the structure marginal is a `StationaryExtension M`), `lower_recovers` (local recovery on every pooled support below rank `n`, the decoder conjugated through the local and block measurable equivalences), and `screening` (screening on every pooled support of rank `n`, a pullback through `measurePreserving_pooledJointEquiv` followed by `CondIndepFun.comp` on the codomains and `CondIndepFun.congr_cond` with `comap_measurableEquiv_comp` on the conditioning algebra — no conditional-expectation reasoning). `PooledRankExtension.map_poolVertexEquiv` is the canonical specialization; bundling that restriction as the measurable equivalence `pooledJointEquiv` and cancelling it yields **`PooledRankExtension.law_eq`, a uniqueness theorem** — every pooled rank extension *is* the cheap one. Marginals, the `StationaryExtension` structure, recovery and screening therefore transport from `C.P` through one canonical law identity rather than requiring separate measure arguments
 * `Graphon.RelRankSuccessorContract` — R4 converse (#107), **interface only**: the shared witness both successor constructions must produce, and the two identically typed statements they target. `RankSuccessor C` carries the next representation together with **exact truncation compatibility**, `next.P.map (Prod.map id (rankLatentProjection (Nat.le_succ n))) = C.P` — the observable that makes the statement mention `C` at all. A theorem returning merely `Nonempty (RankRepresentation (n + 1))` could ignore `C` and produce an unrelated representation, which is the same underdetermination that sank the earlier shell attempt. The witness carries **no independence field** beyond `RankRepresentation`'s own, and **no equality between the two routes' outputs** is asserted — they prove one statement by different means and will not produce canonically equal representations. `AustinSuccessor` and `KallenbergSuccessor` are the same proposition by construction, so whichever lands first discharges the induction while the other remains an independent proof. Regression: `truncation_zero` shows the truncation equation is **automatic at rank zero** — the rank-zero latent cube is a single point, so both sides are determined by their structure marginals, which the representation axioms already pin, and the base case imposes nothing extra. The witness exposes no pooled carrier, so whether a construction genuinely used boundary-crossing permutations is observed by the pooled gate's `map_restrict_embedding` rather than by any final-output check here; each route's intermediate construction consumes that theorem. Adversarial examples are kept in route-independent regression modules, outside this interface
 * `Graphon.DigraphCoordSupport` — shared regression infrastructure: the support of a digraph coordinate is the pair of its endpoints, with the off-diagonal cardinality corollary, over an arbitrary vertex type. A bridge module so that the D1 carrier `Graphon.InfiniteDigraph` does not acquire a dependency on the equality-pattern layer where `RelCoord.support` lives — the same separation `Graphon.SimpleGraphDigraphBridge` maintains for `SimpleGraph`. Stated with `[DecidableEq V]` and proved by membership, because `RelCoord.support` is built classically and over a concrete carrier the natural instance is not definitionally the classical one, so an image-shaped statement would not apply at the sites that need it
-* `Graphon.RelAustinPolling` — R4 converse (#107/#197), **route A (Austin) unit 1**: pooled polling. Austin's Proposition 3.12 polls with swaps into a *spare vertex set*, and the pooled carrier is exactly that — `PoolVertex` is `Vinfinite ⊕ Vinfinite` with `originalVertex = Sum.inl` and `poolVertex = Sum.inr`, so the halves are disjoint definitionally, and the extension's invariance under the **full** pooled permutation family means the swaps carry no finite-support side condition. **The geometry is the delicate part**: the observed blocks are confined to the original half and the poll to supports containing a spare vertex, so the two families are disjoint by construction — reading the blocks through the canonical `pooledJointEquiv` instead is tempting, since it makes the transport to `C.P` exact, but it is wrong, because that bijection sends blocks across *both* summands and they would then overlap the poll. **The seam is an enriched law, not `C.P`**: Austin's polling data is the family of *mixed* clusters straddling the two halves, and forgetting it into a bare `C.P` statement would discard what the successor construction consumes, so `enrichedPollingLaw` retains the clusters alongside the original structure and old latents, with `enrichedPollingLaw_map_fst` recovering `C.P` exactly through `map_restrict_embedding` at the original-vertex embedding. `pollingCond` pins the conditioning concretely — old latents plus clusters — since an existential factor could be the whole joint object and make the conclusion vacuous. `PooledPollingWitness.mutualCondIndep` is `iCondIndepFun` over the **entire** rank-`n` block family: mutual, not pairwise, which is Austin's actual conclusion and what the #196 battery keeps honest. Carries `[Fintype S.Srt]` to match the polling/fixing-algebra stack, leaving the pooled API countable-only; rank zero is routed to `nonempty_rankRepresentation_one` with `truncation_zero`, respecting `stepKernel`'s deliberate lack of an `A = ∅` realization theorem
+* `Graphon.RelAustinPolling` — R4 converse (#107/#197), **route A (Austin) unit 1**: pooled polling. Austin's Proposition 3.12 polls with swaps into a *spare vertex set*, and the pooled carrier is exactly that — `PoolVertex` is `Vinfinite ⊕ Vinfinite` with `originalVertex = Sum.inl` and `poolVertex = Sum.inr`, so the halves are disjoint definitionally, and the extension's invariance under the **full** pooled permutation family means the swaps carry no finite-support side condition. **The geometry is the delicate part**: the observed blocks are confined to the original half and the poll to supports containing a spare vertex, so the two families are disjoint by construction — reading the blocks through the canonical `pooledJointEquiv` instead is tempting, since it makes the transport to `C.P` exact, but it is wrong, because that bijection sends blocks across *both* summands and they would then overlap the poll. **The seam is an enriched law, not `C.P`**: Austin's polling data is the family of *mixed* clusters — those not wholly original, all-spare included — spanning the two halves, and forgetting it into a bare `C.P` statement would discard what the successor construction consumes, so `enrichedPollingLaw` retains the clusters alongside the original structure and old latents, with `enrichedPollingLaw_map_fst` recovering `C.P` exactly through `map_restrict_embedding` at the original-vertex embedding. `pollingCond` pins the conditioning concretely — the whole pooled rank-`n` latent array plus the mixed clusters — since an existential factor could be the whole joint object and make the conclusion vacuous. `PooledPollingWitness.mutualCondIndep` is `iCondIndepFun` over the **entire** rank-`n` block family: mutual, not pairwise, which is Austin's actual conclusion and what the #196 battery keeps honest. Needs only the ambient `Countable` assumptions — because the conditional independence comes from the assumed screening contract rather than from a polling argument, the `Fintype S.Srt` hypothesis the fixing-algebra stack carries is not required; rank zero is routed to `nonempty_rankRepresentation_one` with `truncation_zero`, respecting `stepKernel`'s deliberate lack of an `A = ∅` realization theorem
 * `Graphon.RelBipartiteRegression` — R4 converse (#107/#196): the **bipartite regression** for the successor contract, a hand-built rank `1 → 2` witness over `digraphSig` whose purpose is to test that `RankSuccessor` is an expressive specification *before* either route is attempted. Each vertex carries an i.i.d. colour on its own fresh singleton coordinate and the edge is the parity, so the diagonal is constantly `false` for free. Three independent things make it a regression rather than a construction: the array law is defined **from the fresh singleton layer alone** and the rank-one coupling as the independent product `bipartiteLaw × rankLatentSource 1`, so `rankTwoCoupling_truncation` compares two separately described couplings and genuinely consumes the source factorization; the rank-two block decoder recovers **both** directed coordinates `X_uv` and `X_vu` as the same parity, exhibiting symmetry as a property of this law rather than of the signature; and `not_indepFun_rankTwoCoupling` is **numerical** — the edge and colour-parity events coincide with probability `1/2` against a product of marginals `1/4`, which a constant edge could not achieve even though it too would be "a function of the colours". `bipartiteSuccessor : RankSuccessor rankOneRep` is the witness itself
 * `Graphon.RelIidEdgeRegression` — R4 converse (#107/#196): the **i.i.d.-edge regression** for the successor contract, a hand-built rank `2 → 3` witness over `digraphSig` that tests **staging and recovery** where the bipartite regression tested independence and symmetry. The array is keyed by a coordinate's *support*, which gives symmetry (`X_uv = X_vu`) and the empty diagonal by construction — each is still proved from a support computation, but neither requires a choice of orientation. Two things make it a regression rather than a construction. First, recovery is genuinely staged: at rank three a two-point block is decoded from the latent coordinate at its own support — carried by the rank-three array because `2 < 3` — while at rank two the same blocks are not latent-measurable at all, so the two ranks exercise opposite sides of `lower_recovers`. Second, rank-two screening is a genuine conditional-independence statement: the block reads one coordinate of the edge source and the remainder reads the others plus the whole latent array, so screening follows from **independence**, not from determinism as in the bipartite case. `iidEdgeLaw_edge_eq_half` pins the edge probability at exactly `1/2`, which rules out a *constant* block; that the block is not measurable from the old latents is a separate fact, supplied by the product independence built into the rank-two coupling. The private conditional-independence lemma is stated for abstract σ-algebras rather than for the two coordinates of a product because the ambient measure is a pushforward of a product and the current API only transports conditional independence **backward**: a source-level proof would require a new forward law-transport theorem, whereas transporting the unconditional independence needs no new theorem. `iidEdgeSuccessor : RankSuccessor rankTwoRep` is the witness itself
 * `Graphon.RelRankInjectionInvariance` — R4 converse (#107), the isolated proof risk of the pooled-latent extension gate: **joint invariance under arbitrary sortwise self-injections**. `RankRepresentation.invariant` is stated for *finitely supported permutations*, but a pooled object built cheaply through `poolVertexEquiv` needs the joint law invariant under every self-injection; `RankRepresentation.map_prodMap_restrict_self` supplies exactly that, so full mixed pooled invariance later costs no additional mathematics. The route is finite-cylinder extensionality on the **joint** space, which had no machinery before — rank one's joint invariance goes through only because the rank-one latent action is trivial. `rankLatentIndexInj`/`rankLatentReindex` extend the latent action from permutations to injections (only injectivity is used — a support keeps its cardinality); `exists_finSuppPerm_agree_on_finset` matches an injection to a finitely supported permutation on any finite tagged-vertex support; `ext_of_prod_cylinders` is the joint extensionality, rectangles of coordinate cylinders on both factors. **No finiteness/`Fintype` hypothesis beyond `RankRepresentation`'s ambient countability.** Equality is tested on *coordinate* cylinders — finitely many `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
diff --git a/Graphon/RelAustinPolling.lean b/Graphon/RelAustinPolling.lean
index ea4782b..bc42aea 100644
--- a/Graphon/RelAustinPolling.lean
+++ b/Graphon/RelAustinPolling.lean
@@ -15,8 +15,9 @@ means and will not produce canonically equal representations.
 
 ## What is Austin's here, and what is not
 
-The **construction** follows Austin (arXiv:0801.1698): a spare vertex reservoir, mixed clusters
-straddling it, and an enriched law that carries the polling data forward. `PoolVertex S s` is
+The **construction** follows Austin (arXiv:0801.1698): a spare vertex reservoir, mixed clusters —
+those not wholly original, all-spare included — and an enriched law that carries the polling data
+forward. `PoolVertex S s` is
 `Vinfinite S s ⊕ Vinfinite S s`, with `originalVertex = Sum.inl` and `poolVertex = Sum.inr`, so the
 two halves are disjoint definitionally, and a `PooledRankExtension` is invariant under the *full*
 pooled permutation family.
@@ -47,8 +48,8 @@ half — the two would overlap.
 Austin's polling data must survive into the next law; forgetting it into a bare `C.P` statement
 would discard exactly what the successor construction consumes. That data is the family of
 **mixed** clusters — pooled rank-`n` blocks that are *not wholly original* — and not merely the
-induced structure on the spare half. "Mixed" is exactly that negation: an all-spare support
-qualifies, its original part being empty and therefore proper.
+induced structure on the spare half. "Mixed" is the negation of "wholly original", so an all-spare
+support qualifies, its original part being empty and therefore proper.
 
 * `pollingClusters` — the mixed cluster observation, indexed by `MixedClusterIndex`: pooled
   rank-`n` supports containing at least one spare vertex, all-spare supports included. Each such
@@ -68,9 +69,9 @@ proper-subset data carrying no rank-`n` block.
 
 ## Scope
 
-* `[Fintype S.Srt]` is carried by the witness, matching the polling/fixing-algebra stack it is to
-  be built from. The pooled API itself remains countable-only; removing the hypothesis is a
-  separate generalization and deliberately not attempted here.
+* Only the ambient `Countable` assumptions are needed. Because the conditional independence comes
+  from the assumed screening contract rather than from a polling argument, the `Fintype S.Srt`
+  hypothesis that the fixing-algebra stack carries is not required here.
 * Rank zero is not this module's business. The successor at `n = 0` is supplied by
   `nonempty_rankRepresentation_one` together with `truncation_zero`, which is also what respects
   `stepKernel`'s deliberate lack of an `A = ∅` realization theorem.
@@ -308,9 +309,9 @@ together with the mixed clusters — that is, the auxiliary component. Not a wit
 existential factor could be taken to be the whole joint object and would make the conclusion
 vacuous.
 
-Reading the *pooled* array rather than its original part is what makes the conditioning stable
-under the permutations the peel uses; every index still has cardinality `< n`, so the latent half
-carries no rank-`n` block. -/
+The array read is the *pooled* one because `Q.screening`'s remainder contains it in full and weak
+union conditions on exactly that lower-rank factor. Every index has cardinality `< n`, so the
+latent half carries no rank-`n` block. -/
 noncomputable def pollingCond :
     EnrichedSpace S n → PooledRankLatentSpace S n × ClusterSpace S n :=
   fun q => q.2
@@ -372,7 +373,7 @@ than as a bare algebra inequality, so it records exactly which information the r
 and lets `CondIndepFun.comp` consume the screening statement directly. -/
 
 open scoped Classical in
-omit [Countable S.Rel] in
+omit [Countable S.Srt] [Countable S.Rel] in
 /-- A support in the image of the original half carries no spare vertex. -/
 theorem isRight_eq_false_of_mem_supportImage_original
     {X : Finset (Σ s : S.Srt, Vinfinite S s)} {v : Σ s : S.Srt, PoolVertex S s}
@@ -381,7 +382,7 @@ theorem isRight_eq_false_of_mem_supportImage_original
   rfl
 
 open scoped Classical in
-omit [Countable S.Rel] in
+omit [Countable S.Srt] [Countable S.Rel] in
 /-- **Separation, original against original**: distinct rank-`n` supports have distinct images,
 since `supportImage` is injective. -/
 theorem supportImage_ne_of_ne {B e : RankSupport S n} (h : B ≠ e) :
@@ -389,6 +390,7 @@ theorem supportImage_ne_of_ne {B e : RankSupport S n} (h : B ≠ e) :
   fun heq => h (Subtype.ext (supportImage_injective _ heq))
 
 open scoped Classical in
+omit [Countable S.Srt] [Countable S.Rel] in
 /-- **Separation, cluster against original**: a mixed cluster carries a spare vertex, while the
 image of an original support is wholly original. -/
 theorem mixedCluster_ne_supportImage (Ac : MixedClusterIndex S n) (e : RankSupport S n) :
@@ -424,6 +426,7 @@ noncomputable def restToPollingData (e : RankSupport S n) (F : Finset (RankSuppo
         · rw [c.2]; exact mixedCluster_ne_supportImage Ac e⟩))
 
 open scoped Classical in
+omit [Countable S.Srt] [Countable S.Rel] in
 theorem measurable_restToPollingData (e : RankSupport S n) (F : Finset (RankSupport S n))
     (heF : e ∉ F) : Measurable (restToPollingData e F heF) :=
   (measurable_pi_lambda _ fun _ => measurable_pi_lambda _ fun _ => measurable_fst.eval).prodMk
@@ -431,6 +434,7 @@ theorem measurable_restToPollingData (e : RankSupport S n) (F : Finset (RankSupp
       (measurable_pi_lambda _ fun _ => measurable_pi_lambda _ fun _ => measurable_fst.eval))
 
 open scoped Classical in
+omit [Countable S.Srt] [Countable S.Rel] in
 /-- **The exact factorization.** Both the accumulated blocks and the polling conditioning are
 functions of the screening remainder, on the nose. -/
 theorem restToPollingData_comp (e : RankSupport S n) (F : Finset (RankSupport S n)) (heF : e ∉ F) :
@@ -569,7 +573,7 @@ private theorem iCondIndepFun_comp {Ω : Type*} [mΩ : MeasurableSpace Ω] [Stan
   Kernel.iIndepFun.comp h φ hφ
 
 open scoped Classical in
-omit [Countable S.Srt] in
+omit [Countable S.Srt] [Countable S.Rel] in
 /-- **The block codomains agree, exactly.** Reading a block of the restricted original structure is
 reading the pooled block at the image support and transporting along `blockSpaceCongr`. -/
 theorem enrichedBlock_comp_enrichedPollingMap (A : RankSupport S n) :
@@ -634,8 +638,6 @@ private theorem iCondIndepFun_of_map {α β : Type*} {m' : MeasurableSpace β}
 
 /-! ### The witness -/
 
-variable [Fintype S.Srt]
-
 /-- **The polling conclusion**: mutual conditional independence of the *entire* rank-`n` block
 family of the original structure, given the pooled latents and the mixed clusters, under the
 enriched law.
@@ -657,7 +659,7 @@ open scoped Classical in
 probability content is `iCondIndepFun_originalBlock_sourcePollingCond`, and this constructor only
 moves it along `enrichedPollingMap`, matching the block codomains by `blockSpaceCongr` and the
 conditioning algebra by the named identity. -/
-noncomputable def pooledPollingWitness {C : M.RankRepresentation n} (Q : PooledRankExtension C) :
+theorem pooledPollingWitness {C : M.RankRepresentation n} (Q : PooledRankExtension C) :
     PooledPollingWitness C Q where
   mutualCondIndep := by
     haveI := C.isProbabilityMeasure_P

From a2ddf5318d19c466f46b1da0f6c1e382e4d93310 Mon Sep 17 00:00:00 2001
From: Cameron Freer <cameronfreer@gmail.com>
Date: Wed, 26 Aug 2026 02:26:21 +0000
Subject: [PATCH 13/13] docs: name the pooled latent array in every
 enriched-law summary (#197)

Three residues from the widening that carried the pooled rank-`n` latent array into
the enriched data. The `EnrichedSpace` docstring and `pollingCond`'s rationale were
updated at the time; these summaries of the same objects were not:

* `pollingCond` is the whole pooled rank-`n` latent array together with the clusters,
  not the old latents;
* the enriched-law summaries in the module header, on `enrichedPollingLaw`, and in
  the `Graphon.lean` entry now name the pooled array alongside the clusters;
* `Set.biInter_insert` corrected to `Finset.set_biInter_insert` in the insertion
  identity's docstring.

No statement or proof changes.

Gates: lake build clean (3409 jobs), census + axiom audit pass, zero sorries, no
warnings.
---
 Graphon.lean                  |  2 +-
 Graphon/RelAustinPolling.lean | 19 ++++++++++---------
 2 files changed, 11 insertions(+), 10 deletions(-)

diff --git a/Graphon.lean b/Graphon.lean
index 65363e1..727e043 100644
--- a/Graphon.lean
+++ b/Graphon.lean
@@ -274,7 +274,7 @@ in Lean 4 using Mathlib.
 * `Graphon.RelPooledAcceptance` — R4 converse (#107), stage 3 of the pooled-latent extension gate, organizing result: **the joint restriction theorem**. For *every* sortwise embedding `e : ∀ s, Vinfinite S s ↪ PoolVertex S s`, restricting a pooled rank extension jointly — structure and latents along the same embedding — returns the representation exactly: `Q.law.map (Prod.map (RelStructure.restrict e) (latentRestrictOver e n)) = C.P`. Being **joint** is the point: it recovers the `(X, U_{<n})` law and says strictly more than a structure-only window theorem. Proved by joint-cylinder extensionality plus finite agreement with a mixed pooled permutation — on a cylinder the combined vertex support is finite, the assignment `originalVertex v ↦ e v` there is a finite partial injection of the pooled carrier, and `exists_perm_extend_of_injOn` extends it; the full mixed invariance then absorbs the permutation, which is also what lets it be chosen independently on each sort with no finite-support or uniform-bound issue. The four route-neutral consequences follow from it: `map_snd` (the pooled latent marginal is the pooled i.i.d. source), `toStationaryExtension` (the structure marginal is a `StationaryExtension M`), `lower_recovers` (local recovery on every pooled support below rank `n`, the decoder conjugated through the local and block measurable equivalences), and `screening` (screening on every pooled support of rank `n`, a pullback through `measurePreserving_pooledJointEquiv` followed by `CondIndepFun.comp` on the codomains and `CondIndepFun.congr_cond` with `comap_measurableEquiv_comp` on the conditioning algebra — no conditional-expectation reasoning). `PooledRankExtension.map_poolVertexEquiv` is the canonical specialization; bundling that restriction as the measurable equivalence `pooledJointEquiv` and cancelling it yields **`PooledRankExtension.law_eq`, a uniqueness theorem** — every pooled rank extension *is* the cheap one. Marginals, the `StationaryExtension` structure, recovery and screening therefore transport from `C.P` through one canonical law identity rather than requiring separate measure arguments
 * `Graphon.RelRankSuccessorContract` — R4 converse (#107), **interface only**: the shared witness both successor constructions must produce, and the two identically typed statements they target. `RankSuccessor C` carries the next representation together with **exact truncation compatibility**, `next.P.map (Prod.map id (rankLatentProjection (Nat.le_succ n))) = C.P` — the observable that makes the statement mention `C` at all. A theorem returning merely `Nonempty (RankRepresentation (n + 1))` could ignore `C` and produce an unrelated representation, which is the same underdetermination that sank the earlier shell attempt. The witness carries **no independence field** beyond `RankRepresentation`'s own, and **no equality between the two routes' outputs** is asserted — they prove one statement by different means and will not produce canonically equal representations. `AustinSuccessor` and `KallenbergSuccessor` are the same proposition by construction, so whichever lands first discharges the induction while the other remains an independent proof. Regression: `truncation_zero` shows the truncation equation is **automatic at rank zero** — the rank-zero latent cube is a single point, so both sides are determined by their structure marginals, which the representation axioms already pin, and the base case imposes nothing extra. The witness exposes no pooled carrier, so whether a construction genuinely used boundary-crossing permutations is observed by the pooled gate's `map_restrict_embedding` rather than by any final-output check here; each route's intermediate construction consumes that theorem. Adversarial examples are kept in route-independent regression modules, outside this interface
 * `Graphon.DigraphCoordSupport` — shared regression infrastructure: the support of a digraph coordinate is the pair of its endpoints, with the off-diagonal cardinality corollary, over an arbitrary vertex type. A bridge module so that the D1 carrier `Graphon.InfiniteDigraph` does not acquire a dependency on the equality-pattern layer where `RelCoord.support` lives — the same separation `Graphon.SimpleGraphDigraphBridge` maintains for `SimpleGraph`. Stated with `[DecidableEq V]` and proved by membership, because `RelCoord.support` is built classically and over a concrete carrier the natural instance is not definitionally the classical one, so an image-shaped statement would not apply at the sites that need it
-* `Graphon.RelAustinPolling` — R4 converse (#107/#197), **route A (Austin) unit 1**: pooled polling. Austin's Proposition 3.12 polls with swaps into a *spare vertex set*, and the pooled carrier is exactly that — `PoolVertex` is `Vinfinite ⊕ Vinfinite` with `originalVertex = Sum.inl` and `poolVertex = Sum.inr`, so the halves are disjoint definitionally, and the extension's invariance under the **full** pooled permutation family means the swaps carry no finite-support side condition. **The geometry is the delicate part**: the observed blocks are confined to the original half and the poll to supports containing a spare vertex, so the two families are disjoint by construction — reading the blocks through the canonical `pooledJointEquiv` instead is tempting, since it makes the transport to `C.P` exact, but it is wrong, because that bijection sends blocks across *both* summands and they would then overlap the poll. **The seam is an enriched law, not `C.P`**: Austin's polling data is the family of *mixed* clusters — those not wholly original, all-spare included — spanning the two halves, and forgetting it into a bare `C.P` statement would discard what the successor construction consumes, so `enrichedPollingLaw` retains the clusters alongside the original structure and old latents, with `enrichedPollingLaw_map_fst` recovering `C.P` exactly through `map_restrict_embedding` at the original-vertex embedding. `pollingCond` pins the conditioning concretely — the whole pooled rank-`n` latent array plus the mixed clusters — since an existential factor could be the whole joint object and make the conclusion vacuous. `PooledPollingWitness.mutualCondIndep` is `iCondIndepFun` over the **entire** rank-`n` block family: mutual, not pairwise, which is Austin's actual conclusion and what the #196 battery keeps honest. Needs only the ambient `Countable` assumptions — because the conditional independence comes from the assumed screening contract rather than from a polling argument, the `Fintype S.Srt` hypothesis the fixing-algebra stack carries is not required; rank zero is routed to `nonempty_rankRepresentation_one` with `truncation_zero`, respecting `stepKernel`'s deliberate lack of an `A = ∅` realization theorem
+* `Graphon.RelAustinPolling` — R4 converse (#107/#197), **route A (Austin) unit 1**: pooled polling. Austin's Proposition 3.12 polls with swaps into a *spare vertex set*, and the pooled carrier is exactly that — `PoolVertex` is `Vinfinite ⊕ Vinfinite` with `originalVertex = Sum.inl` and `poolVertex = Sum.inr`, so the halves are disjoint definitionally, and the extension's invariance under the **full** pooled permutation family means the swaps carry no finite-support side condition. **The geometry is the delicate part**: the observed blocks are confined to the original half and the poll to supports containing a spare vertex, so the two families are disjoint by construction — reading the blocks through the canonical `pooledJointEquiv` instead is tempting, since it makes the transport to `C.P` exact, but it is wrong, because that bijection sends blocks across *both* summands and they would then overlap the poll. **The seam is an enriched law, not `C.P`**: Austin's polling data is the family of *mixed* clusters — those not wholly original, all-spare included — spanning the two halves, and forgetting it into a bare `C.P` statement would discard what the successor construction consumes, so `enrichedPollingLaw` retains the whole pooled rank-`n` latent array and the clusters alongside the original structure and old latents, with `enrichedPollingLaw_map_fst` recovering `C.P` exactly through `map_restrict_embedding` at the original-vertex embedding. `pollingCond` pins the conditioning concretely — the whole pooled rank-`n` latent array plus the mixed clusters — since an existential factor could be the whole joint object and make the conclusion vacuous. `PooledPollingWitness.mutualCondIndep` is `iCondIndepFun` over the **entire** rank-`n` block family: mutual, not pairwise, which is Austin's actual conclusion and what the #196 battery keeps honest. Needs only the ambient `Countable` assumptions — because the conditional independence comes from the assumed screening contract rather than from a polling argument, the `Fintype S.Srt` hypothesis the fixing-algebra stack carries is not required; rank zero is routed to `nonempty_rankRepresentation_one` with `truncation_zero`, respecting `stepKernel`'s deliberate lack of an `A = ∅` realization theorem
 * `Graphon.RelBipartiteRegression` — R4 converse (#107/#196): the **bipartite regression** for the successor contract, a hand-built rank `1 → 2` witness over `digraphSig` whose purpose is to test that `RankSuccessor` is an expressive specification *before* either route is attempted. Each vertex carries an i.i.d. colour on its own fresh singleton coordinate and the edge is the parity, so the diagonal is constantly `false` for free. Three independent things make it a regression rather than a construction: the array law is defined **from the fresh singleton layer alone** and the rank-one coupling as the independent product `bipartiteLaw × rankLatentSource 1`, so `rankTwoCoupling_truncation` compares two separately described couplings and genuinely consumes the source factorization; the rank-two block decoder recovers **both** directed coordinates `X_uv` and `X_vu` as the same parity, exhibiting symmetry as a property of this law rather than of the signature; and `not_indepFun_rankTwoCoupling` is **numerical** — the edge and colour-parity events coincide with probability `1/2` against a product of marginals `1/4`, which a constant edge could not achieve even though it too would be "a function of the colours". `bipartiteSuccessor : RankSuccessor rankOneRep` is the witness itself
 * `Graphon.RelIidEdgeRegression` — R4 converse (#107/#196): the **i.i.d.-edge regression** for the successor contract, a hand-built rank `2 → 3` witness over `digraphSig` that tests **staging and recovery** where the bipartite regression tested independence and symmetry. The array is keyed by a coordinate's *support*, which gives symmetry (`X_uv = X_vu`) and the empty diagonal by construction — each is still proved from a support computation, but neither requires a choice of orientation. Two things make it a regression rather than a construction. First, recovery is genuinely staged: at rank three a two-point block is decoded from the latent coordinate at its own support — carried by the rank-three array because `2 < 3` — while at rank two the same blocks are not latent-measurable at all, so the two ranks exercise opposite sides of `lower_recovers`. Second, rank-two screening is a genuine conditional-independence statement: the block reads one coordinate of the edge source and the remainder reads the others plus the whole latent array, so screening follows from **independence**, not from determinism as in the bipartite case. `iidEdgeLaw_edge_eq_half` pins the edge probability at exactly `1/2`, which rules out a *constant* block; that the block is not measurable from the old latents is a separate fact, supplied by the product independence built into the rank-two coupling. The private conditional-independence lemma is stated for abstract σ-algebras rather than for the two coordinates of a product because the ambient measure is a pushforward of a product and the current API only transports conditional independence **backward**: a source-level proof would require a new forward law-transport theorem, whereas transporting the unconditional independence needs no new theorem. `iidEdgeSuccessor : RankSuccessor rankTwoRep` is the witness itself
 * `Graphon.RelRankInjectionInvariance` — R4 converse (#107), the isolated proof risk of the pooled-latent extension gate: **joint invariance under arbitrary sortwise self-injections**. `RankRepresentation.invariant` is stated for *finitely supported permutations*, but a pooled object built cheaply through `poolVertexEquiv` needs the joint law invariant under every self-injection; `RankRepresentation.map_prodMap_restrict_self` supplies exactly that, so full mixed pooled invariance later costs no additional mathematics. The route is finite-cylinder extensionality on the **joint** space, which had no machinery before — rank one's joint invariance goes through only because the rank-one latent action is trivial. `rankLatentIndexInj`/`rankLatentReindex` extend the latent action from permutations to injections (only injectivity is used — a support keeps its cardinality); `exists_finSuppPerm_agree_on_finset` matches an injection to a finitely supported permutation on any finite tagged-vertex support; `ext_of_prod_cylinders` is the joint extensionality, rectangles of coordinate cylinders on both factors. **No finiteness/`Fintype` hypothesis beyond `RankRepresentation`'s ambient countability.** Equality is tested on *coordinate* cylinders — finitely many `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
diff --git a/Graphon/RelAustinPolling.lean b/Graphon/RelAustinPolling.lean
index bc42aea..5f1dae3 100644
--- a/Graphon/RelAustinPolling.lean
+++ b/Graphon/RelAustinPolling.lean
@@ -56,14 +56,15 @@ support qualifies, its original part being empty and therefore proper.
   support has a *proper* original part, since at least one of its `n` vertices is spare; for an
   all-spare support that part is empty, which is proper as well.
 * `enrichedPollingLaw` — the pushforward of `Q.law` retaining the original structure and old
-  latents together with the clusters.
+  latents together with the auxiliary polling data: the whole pooled rank-`n` latent array and the
+  clusters.
 * `enrichedPollingLaw_map_fst` — the first marginal is `C.P` exactly, proved through
   `Q.map_restrict_embedding (originalVertex S)`. The gate theorem is a compiled dependency here,
   not a citation.
 
-The conditioning is pinned by `pollingCond`: the old latents together with the clusters. It is a
-definition rather than a witness field, because an existential conditioning factor could be taken
-to be the whole joint object and would make the conclusion vacuous. Every index of
+The conditioning is pinned by `pollingCond`: the whole pooled rank-`n` latent array together with
+the clusters. It is a definition rather than a witness field, because an existential conditioning
+factor could be taken to be the whole joint object and would make the conclusion vacuous. Every index of
 `RankLatentIndex S n` has cardinality `< n`, so the latent half of the conditioning is
 proper-subset data carrying no rank-`n` block.
 
@@ -275,9 +276,9 @@ theorem measurable_enrichedPollingMap : Measurable (enrichedPollingMap (S := S)
       (measurable_snd.prodMk measurable_pollingClusters)
 
 open scoped Classical in
-/-- **The enriched polling law.** Austin's polling data survives here: the clusters are retained
-alongside the original structure and old latents, rather than being forgotten into a bare `C.P`
-statement. -/
+/-- **The enriched polling law.** Austin's polling data survives here: the whole pooled rank-`n`
+latent array and the clusters are retained alongside the original structure and old latents, rather
+than being forgotten into a bare `C.P` statement. -/
 noncomputable def enrichedPollingLaw {C : M.RankRepresentation n} (Q : PooledRankExtension C) :
     Measure (EnrichedSpace S n) :=
   (Q.law : Measure (RelStructure S (PoolVertex S) × PooledRankLatentSpace S n)).map
@@ -463,8 +464,8 @@ The peel step, assembled from the pieces above: `Q.screening` at the original im
 remainder pushed through `restToPollingData`, `comap_prodMk` to split the resulting algebra into
 the accumulated blocks joined with the polling conditioning, and weak union to drop back to the
 polling conditioning alone. Stated as a direct conditional-expectation identity so that it feeds
-`Finset.induction_on` with `Set.biInter_insert` and `Finset.prod_insert`, without any dependent
-tuple reindexing inside the induction. -/
+`Finset.induction_on` with `Finset.set_biInter_insert` and `Finset.prod_insert`, without any
+dependent tuple reindexing inside the induction. -/
 
 open scoped Classical in
 private theorem polling_condExp_insert {C : M.RankRepresentation n} (Q : PooledRankExtension C)