From a4b3c33c78ff662f3aed3d2804af9e4950bce9e2 Mon Sep 17 00:00:00 2001
From: Cameron Freer <cameronfreer@gmail.com>
Date: Fri, 28 Aug 2026 00:21:26 +0000
Subject: [PATCH 1/5] =?UTF-8?q?feat:=20the=20Austin=20base=20and=20its=20a?=
 =?UTF-8?q?ction=20=E2=80=94=20unit=202=20law-free=20checkpoint=20(#197)?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Fixes the action and proves it **strict** before any bundle, kernel or
conditional-distribution statement is written. Equivariance cannot be repaired
downstream, so it is established first.

`AustinBaseSpace = PooledRankLatentSpace × ClusterSpace` is the equivariant
lower-rank base over which the enriched kernel will be built — not fresh rank-`n`
coordinates and not relational data. Every pooled latent index has cardinality
`< n`, so it carries no rank-`n` block.

All five required results:

* `mixedClusterLift` with `_one` and `_mul`. `poolLift` acts on the original half and
  fixes the spare half; its preservation of `Sum.isRight` is what keeps mixed
  clusters mixed, all-spare ones included.
* `austinBaseRelabel_one` and `_mul` as exact **function equalities**, in the
  **contravariant** orientation `austinBaseRelabel (σ * τ) = austinBaseRelabel τ ∘
  austinBaseRelabel σ`. The orientation is forced by `Equiv.trans` applying its first
  argument first, and is stated explicitly so it is not re-derived wrongly.
* `enrichedPollingMap_naturality` — **one square for all four components**: structure
  and pooled latents definitionally, clusters by `pollingClusters_relabel` (itself
  `rfl`), original latents by the split corollary `restrictOriginalLatents_sumCongr`.
* `enrichedPollingLaw_map_enrichedAction` — exact invariance, derived from
  `Measure.map_map`, that square, and `Q.invariant` alone. No almost-everywhere
  reasoning and no component rewriting appear in it.
* `StandardBorelSpace` **inferred** for `AustinBaseSpace`, `EnrichedLowerSpace` and
  `EnrichedBoundarySpace`. The adapter spaces take an arbitrary coherent basis, so no
  `Fintype S.Srt` enters.

The dependent cluster fibres are handled by `Bool`-valued pointwise bridges, with the
single required cast isolated in one private lemma. Marking `MixedClusterIndex`
reducible would also have worked but was rejected: unlike the compatibility aliases
elsewhere in the repository it is a substantive subtype, and exposing its
implementation globally to solve a local elaboration problem is too broad.

Lean note: `rankLatentRelabel` and `latentRelabelOver` are not interchangeable at
face value; the split corollary is carrier-parametric, so the square bridges them
with `rankLatentRelabel_eq_latentRelabelOver`.

Audit 433 → 437. Gates: lake build clean (3410 jobs), census + axiom audit pass, zero
sorries, no warnings.
---
 Graphon.lean                       |   2 +
 Graphon/RelAustinEnriched.lean     | 428 +++++++++++++++++++++++++++++
 scripts/axiom_audit.lean           |   6 +
 scripts/check_census_and_axioms.py |   4 +
 4 files changed, 440 insertions(+)
 create mode 100644 Graphon/RelAustinEnriched.lean

diff --git a/Graphon.lean b/Graphon.lean
index 727e043..26d2e8f 100644
--- a/Graphon.lean
+++ b/Graphon.lean
@@ -49,6 +49,7 @@ import Graphon.RelPooledLatents
 import Graphon.RelPooledExtension
 import Graphon.RelPooledAcceptance
 import Graphon.RelAustinPolling
+import Graphon.RelAustinEnriched
 import Graphon.RelRankSuccessorContract
 import Graphon.DigraphCoordSupport
 import Graphon.RelBipartiteRegression
@@ -274,6 +275,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.RelAustinEnriched` — R4 converse (#107/#197), **route A (Austin) unit 2**, law-free checkpoint: the Austin base and its action. `AustinBaseSpace = PooledRankLatentSpace × ClusterSpace` is the **equivariant lower-rank base** over which the enriched kernel is later built — not fresh rank-`n` coordinates and not relational data; every pooled latent index has cardinality `< n`, so it carries no rank-`n` block. `poolLift` acts on the original half and fixes the spare half, and its preservation of `Sum.isRight` is what keeps mixed clusters mixed. **The orientation is contravariant** — `Equiv.trans` applies its first argument first, so `austinBaseRelabel (σ * τ) = austinBaseRelabel τ ∘ austinBaseRelabel σ`. `enrichedPollingMap_naturality` is **one square for all four components**: structure and pooled latents definitionally, clusters by `pollingClusters_relabel`, original latents by the split corollary `restrictOriginalLatents_sumCongr`; and `enrichedPollingLaw_map_enrichedAction` derives exact invariance from it with nothing but `Measure.map_map` and the extension's own invariance — no almost-everywhere step. The dependent cluster fibres are handled by `Bool`-valued pointwise bridges, with the single required cast isolated in one private lemma rather than by weakening `MixedClusterIndex`'s reducibility, which would expose a substantive subtype's implementation globally to solve a local elaboration problem
 * `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
diff --git a/Graphon/RelAustinEnriched.lean b/Graphon/RelAustinEnriched.lean
new file mode 100644
index 0000000..07cfe1c
--- /dev/null
+++ b/Graphon/RelAustinEnriched.lean
@@ -0,0 +1,428 @@
+/-
+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.RelAustinPolling
+import Graphon.RelLowerFactor
+import Graphon.RelFactorLaws
+import Graphon.RelRankSuccessor
+
+/-!
+# The Austin base and its action: unit 2, law-free checkpoint (R4 converse, #107, #197)
+
+Route **A** (Austin) only. No Kallenberg machinery, and nothing here asserts that the two routes'
+outputs agree.
+
+The **auxiliary base** carried alongside the representation is
+`AustinBaseSpace S n = PooledRankLatentSpace S n × ClusterSpace S n`: the pooled lower-rank latents
+together with the mixed clusters. It is the equivariant lower-rank base over which the enriched
+kernel will later be built — not a family of fresh rank-`n` coordinates, and not relational data.
+Every pooled latent index has cardinality `< n`, so the base carries no rank-`n` block.
+
+This module is deliberately **law-free apart from one invariance**: it fixes the action and proves
+it strict, before any bundle, kernel, or conditional-distribution statement is written.
+Equivariance cannot be repaired downstream, so it is established first.
+
+## Contents
+
+* `poolLift` — the split lift of a finitely supported relabeling: act on the original half, fix
+  the spare half. Its `Sum.isRight` preservation is what keeps mixed clusters mixed.
+* `mixedClusterLift`, with identity and composition laws — the induced permutation of the cluster
+  index.
+* `austinBaseRelabel`, with identity and composition laws as **function equalities** — the action
+  on the base. A pinned definition, not an opaque structure field.
+* `enrichedPollingMap_naturality` — **one global square** covering the structure, the original
+  latents, the pooled latents and the clusters simultaneously. Stated generically in the cluster
+  index, so genuinely mixed and all-spare indices are both covered.
+* `enrichedPollingLaw_map_austinBaseRelabel` — exact invariance of the pushed enriched law,
+  derived from that square together with the extension's own invariance.
+
+The adapter spaces `EnrichedLowerSpace` and `EnrichedBoundarySpace` are introduced here only so
+that their standard-Borel structure is available; their maps and commuting laws belong to the
+bundle that follows.
+-/
+
+open MeasureTheory ProbabilityTheory
+
+namespace RelSignature
+
+namespace InfiniteRelExchangeableLaw
+
+variable {S : RelSignature} [Countable S.Srt] [Countable S.Rel]
+  {M : InfiniteRelExchangeableLaw S} {n : ℕ}
+
+/-! ### The auxiliary base -/
+
+variable (S n) in
+/-- **The Austin base**: pooled lower-rank latents together with the mixed clusters. The
+equivariant lower-rank base of the construction; it carries no rank-`n` block, since every pooled
+latent index has cardinality `< n` and every cluster index carries a spare vertex. -/
+abbrev AustinBaseSpace := PooledRankLatentSpace S n × ClusterSpace S n
+
+instance : StandardBorelSpace (AustinBaseSpace S n) := inferInstance
+
+/-! ### The split lift -/
+
+/-- **The split lift** of a finitely supported relabeling: act on the original half, fix the spare
+half. Restricting to split permutations is what makes the original-latent component natural; a
+boundary-crossing permutation has no such law. -/
+def poolLift (σ : FinSuppPerm S) : ∀ s, Equiv.Perm (PoolVertex S s) :=
+  fun s => Equiv.sumCongr (σ.1 s) (Equiv.refl _)
+
+omit [Countable S.Srt] [Countable S.Rel] in
+/-- The split lift preserves the spare half, which is what keeps mixed clusters mixed. -/
+@[simp] theorem isRight_poolLift (σ : FinSuppPerm S) (s : S.Srt) (x : PoolVertex S s) :
+    Sum.isRight (poolLift σ s x) = Sum.isRight x := by
+  cases x <;> rfl
+
+omit [Countable S.Srt] [Countable S.Rel] in
+@[simp] theorem poolLift_one (s : S.Srt) :
+    poolLift (S := S) 1 s = Equiv.refl _ :=
+  Equiv.ext fun x => by cases x <;> rfl
+
+omit [Countable S.Srt] [Countable S.Rel] in
+theorem poolLift_mul (σ τ : FinSuppPerm S) (s : S.Srt) :
+    poolLift (σ * τ) s = poolLift σ s * poolLift τ s :=
+  Equiv.ext fun x => by cases x <;> rfl
+
+/-! ### The induced action on cluster indices -/
+
+open scoped Classical in
+omit [Countable S.Srt] [Countable S.Rel] in
+/-- Round trip of the split lift on supports, proved by membership so that no `DecidableEq`
+instance enters the statement. -/
+private theorem supportImage_poolLift_inv (σ : FinSuppPerm S)
+    (A : Finset (Σ s : S.Srt, PoolVertex S s)) :
+    supportImage (fun s => (poolLift σ⁻¹ s).toEmbedding)
+      (supportImage (fun s => (poolLift σ s).toEmbedding) A) = A := by
+  have hx : ∀ (s : S.Srt) (x : PoolVertex S s), poolLift σ⁻¹ s (poolLift σ s x) = x := by
+    intro s x
+    rw [show poolLift σ⁻¹ s (poolLift σ s x) = (poolLift σ⁻¹ s * poolLift σ s) x from rfl,
+      ← poolLift_mul]
+    simp
+  refine Finset.ext fun v => ?_
+  rw [mem_supportImage_iff]
+  constructor
+  · rintro ⟨w, hw, rfl⟩
+    rw [mem_supportImage_iff] at hw
+    obtain ⟨u, hu, rfl⟩ := hw
+    obtain ⟨s, x⟩ := u
+    show (⟨s, poolLift σ⁻¹ s (poolLift σ s x)⟩ : Σ s : S.Srt, PoolVertex S s) ∈ A
+    rw [hx]
+    exact hu
+  · intro hv
+    obtain ⟨s, x⟩ := v
+    refine ⟨Sigma.map id (fun s => ⇑(poolLift σ s)) ⟨s, x⟩,
+      (mem_supportImage_iff _ _ _).mpr ⟨⟨s, x⟩, hv, rfl⟩, ?_⟩
+    show (⟨s, poolLift σ⁻¹ s (poolLift σ s x)⟩ : Σ s : S.Srt, PoolVertex S s) = ⟨s, x⟩
+    rw [hx]
+
+open scoped Classical in
+/-- **The split lift permutes the mixed cluster indices**: it preserves cardinality, and preserves
+the presence of a spare vertex, so a mixed index stays mixed — including the all-spare ones. -/
+noncomputable def mixedClusterLift (σ : FinSuppPerm S) (n : ℕ) :
+    MixedClusterIndex S n ≃ MixedClusterIndex S n where
+  toFun A := ⟨supportImage (fun s => (poolLift σ s).toEmbedding) A.1, by
+    refine ⟨by rw [card_supportImage]; exact A.2.1, ?_⟩
+    obtain ⟨v, hv, hvr⟩ := A.2.2
+    exact ⟨Sigma.map id (fun s => ⇑(poolLift σ s)) v,
+      (mem_supportImage_iff _ _ _).mpr ⟨v, hv, rfl⟩, by
+        rw [show (Sigma.map id (fun s => ⇑(poolLift σ s)) v).2 = poolLift σ v.1 v.2 from rfl,
+          isRight_poolLift]
+        exact hvr⟩⟩
+  invFun A := ⟨supportImage (fun s => (poolLift σ⁻¹ s).toEmbedding) A.1, by
+    refine ⟨by rw [card_supportImage]; exact A.2.1, ?_⟩
+    obtain ⟨v, hv, hvr⟩ := A.2.2
+    exact ⟨Sigma.map id (fun s => ⇑(poolLift σ⁻¹ s)) v,
+      (mem_supportImage_iff _ _ _).mpr ⟨v, hv, rfl⟩, by
+        rw [show (Sigma.map id (fun s => ⇑(poolLift σ⁻¹ s)) v).2 = poolLift σ⁻¹ v.1 v.2 from rfl,
+          isRight_poolLift]
+        exact hvr⟩⟩
+  left_inv A := Subtype.ext (supportImage_poolLift_inv σ A.1)
+  right_inv A := Subtype.ext (by
+    have h := supportImage_poolLift_inv σ⁻¹ A.1
+    rwa [inv_inv] at h)
+
+open scoped Classical in
+omit [Countable S.Srt] [Countable S.Rel] in
+@[simp] theorem mixedClusterLift_coe (σ : FinSuppPerm S) (n : ℕ) (A : MixedClusterIndex S n) :
+    (mixedClusterLift σ n A).1 = supportImage (fun s => (poolLift σ s).toEmbedding) A.1 := rfl
+
+open scoped Classical in
+omit [Countable S.Srt] [Countable S.Rel] in
+private theorem supportImage_poolLift_one (A : Finset (Σ s : S.Srt, PoolVertex S s)) :
+    supportImage (fun s => (poolLift (S := S) 1 s).toEmbedding) A = A := by
+  refine Finset.ext fun v => ?_
+  rw [mem_supportImage_iff]
+  constructor
+  · rintro ⟨w, hw, rfl⟩
+    obtain ⟨s, x⟩ := w
+    show (⟨s, poolLift (S := S) 1 s x⟩ : Σ s : S.Srt, PoolVertex S s) ∈ A
+    rw [poolLift_one]
+    exact hw
+  · intro hv
+    obtain ⟨s, x⟩ := v
+    refine ⟨⟨s, x⟩, hv, ?_⟩
+    show (⟨s, poolLift (S := S) 1 s x⟩ : Σ s : S.Srt, PoolVertex S s) = ⟨s, x⟩
+    rw [poolLift_one]
+    rfl
+
+open scoped Classical in
+omit [Countable S.Srt] [Countable S.Rel] in
+private theorem supportImage_poolLift_mul (σ τ : FinSuppPerm S)
+    (A : Finset (Σ s : S.Srt, PoolVertex S s)) :
+    supportImage (fun s => (poolLift (σ * τ) s).toEmbedding) A =
+      supportImage (fun s => (poolLift σ s).toEmbedding)
+        (supportImage (fun s => (poolLift τ s).toEmbedding) A) := by
+  refine Finset.ext fun v => ?_
+  rw [mem_supportImage_iff, mem_supportImage_iff]
+  constructor
+  · rintro ⟨w, hw, rfl⟩
+    obtain ⟨s, x⟩ := w
+    refine ⟨Sigma.map id (fun s => ⇑(poolLift τ s)) ⟨s, x⟩,
+      (mem_supportImage_iff _ _ _).mpr ⟨⟨s, x⟩, hw, rfl⟩, ?_⟩
+    show (⟨s, poolLift σ s (poolLift τ s x)⟩ : Σ s : S.Srt, PoolVertex S s) =
+      ⟨s, poolLift (σ * τ) s x⟩
+    rw [poolLift_mul]
+    rfl
+  · rintro ⟨w, hw, rfl⟩
+    rw [mem_supportImage_iff] at hw
+    obtain ⟨u, hu, rfl⟩ := hw
+    obtain ⟨s, x⟩ := u
+    refine ⟨⟨s, x⟩, hu, ?_⟩
+    show (⟨s, poolLift (σ * τ) s x⟩ : Σ s : S.Srt, PoolVertex S s) =
+      ⟨s, poolLift σ s (poolLift τ s x)⟩
+    rw [poolLift_mul]
+    rfl
+
+open scoped Classical in
+omit [Countable S.Srt] [Countable S.Rel] in
+@[simp] theorem mixedClusterLift_one (n : ℕ) :
+    mixedClusterLift (S := S) 1 n = Equiv.refl _ :=
+  Equiv.ext fun A => Subtype.ext (supportImage_poolLift_one A.1)
+
+open scoped Classical in
+omit [Countable S.Srt] [Countable S.Rel] in
+theorem mixedClusterLift_mul (σ τ : FinSuppPerm S) (n : ℕ) :
+    mixedClusterLift (S := S) (σ * τ) n =
+      (mixedClusterLift τ n).trans (mixedClusterLift σ n) :=
+  Equiv.ext fun A => Subtype.ext (supportImage_poolLift_mul σ τ A.1)
+
+/-! ### The action on the base -/
+
+open scoped Classical in
+/-- **The action on the Austin base**: the pooled latents move by the split lift, and each cluster
+coordinate is re-read at the moved index and transported by `blockSpaceCongr`. A pinned definition
+rather than an opaque field, so its laws are checkable. -/
+noncomputable def austinBaseRelabel (σ : FinSuppPerm S) (n : ℕ) :
+    AustinBaseSpace S n → AustinBaseSpace S n :=
+  fun z => (pooledRankLatentRelabel (poolLift σ) n z.1,
+    fun A => blockSpaceCongr (fun s => (poolLift σ s).toEmbedding) A.1
+      (z.2 (mixedClusterLift σ n A)))
+
+open scoped Classical in
+omit [Countable S.Srt] [Countable S.Rel] in
+theorem measurable_austinBaseRelabel (σ : FinSuppPerm S) (n : ℕ) :
+    Measurable (austinBaseRelabel (S := S) σ n) :=
+  ((pooledRankLatentRelabel (poolLift σ) n).measurable.comp measurable_fst).prodMk
+    (measurable_pi_lambda _ fun A =>
+      (blockSpaceCongr (fun s => (poolLift σ s).toEmbedding) A.1).measurable.comp
+        (measurable_snd.eval))
+
+/-! ### The laws of the action
+
+Note the **orientation**: `pooledRankLatentRelabel_comp` is contravariant (`Equiv.trans f g` applies
+`f` first), so the action composes as `austinBaseRelabel (σ * τ) = austinBaseRelabel τ ∘
+austinBaseRelabel σ`. -/
+
+open scoped Classical in
+omit [Countable S.Srt] [Countable S.Rel] in
+/-- **Pointwise cluster naturality**: relabeling the pooled structure and reading a cluster
+coordinate is reading the moved cluster at the moved coordinate. Stated at the block coordinate so
+that no fibre transport appears in the statement, and generically in the cluster index, so
+genuinely mixed and all-spare indices are covered alike. -/
+theorem pollingClusters_relabel (σ : FinSuppPerm S)
+    (p : RelStructure S (PoolVertex S) × PooledRankLatentSpace S n)
+    (A : MixedClusterIndex S n) (c : BlockIndexOver (PoolVertex S) A.1) :
+    pollingClusters (Prod.map (RelStructure.relabel (poolLift σ))
+        (pooledRankLatentRelabel (poolLift σ) n) p) A c =
+      pollingClusters p (mixedClusterLift σ n A)
+        (blockIndexCongr (fun s => (poolLift σ s).toEmbedding) A.1 c) := rfl
+
+open scoped Classical in
+omit [Countable S.Srt] [Countable S.Rel] in
+/-- **The one cast this development needs.** Reading a cluster coordinate at equal indices, with
+the fibres identified by substituting the index equality and the coordinates compared as raw
+relation coordinates. Isolated here deliberately: the alternative — weakening
+`MixedClusterIndex`'s reducibility — would expose a substantive subtype's implementation globally
+in order to solve a local elaboration problem. -/
+private theorem cluster_eval_congr (z : ClusterSpace S n) {A B : MixedClusterIndex S n}
+    (hAB : A = B) {c : BlockIndexOver (PoolVertex S) A.1}
+    {d : BlockIndexOver (PoolVertex S) B.1} (hcd : (c.1 : RelCoord S (PoolVertex S)) = d.1) :
+    z A c = z B d := by
+  subst hAB
+  exact congrArg (z A) (Subtype.ext hcd)
+
+open scoped Classical in
+omit [Countable S.Srt] [Countable S.Rel] in
+/-- Pointwise evaluation of the base action on a cluster coordinate: a `Bool`-valued identity, so
+no dependent fibre appears. The bridge through which the function-level laws are proved. -/
+theorem austinBaseRelabel_apply_cluster (σ : FinSuppPerm S) (n : ℕ) (z : AustinBaseSpace S n)
+    (A : MixedClusterIndex S n) (c : BlockIndexOver (PoolVertex S) A.1) :
+    (austinBaseRelabel σ n z).2 A c =
+      z.2 (mixedClusterLift σ n A)
+        (blockIndexCongr (fun s => (poolLift σ s).toEmbedding) A.1 c) := rfl
+
+open scoped Classical in
+omit [Countable S.Srt] [Countable S.Rel] in
+/-- **Identity law**, pointwise. -/
+theorem austinBaseRelabel_apply_cluster_one (n : ℕ) (z : AustinBaseSpace S n)
+    (A : MixedClusterIndex S n) (c : BlockIndexOver (PoolVertex S) A.1) :
+    (austinBaseRelabel (S := S) 1 n z).2 A c = z.2 A c := by
+  rw [austinBaseRelabel_apply_cluster]
+  refine cluster_eval_congr z.2 (Subtype.ext (supportImage_poolLift_one A.1)) ?_
+  show RelCoord.map (fun s => ⇑(poolLift (S := S) 1 s)) c.1 = c.1
+  rw [show poolLift (S := S) 1 = fun _ => 1 from funext fun s => by rw [poolLift_one]; rfl]
+  rfl
+
+open scoped Classical in
+omit [Countable S.Srt] [Countable S.Rel] in
+/-- **Composition law**, pointwise, in the contravariant orientation forced by
+`pooledRankLatentRelabel_comp`. -/
+theorem austinBaseRelabel_apply_cluster_mul (σ τ : FinSuppPerm S) (n : ℕ)
+    (z : AustinBaseSpace S n) (A : MixedClusterIndex S n)
+    (c : BlockIndexOver (PoolVertex S) A.1) :
+    (austinBaseRelabel (S := S) (σ * τ) n z).2 A c =
+      (austinBaseRelabel τ n (austinBaseRelabel σ n z)).2 A c := by
+  rw [austinBaseRelabel_apply_cluster, austinBaseRelabel_apply_cluster,
+    austinBaseRelabel_apply_cluster]
+  refine cluster_eval_congr z.2 (Subtype.ext (supportImage_poolLift_mul σ τ A.1)) ?_
+  show RelCoord.map (fun s => ⇑(poolLift (σ * τ) s)) c.1 =
+    RelCoord.map (fun s => ⇑(poolLift σ s)) (RelCoord.map (fun s => ⇑(poolLift τ s)) c.1)
+  rw [show (fun s => ⇑(poolLift (σ * τ) s)) =
+      (fun s x => poolLift σ s (poolLift τ s x)) from
+    funext fun s => funext fun x => by rw [poolLift_mul]; rfl]
+  rfl
+
+/-! ### The function-level laws -/
+
+open scoped Classical in
+omit [Countable S.Srt] [Countable S.Rel] in
+@[simp] theorem austinBaseRelabel_one (n : ℕ) :
+    austinBaseRelabel (S := S) 1 n = id := by
+  funext z
+  refine Prod.ext ?_ ?_
+  · show pooledRankLatentRelabel (poolLift (S := S) 1) n z.1 = z.1
+    rw [show poolLift (S := S) 1 = fun _ => 1 from funext fun s => by rw [poolLift_one]; rfl,
+      pooledRankLatentRelabel_one]
+    rfl
+  · funext A
+    funext c
+    exact austinBaseRelabel_apply_cluster_one n z A c
+
+open scoped Classical in
+omit [Countable S.Srt] [Countable S.Rel] in
+theorem austinBaseRelabel_mul (σ τ : FinSuppPerm S) (n : ℕ) :
+    austinBaseRelabel (S := S) (σ * τ) n =
+      austinBaseRelabel τ n ∘ austinBaseRelabel σ n := by
+  funext z
+  refine Prod.ext ?_ ?_
+  · show pooledRankLatentRelabel (poolLift (σ * τ)) n z.1 =
+      pooledRankLatentRelabel (poolLift τ) n (pooledRankLatentRelabel (poolLift σ) n z.1)
+    rw [show poolLift (σ * τ) = fun s => poolLift σ s * poolLift τ s from
+        funext fun s => poolLift_mul σ τ s,
+      pooledRankLatentRelabel_comp]
+    rfl
+  · funext A
+    funext c
+    exact austinBaseRelabel_apply_cluster_mul σ τ n z A c
+
+/-! ### The global naturality square, and the invariance it yields -/
+
+variable (S n) in
+open scoped Classical in
+/-- The action on the pooled objects by the split lift. -/
+noncomputable def pooledAction (σ : FinSuppPerm S) :
+    RelStructure S (PoolVertex S) × PooledRankLatentSpace S n →
+      RelStructure S (PoolVertex S) × PooledRankLatentSpace S n :=
+  Prod.map (RelStructure.relabel (poolLift σ)) (pooledRankLatentRelabel (poolLift σ) n)
+
+variable (S n) in
+open scoped Classical in
+/-- The action on the enriched objects: the representation coordinates move by `σ`, the auxiliary
+base by `austinBaseRelabel`. -/
+noncomputable def enrichedAction (σ : FinSuppPerm S) :
+    EnrichedSpace S n → EnrichedSpace S n :=
+  Prod.map (Prod.map (RelStructure.relabel σ.1) (rankLatentRelabel σ n)) (austinBaseRelabel σ n)
+
+open scoped Classical in
+omit [Countable S.Srt] [Countable S.Rel] in
+theorem measurable_enrichedAction (σ : FinSuppPerm S) (n : ℕ) :
+    Measurable (enrichedAction S n σ) :=
+  ((measurable_relabel σ.1).prodMap (rankLatentRelabel σ n).measurable).prodMap
+    (measurable_austinBaseRelabel σ n)
+
+open scoped Classical in
+omit [Countable S.Srt] [Countable S.Rel] in
+theorem measurable_pooledAction (σ : FinSuppPerm S) (n : ℕ) :
+    Measurable (pooledAction S n σ) :=
+  (measurable_relabel (poolLift σ)).prodMap (pooledRankLatentRelabel (poolLift σ) n).measurable
+
+open scoped Classical in
+omit [Countable S.Srt] [Countable S.Rel] in
+/-- **One square for all four components.** Enriching after acting on the pooled objects is acting
+on the enriched objects after enriching. The structure and pooled-latent components are
+definitional, the clusters are `pollingClusters_relabel`, and the original latents are the split
+corollary `restrictOriginalLatents_sumCongr`. An exact function equality. -/
+theorem enrichedPollingMap_naturality (σ : FinSuppPerm S) (n : ℕ) :
+    enrichedPollingMap ∘ pooledAction S n σ =
+      enrichedAction S n σ ∘ (enrichedPollingMap (S := S) (n := n)) := by
+  funext p
+  dsimp only [Function.comp_apply, enrichedAction, pooledAction, enrichedPollingMap, Prod.map]
+  refine Prod.ext (Prod.ext rfl ?_) (Prod.ext rfl ?_)
+  · have h := congrFun (restrictOriginalLatents_sumCongr σ.1 n) p.2
+    rw [rankLatentRelabel_eq_latentRelabelOver]
+    exact h
+  · funext A
+    funext c
+    exact pollingClusters_relabel σ p A c
+
+open scoped Classical in
+/-- **Exact invariance of the enriched law.** Nothing but `Measure.map_map`, the naturality square,
+and the extension's own invariance — no almost-everywhere reasoning and no component rewriting. -/
+theorem enrichedPollingLaw_map_enrichedAction {C : M.RankRepresentation n}
+    (Q : PooledRankExtension C) (σ : FinSuppPerm S) :
+    (enrichedPollingLaw Q).map (enrichedAction S n σ) = enrichedPollingLaw Q := by
+  rw [enrichedPollingLaw,
+    Measure.map_map (measurable_enrichedAction σ n) measurable_enrichedPollingMap,
+    ← enrichedPollingMap_naturality σ n,
+    ← Measure.map_map measurable_enrichedPollingMap (measurable_pooledAction σ n),
+    show (Q.law : Measure (RelStructure S (PoolVertex S) × PooledRankLatentSpace S n)).map
+        (pooledAction S n σ) = Q.law from Q.invariant (poolLift σ)]
+
+/-! ### Adapter spaces
+
+Introduced here only so that their standard-Borel structure is available and inferred rather than
+assumed; their maps and commuting laws belong to the bundle that follows. Stated for an arbitrary
+coherent basis — selecting one via `nonempty_coherentBasis` is what would introduce
+`[Fintype S.Srt]`, and that is deliberately not done here. -/
+
+/-- The lower-factor space extended by the Austin base. -/
+abbrev EnrichedLowerSpace (B : CoherentBasis M) (m : ℕ) :=
+  B.LowerFactorSpace m × AustinBaseSpace S m
+
+/-- The boundary space at `A` extended by the Austin base. -/
+abbrev EnrichedBoundarySpace (B : CoherentBasis M) (m : ℕ)
+    (A : Finset (Σ s : S.Srt, Vinfinite S s)) :=
+  B.BoundarySpace A × AustinBaseSpace S m
+
+instance (B : CoherentBasis M) (m : ℕ) :
+    StandardBorelSpace (EnrichedLowerSpace B m) := inferInstance
+
+instance (B : CoherentBasis M) (m : ℕ) (A : Finset (Σ s : S.Srt, Vinfinite S s)) :
+    StandardBorelSpace (EnrichedBoundarySpace B m A) := inferInstance
+
+end InfiniteRelExchangeableLaw
+
+end RelSignature
diff --git a/scripts/axiom_audit.lean b/scripts/axiom_audit.lean
index ae31984..6c1cdf9 100644
--- a/scripts/axiom_audit.lean
+++ b/scripts/axiom_audit.lean
@@ -347,6 +347,12 @@ 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): the Austin base and its action, unit 2 checkpoint.
+#print axioms RelSignature.InfiniteRelExchangeableLaw.austinBaseRelabel_one
+#print axioms RelSignature.InfiniteRelExchangeableLaw.austinBaseRelabel_mul
+#print axioms RelSignature.InfiniteRelExchangeableLaw.enrichedPollingMap_naturality
+#print axioms RelSignature.InfiniteRelExchangeableLaw.enrichedPollingLaw_map_enrichedAction
+
 -- R4 converse route A (#197): pooled polling, unit 1.
 #print axioms RelSignature.InfiniteRelExchangeableLaw.PooledRankExtension.iCondIndepFun_originalBlock_sourcePollingCond
 #print axioms RelSignature.InfiniteRelExchangeableLaw.pooledPollingWitness
diff --git a/scripts/check_census_and_axioms.py b/scripts/check_census_and_axioms.py
index 8806974..55a36cc 100644
--- a/scripts/check_census_and_axioms.py
+++ b/scripts/check_census_and_axioms.py
@@ -307,6 +307,10 @@
     "RelSignature.BipartiteRegression.bipartiteSuccessor",
     "RelSignature.BipartiteRegression.ae_edge_xor",
     "RelSignature.BipartiteRegression.not_indepFun_rankTwoCoupling",
+    "RelSignature.InfiniteRelExchangeableLaw.austinBaseRelabel_one",
+    "RelSignature.InfiniteRelExchangeableLaw.austinBaseRelabel_mul",
+    "RelSignature.InfiniteRelExchangeableLaw.enrichedPollingMap_naturality",
+    "RelSignature.InfiniteRelExchangeableLaw.enrichedPollingLaw_map_enrichedAction",
     "RelSignature.InfiniteRelExchangeableLaw.pollingClusters",
     "RelSignature.InfiniteRelExchangeableLaw.PooledRankExtension.iCondIndepFun_originalBlock_sourcePollingCond",
     "RelSignature.InfiniteRelExchangeableLaw.pooledPollingWitness",

From 96dd17b981e32def0f1d9c5524b71c3de3632ddf Mon Sep 17 00:00:00 2001
From: Cameron Freer <cameronfreer@gmail.com>
Date: Mon, 31 Aug 2026 09:30:49 +0000
Subject: [PATCH 2/5] refactor: make the forward transport route-local public
 under `Austin` (#197)

Compressing the enriched law in unit 2 needs the same forward transport of mutual
conditional independence that unit 1's witness uses. Duplicating the proof would be
the wrong fix, so `iCondIndepFun_of_map` moves from `private` into a route-local
`Austin` namespace: public within this development, which now has more than one
consumer for it, and consumed by both units.

This is **not** promotion to `ForMathlib/`. A second consumer inside the same route
is not an independent consumer; that remains the condition for extracting a general
transport theorem, and the docstring says so.

`PooledPollingWitness` deliberately stays outside the namespace, keeping the name it
already has on master.

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

diff --git a/Graphon/RelAustinPolling.lean b/Graphon/RelAustinPolling.lean
index 5f1dae3..66a2498 100644
--- a/Graphon/RelAustinPolling.lean
+++ b/Graphon/RelAustinPolling.lean
@@ -584,11 +584,14 @@ 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.** 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 β}
+namespace Austin
+
+/-- **Forward transport of mutual conditional independence along a measurable map.** Route-local:
+public within the Austin development, which has more than one consumer for it, but not promoted to
+`ForMathlib/` — that awaits a consumer independent of this route. No injectivity is needed, which
+is why neither direction of the existing transport API applies: the maps that build the enriched
+objects forget the spare half of the structure. -/
+theorem iCondIndepFun_of_map {α β : Type*} {m' : MeasurableSpace β}
     [mα : MeasurableSpace α] [mβ : MeasurableSpace β]
     [StandardBorelSpace α] [StandardBorelSpace β]
     {P : Measure α} [IsFiniteMeasure P] {T : α → β}
@@ -637,6 +640,8 @@ private theorem iCondIndepFun_of_map {α β : Type*} {m' : MeasurableSpace β}
     exact Finset.measurable_prod S fun i _ => (stronglyMeasurable_condExp.mono hm').measurable
   exact (ae_map_iff hT.aemeasurable hmeas).mpr hcomp
 
+end Austin
+
 /-! ### The witness -/
 
 /-- **The polling conclusion**: mutual conditional independence of the *entire* rank-`n` block
@@ -683,7 +688,7 @@ theorem pooledPollingWitness {C : M.RankRepresentation n} (Q : PooledRankExtensi
       ((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
+    exact Austin.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

From a8c4f69bfdc4a60418c98bc5451e2efbe6fae3d9 Mon Sep 17 00:00:00 2001
From: Cameron Freer <cameronfreer@gmail.com>
Date: Mon, 31 Aug 2026 09:59:25 +0000
Subject: [PATCH 3/5] =?UTF-8?q?feat:=20the=20Austin=20enriched=20object=20?=
 =?UTF-8?q?and=20its=20coherent-basis=20adapter=20=E2=80=94=20unit=202=20b?=
 =?UTF-8?q?undle=20(#197)?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

`AustinEnrichedObject` packages a **base-extended law over the existing signature**:
no synthetic relational signature is introduced, and the pooled real latents remain
real rather than being encoded as Boolean relation coordinates.

`austinEnrichedObject` constructs it from `Q` and the unit-1 witness as the **exact
pushforward** of `enrichedPollingLaw` along the compression that drops the redundant
original-latent coordinate — redundant because on the image of `enrichedPollingMap`
it is `restrictOriginalLatents` of the pooled array. So `map_original` recovers `C.P`
from the pooled component alone, through `Q.map_restrict_embedding` at the
original-vertex embedding. `mutualCondIndep` is the unit-1 witness moved forward by
the route-local `Austin.iCondIndepFun_of_map`, not a second proof.

The adapter is stated for an **arbitrary** coherent basis, so no `Fintype S.Srt`
enters; selecting one via `nonempty_coherentBasis` is what would introduce it. All
four commuting laws are exact:

* boundary projection through the extended lower factor — `rfl`;
* exact-anchor projection through the layer — `rfl`;
* `map_forget_base` — forgetting the base returns the corresponding pushforward of
  `M.law`, since the base carries no structural information;
* `map_recombine` — **the unit-2 regression for exact truncation**: recombining lower
  and layer through `lowerFactorSpaceSuccEquiv.symm` returns the rank-`(n+1)`
  lower-factor law. An equality of pushed measures with the base forgotten; an a.e.
  version, or one retaining a base coordinate, would not constrain the successor
  construction where it must be constrained.

The rank-`m` layer deliberately does **not** carry the base: the layer is where the
fresh rank-`m` information lives, and the base is the lower-rank data it is read
against.

Lean note: `measurable_lowerFactorMap` is stated at `lowerRankAlgebra`; the
ambient-measurable form is `measurable_lowerFactorMap'`.

Audit 437 → 442. Gates: lake build clean (3410 jobs), census + axiom audit pass, zero
sorries, no warnings.
---
 Graphon/RelAustinEnriched.lean     | 201 +++++++++++++++++++++++++++++
 Graphon/RelAustinPolling.lean      |  13 +-
 scripts/axiom_audit.lean           |   7 +-
 scripts/check_census_and_axioms.py |   5 +
 4 files changed, 221 insertions(+), 5 deletions(-)

diff --git a/Graphon/RelAustinEnriched.lean b/Graphon/RelAustinEnriched.lean
index 07cfe1c..d43c734 100644
--- a/Graphon/RelAustinEnriched.lean
+++ b/Graphon/RelAustinEnriched.lean
@@ -401,6 +401,118 @@ theorem enrichedPollingLaw_map_enrichedAction {C : M.RankRepresentation n}
     show (Q.law : Measure (RelStructure S (PoolVertex S) × PooledRankLatentSpace S n)).map
         (pooledAction S n σ) = Q.law from Q.invariant (poolLift σ)]
 
+/-! ### The bundle
+
+Compressing the enriched law drops the *original* rank-`n` latents, which are redundant: on the
+image of `enrichedPollingMap` they are `restrictOriginalLatents` of the pooled array, so nothing is
+lost and `map_original` recovers `C.P` from the pooled component alone. -/
+
+open scoped Classical in
+/-- Forget the redundant original-latent coordinate. -/
+noncomputable def compressEnriched :
+    EnrichedSpace S n → RelStructure S (Vinfinite S) × AustinBaseSpace S n :=
+  fun q => (q.1.1, q.2)
+
+open scoped Classical in
+omit [Countable S.Srt] [Countable S.Rel] in
+theorem measurable_compressEnriched :
+    Measurable (compressEnriched (S := S) (n := n)) :=
+  (measurable_fst.fst).prodMk measurable_snd
+
+open scoped Classical in
+/-- **The base-extended law**: the representation's structure together with the Austin base, over
+the existing signature. No synthetic relational signature is introduced, and the pooled real
+latents remain real — they are never encoded as Boolean relation coordinates. -/
+structure AustinEnrichedObject (C : M.RankRepresentation n) where
+  /-- The joint law of the structure and the auxiliary base. -/
+  law : Measure (RelStructure S (Vinfinite S) × AustinBaseSpace S n)
+  /-- It is a probability measure. -/
+  isProbabilityMeasure_law : IsProbabilityMeasure law
+  /-- Its structure marginal is the exchangeable law. -/
+  map_fst : law.map Prod.fst = (M.law : Measure (RelStructure S (Vinfinite S)))
+  /-- **Recovery of the representation**: reading the structure together with the original-support
+  latents of the pooled array returns `C.P` exactly. -/
+  map_original :
+    law.map (fun p => (p.1, restrictOriginalLatents S n p.2.1)) = C.P
+  /-- Invariance under the diagonal action. -/
+  invariant : ∀ σ : FinSuppPerm S,
+    law.map (Prod.map (RelStructure.relabel σ.1) (austinBaseRelabel σ n)) = law
+  /-- **Mutual** conditional independence of the whole rank-`n` block family given the base. -/
+  mutualCondIndep :
+    iCondIndepFun (MeasurableSpace.comap
+        (Prod.snd : RelStructure S (Vinfinite S) × AustinBaseSpace S n → _) inferInstance)
+      measurable_snd.comap_le
+      (fun A : RankSupport S n => blockMap A.1 ∘ Prod.fst) law
+
+open scoped Classical in
+/-- The compressed observation, read directly on the pooled space. -/
+noncomputable def pooledToEnrichedObject :
+    RelStructure S (PoolVertex S) × PooledRankLatentSpace S n →
+      RelStructure S (Vinfinite S) × AustinBaseSpace S n :=
+  fun p => (restrictOriginal S p.1, (p.2, pollingClusters p))
+
+open scoped Classical in
+omit [Countable S.Srt] [Countable S.Rel] in
+theorem compressEnriched_comp_enrichedPollingMap :
+    compressEnriched ∘ (enrichedPollingMap (S := S) (n := n)) = pooledToEnrichedObject := rfl
+
+open scoped Classical in
+omit [Countable S.Srt] in
+theorem measurable_pooledToEnrichedObject :
+    Measurable (pooledToEnrichedObject (S := S) (n := n)) :=
+  ((measurable_restrict _).comp measurable_fst).prodMk
+    (measurable_snd.prodMk measurable_pollingClusters)
+
+open scoped Classical in
+/-- **The bundle exists.** The law is the exact pushforward of the enriched polling law; the four
+laws are transports of results already established, and the mutual conditional independence is the
+unit-1 witness moved forward by the route-local transport rather than reproved. -/
+noncomputable def austinEnrichedObject [Fintype S.Srt] {C : M.RankRepresentation n}
+    (Q : PooledRankExtension C) (W : PooledPollingWitness C Q) :
+    AustinEnrichedObject C where
+  law := (enrichedPollingLaw Q).map compressEnriched
+  isProbabilityMeasure_law := by
+    haveI : IsProbabilityMeasure (enrichedPollingLaw Q) := inferInstance
+    exact Measure.isProbabilityMeasure_map measurable_compressEnriched.aemeasurable
+  map_fst := by
+    haveI := C.isProbabilityMeasure_P
+    rw [Measure.map_map measurable_fst measurable_compressEnriched,
+      show (Prod.fst ∘ compressEnriched (S := S) (n := n)) = Prod.fst ∘ Prod.fst from rfl,
+      ← Measure.map_map measurable_fst measurable_fst, enrichedPollingLaw_map_fst, C.map_fst]
+  map_original := by
+    haveI := C.isProbabilityMeasure_P
+    have hm : Measurable (fun p : RelStructure S (Vinfinite S) × AustinBaseSpace S n =>
+        (p.1, restrictOriginalLatents S n p.2.1)) :=
+      measurable_fst.prodMk ((measurable_restrictOriginalLatents n).comp (measurable_snd.fst))
+    rw [Measure.map_map hm measurable_compressEnriched, enrichedPollingLaw,
+      Measure.map_map (hm.comp measurable_compressEnriched) measurable_enrichedPollingMap,
+      show ((fun p : RelStructure S (Vinfinite S) × AustinBaseSpace S n =>
+            (p.1, restrictOriginalLatents S n p.2.1)) ∘ compressEnriched) ∘
+          (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)
+  invariant := fun σ => by
+    rw [Measure.map_map ((measurable_relabel σ.1).prodMap (measurable_austinBaseRelabel σ n))
+        measurable_compressEnriched,
+      show (Prod.map (RelStructure.relabel σ.1) (austinBaseRelabel σ n) ∘
+          compressEnriched (S := S) (n := n)) =
+        compressEnriched ∘ enrichedAction S n σ from rfl,
+      ← Measure.map_map measurable_compressEnriched (measurable_enrichedAction σ n),
+      enrichedPollingLaw_map_enrichedAction Q σ]
+  mutualCondIndep := by
+    haveI := C.isProbabilityMeasure_P
+    refine Austin.iCondIndepFun_of_map measurable_compressEnriched measurable_snd.comap_le
+      (fun A : RankSupport S n => (measurable_blockMap A.1).comp measurable_fst) ?_
+    have h := W.mutualCondIndep
+    refine Austin.iCondIndepFun_congr_cond h ?_ _
+    show MeasurableSpace.comap (pollingCond S n) inferInstance =
+      (MeasurableSpace.comap
+        (Prod.snd : RelStructure S (Vinfinite S) × AustinBaseSpace S n → _)
+        inferInstance).comap compressEnriched
+    rw [MeasurableSpace.comap_comp]
+    rfl
+
 /-! ### Adapter spaces
 
 Introduced here only so that their standard-Borel structure is available and inferred rather than
@@ -423,6 +535,95 @@ instance (B : CoherentBasis M) (m : ℕ) :
 instance (B : CoherentBasis M) (m : ℕ) (A : Finset (Σ s : S.Srt, Vinfinite S s)) :
     StandardBorelSpace (EnrichedBoundarySpace B m A) := inferInstance
 
+/-! ### The adapter into the coherent-basis factor API
+
+For an arbitrary coherent basis: selecting one via `nonempty_coherentBasis` is what would introduce
+`[Fintype S.Srt]`, and that is deliberately not done here. The four commuting laws are exact, and
+the last is the unit-2 regression for eventual exact truncation. -/
+
+variable (B : CoherentBasis M)
+
+/-- The lower factor, extended by the base. -/
+noncomputable def enrichedLowerMap (m : ℕ) :
+    RelStructure S (Vinfinite S) × AustinBaseSpace S m → EnrichedLowerSpace B m :=
+  fun p => (B.lowerFactorMap m p.1, p.2)
+
+/-- The boundary at `A`, extended by the base. -/
+noncomputable def enrichedBoundaryMap (m : ℕ) (A : Finset (Σ s : S.Srt, Vinfinite S s)) :
+    RelStructure S (Vinfinite S) × AustinBaseSpace S m → EnrichedBoundarySpace B m A :=
+  fun p => (B.boundaryMap A p.1, p.2)
+
+/-- The rank-`m` layer. The base is **not** attached: the layer is where the fresh rank-`m`
+information lives, and the base is the lower-rank data it is read against. -/
+noncomputable def enrichedLayerMap (m : ℕ) :
+    RelStructure S (Vinfinite S) × AustinBaseSpace S m → B.RankLayerSpace m :=
+  fun p => B.rankLayerMap m p.1
+
+/-- The exact-anchor layer at `A`. -/
+noncomputable def enrichedExactMap (m : ℕ) (A : Finset (Σ s : S.Srt, Vinfinite S s)) :
+    RelStructure S (Vinfinite S) × AustinBaseSpace S m → B.ExactSpace A :=
+  fun p => B.exactMap A p.1
+
+omit [Countable S.Srt] [Countable S.Rel] in
+/-- **First commuting law**: projecting the extended lower factor to the boundary, leaving the base
+untouched, is the extended boundary map. -/
+theorem lowerToBoundary_comp_enrichedLowerMap {m : ℕ}
+    {A : Finset (Σ s : S.Srt, Vinfinite S s)} (hA : A.card = m) :
+    Prod.map (B.lowerToBoundaryProjection hA) (id : AustinBaseSpace S m → _) ∘
+        enrichedLowerMap B m = enrichedBoundaryMap B m A := rfl
+
+omit [Countable S.Srt] [Countable S.Rel] in
+/-- **Second commuting law**: the exact-anchor layer factors through the rank-`m` layer. -/
+theorem rankLayerToExact_comp_enrichedLayerMap {m : ℕ}
+    {A : Finset (Σ s : S.Srt, Vinfinite S s)} (hA : A.card = m) :
+    B.rankLayerToExactProjection hA ∘ enrichedLayerMap B m = enrichedExactMap B m A := rfl
+
+omit [Countable S.Srt] [Countable S.Rel] in
+theorem measurable_enrichedLowerMap (m : ℕ) : Measurable (enrichedLowerMap B m) :=
+  ((B.measurable_lowerFactorMap' m).comp measurable_fst).prodMk measurable_snd
+
+omit [Countable S.Srt] [Countable S.Rel] in
+theorem measurable_enrichedLayerMap (m : ℕ) : Measurable (enrichedLayerMap B m) :=
+  (B.measurable_rankLayerMap m).comp measurable_fst
+
+/-- **Third commuting law**: forgetting the auxiliary base from the joint lower/layer observation
+returns the corresponding pushforward of `M.law`. The base carries no structural information — it
+is the lower-rank randomness the structure is read against. -/
+theorem map_forget_base {C : M.RankRepresentation n} (O : AustinEnrichedObject C) :
+    (O.law.map fun p => ((enrichedLowerMap B n p).1, enrichedLayerMap B n p)) =
+      (M.law : Measure (RelStructure S (Vinfinite S))).map
+        fun X => (B.lowerFactorMap n X, B.rankLayerMap n X) := by
+  haveI := O.isProbabilityMeasure_law
+  have hjoint : Measurable fun X : RelStructure S (Vinfinite S) =>
+      (B.lowerFactorMap n X, B.rankLayerMap n X) :=
+    (B.measurable_lowerFactorMap' n).prodMk (B.measurable_rankLayerMap n)
+  rw [show (fun p : RelStructure S (Vinfinite S) × AustinBaseSpace S n =>
+        ((enrichedLowerMap B n p).1, enrichedLayerMap B n p)) =
+      (fun X => (B.lowerFactorMap n X, B.rankLayerMap n X)) ∘ Prod.fst from rfl,
+    ← Measure.map_map hjoint measurable_fst, O.map_fst]
+
+/-- **The unit-2 regression for exact truncation**: recombining the lower and layer coordinates
+through `lowerFactorSpaceSuccEquiv.symm` returns the rank-`(n+1)` lower-factor law, on the nose.
+
+This is an equality of pushed measures with the auxiliary base **forgotten** and no
+almost-everywhere weakening: an a.e. version, or one retaining a base coordinate, would not
+constrain the successor construction where it has to be constrained. -/
+theorem map_recombine {C : M.RankRepresentation n} (O : AustinEnrichedObject C) :
+    ((O.law.map fun p => ((enrichedLowerMap B n p).1, enrichedLayerMap B n p)).map
+        (B.lowerFactorSpaceSuccEquiv n).symm) =
+      (M.law : Measure (RelStructure S (Vinfinite S))).map (B.lowerFactorMap (n + 1)) := by
+  haveI := O.isProbabilityMeasure_law
+  rw [map_forget_base B O,
+    Measure.map_map (B.lowerFactorSpaceSuccEquiv n).symm.measurable
+      ((B.measurable_lowerFactorMap' n).prodMk (B.measurable_rankLayerMap n)),
+    show ((B.lowerFactorSpaceSuccEquiv n).symm ∘
+        fun X => (B.lowerFactorMap n X, B.rankLayerMap n X)) =
+      B.lowerFactorMap (n + 1) from funext fun X => by
+        show (B.lowerFactorSpaceSuccEquiv n).symm
+            (B.lowerFactorMap n X, B.rankLayerMap n X) = B.lowerFactorMap (n + 1) X
+        rw [← B.lowerFactorSpaceSuccEquiv_lowerFactorMap n X,
+          (B.lowerFactorSpaceSuccEquiv n).symm_apply_apply]]
+
 end InfiniteRelExchangeableLaw
 
 end RelSignature
diff --git a/Graphon/RelAustinPolling.lean b/Graphon/RelAustinPolling.lean
index 66a2498..808ea47 100644
--- a/Graphon/RelAustinPolling.lean
+++ b/Graphon/RelAustinPolling.lean
@@ -89,11 +89,14 @@ variable {S : RelSignature} [Countable S.Srt] [Countable S.Rel]
 
 attribute [local instance] RankRepresentation.isProbabilityMeasure_P
 
+namespace Austin
+
 /-- **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 Ω]
+counterpart, route-local while its consumers are internal to this development. Needed because the
+conditioning algebra occurs in a dependent position — the `≤` proof mentions it — so `rw` cannot
+reach it. -/
+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 μ)
@@ -101,6 +104,8 @@ private theorem iCondIndepFun_congr_cond {Ω : Type*} [mΩ : MeasurableSpace Ω]
   subst h12
   exact h
 
+end Austin
+
 /-! ### Weak union for conditional independence
 
 The graphoid axiom this development turns on, and which neither Mathlib nor this repository has:
@@ -684,7 +689,7 @@ theorem pooledPollingWitness {C : M.RankRepresentation n} (Q : PooledRankExtensi
     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
+    have h3 := Austin.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
diff --git a/scripts/axiom_audit.lean b/scripts/axiom_audit.lean
index 6c1cdf9..c32f096 100644
--- a/scripts/axiom_audit.lean
+++ b/scripts/axiom_audit.lean
@@ -347,7 +347,12 @@ 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): the Austin base and its action, unit 2 checkpoint.
+-- R4 converse route A (#197): the Austin base and its action, unit 2 checkpoint and bundle.
+#print axioms RelSignature.InfiniteRelExchangeableLaw.austinEnrichedObject
+#print axioms RelSignature.InfiniteRelExchangeableLaw.lowerToBoundary_comp_enrichedLowerMap
+#print axioms RelSignature.InfiniteRelExchangeableLaw.rankLayerToExact_comp_enrichedLayerMap
+#print axioms RelSignature.InfiniteRelExchangeableLaw.map_forget_base
+#print axioms RelSignature.InfiniteRelExchangeableLaw.map_recombine
 #print axioms RelSignature.InfiniteRelExchangeableLaw.austinBaseRelabel_one
 #print axioms RelSignature.InfiniteRelExchangeableLaw.austinBaseRelabel_mul
 #print axioms RelSignature.InfiniteRelExchangeableLaw.enrichedPollingMap_naturality
diff --git a/scripts/check_census_and_axioms.py b/scripts/check_census_and_axioms.py
index 55a36cc..5feff1d 100644
--- a/scripts/check_census_and_axioms.py
+++ b/scripts/check_census_and_axioms.py
@@ -307,6 +307,11 @@
     "RelSignature.BipartiteRegression.bipartiteSuccessor",
     "RelSignature.BipartiteRegression.ae_edge_xor",
     "RelSignature.BipartiteRegression.not_indepFun_rankTwoCoupling",
+    "RelSignature.InfiniteRelExchangeableLaw.austinEnrichedObject",
+    "RelSignature.InfiniteRelExchangeableLaw.lowerToBoundary_comp_enrichedLowerMap",
+    "RelSignature.InfiniteRelExchangeableLaw.rankLayerToExact_comp_enrichedLayerMap",
+    "RelSignature.InfiniteRelExchangeableLaw.map_forget_base",
+    "RelSignature.InfiniteRelExchangeableLaw.map_recombine",
     "RelSignature.InfiniteRelExchangeableLaw.austinBaseRelabel_one",
     "RelSignature.InfiniteRelExchangeableLaw.austinBaseRelabel_mul",
     "RelSignature.InfiniteRelExchangeableLaw.enrichedPollingMap_naturality",

From 0edaf20fa3f233489a36f9da3905259b5234b7fe Mon Sep 17 00:00:00 2001
From: Cameron Freer <cameronfreer@gmail.com>
Date: Mon, 31 Aug 2026 11:40:15 +0000
Subject: [PATCH 4/5] fix: correct the base semantics, drop an accidental
 hypothesis, narrow a claim (#197)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Four corrections, one of them substantive.

* **The base does not "carry no rank-`n` block".** That claim was false of exactly the
  half that matters: `ClusterSpace` is indexed by rank-`n` supports that are not wholly
  original, so the cluster component carries rank-`n` blocks by construction. Only the
  *latent* component is free of them. The claim was also self-undermining — a base with
  no rank-`n` block could not do the work the polling argument needs conditioning on it
  to do. Corrected at all three sites, plus a fourth in `RelAustinPolling` whose scoping
  was ambiguous in the same way; the text now states the asymmetry between the two
  components explicitly rather than a blanket claim.

* **`map_forget_base` asserts no independence.** Its docstring said the base carries no
  structural information; the clusters are correlated structural polling data. The
  identity says only that the structural factor law is recovered once the base is
  discarded.

* **`map_recombine` is a prerequisite, not the truncation statement.** It mentions
  neither `C.P` nor `rankLatentProjection`, so it cannot pin `RankSuccessor.truncation`.
  Exact truncation will come from `map_original` together with the assembly unit's
  source-splitting identity. Narrowed in the theorem, the section header, and the index.

* **`[Fintype S.Srt]` removed from `austinEnrichedObject`.** Nothing there selects a
  basis; it contradicted the countable-only contract, and removing it strictly
  generalizes the signature. No signature in the module now carries it.

Also recalibrates the module header and index entry, which described only the
checkpoint and named the nonexistent `enrichedPollingLaw_map_austinBaseRelabel`; the
declaration is `enrichedPollingLaw_map_enrichedAction`.

No proof changes. Gates: lake build clean (3410 jobs), census + axiom audit pass, zero
sorries, no warnings.
---
 Graphon.lean                   |  2 +-
 Graphon/RelAustinEnriched.lean | 59 ++++++++++++++++++++--------------
 Graphon/RelAustinPolling.lean  |  4 ++-
 3 files changed, 39 insertions(+), 26 deletions(-)

diff --git a/Graphon.lean b/Graphon.lean
index 26d2e8f..6e063ab 100644
--- a/Graphon.lean
+++ b/Graphon.lean
@@ -275,7 +275,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.RelAustinEnriched` — R4 converse (#107/#197), **route A (Austin) unit 2**, law-free checkpoint: the Austin base and its action. `AustinBaseSpace = PooledRankLatentSpace × ClusterSpace` is the **equivariant lower-rank base** over which the enriched kernel is later built — not fresh rank-`n` coordinates and not relational data; every pooled latent index has cardinality `< n`, so it carries no rank-`n` block. `poolLift` acts on the original half and fixes the spare half, and its preservation of `Sum.isRight` is what keeps mixed clusters mixed. **The orientation is contravariant** — `Equiv.trans` applies its first argument first, so `austinBaseRelabel (σ * τ) = austinBaseRelabel τ ∘ austinBaseRelabel σ`. `enrichedPollingMap_naturality` is **one square for all four components**: structure and pooled latents definitionally, clusters by `pollingClusters_relabel`, original latents by the split corollary `restrictOriginalLatents_sumCongr`; and `enrichedPollingLaw_map_enrichedAction` derives exact invariance from it with nothing but `Measure.map_map` and the extension's own invariance — no almost-everywhere step. The dependent cluster fibres are handled by `Bool`-valued pointwise bridges, with the single required cast isolated in one private lemma rather than by weakening `MixedClusterIndex`'s reducibility, which would expose a substantive subtype's implementation globally to solve a local elaboration problem
+* `Graphon.RelAustinEnriched` — R4 converse (#107/#197), **route A (Austin) unit 2**: the Austin base, its action, and the base-extended bundle with its coherent-basis adapter. `AustinBaseSpace = PooledRankLatentSpace × ClusterSpace` is the equivariant base over which the enriched kernel is later built, and **its two components differ in kind**: the latent component carries no rank-`n` latent, every pooled index having cardinality `< n`, while the cluster component deliberately carries rank-`n` blocks at supports that are not wholly original — the clusters are correlated structural polling data, which is precisely why conditioning on them is informative. `poolLift` acts on the original half and fixes the spare half, and its preservation of `Sum.isRight` keeps mixed clusters mixed. **The orientation is contravariant** — `Equiv.trans` applies its first argument first, so `austinBaseRelabel (σ * τ) = austinBaseRelabel τ ∘ austinBaseRelabel σ`. `enrichedPollingMap_naturality` is **one square for all four components**: structure and pooled latents definitionally, clusters by `pollingClusters_relabel`, original latents by the split corollary `restrictOriginalLatents_sumCongr`; `enrichedPollingLaw_map_enrichedAction` derives exact invariance from it using nothing but `Measure.map_map` and the extension's own invariance. `austinEnrichedObject` builds the bundle as the **exact pushforward** of `enrichedPollingLaw` along the compression dropping the redundant original-latent coordinate, so `map_original` recovers `C.P` through `map_restrict_embedding` at the original-vertex embedding. The adapter is stated for an **arbitrary** coherent basis, so no `Fintype S.Srt` enters anywhere in this module; `map_recombine` recombines lower and layer through `lowerFactorSpaceSuccEquiv.symm` to return the rank-`(n+1)` lower-factor law exactly — a prerequisite for exact truncation rather than that statement itself, since it mentions neither `C.P` nor `rankLatentProjection`. The dependent cluster fibres are handled by `Bool`-valued pointwise bridges, with the single required cast isolated in one private lemma rather than by weakening `MixedClusterIndex`'s reducibility, which would expose a substantive subtype's implementation globally to solve a local elaboration problem
 * `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
diff --git a/Graphon/RelAustinEnriched.lean b/Graphon/RelAustinEnriched.lean
index d43c734..1e9d166 100644
--- a/Graphon/RelAustinEnriched.lean
+++ b/Graphon/RelAustinEnriched.lean
@@ -16,13 +16,18 @@ outputs agree.
 
 The **auxiliary base** carried alongside the representation is
 `AustinBaseSpace S n = PooledRankLatentSpace S n × ClusterSpace S n`: the pooled lower-rank latents
-together with the mixed clusters. It is the equivariant lower-rank base over which the enriched
-kernel will later be built — not a family of fresh rank-`n` coordinates, and not relational data.
-Every pooled latent index has cardinality `< n`, so the base carries no rank-`n` block.
+together with the mixed clusters. It is the equivariant base over which the enriched kernel will
+later be built.
 
-This module is deliberately **law-free apart from one invariance**: it fixes the action and proves
-it strict, before any bundle, kernel, or conditional-distribution statement is written.
-Equivariance cannot be repaired downstream, so it is established first.
+Its two components differ in kind, and conflating them would be a mistake. The **latent**
+component carries no rank-`n` latent, every pooled index having cardinality `< n`. The **cluster**
+component, by contrast, deliberately does carry rank-`n` blocks — mixed ones, at supports that are
+not wholly original. That is the point of the poll: the clusters are correlated structural data,
+which is exactly why conditioning on them is informative.
+
+The action is fixed and proved strict before the bundle is built, because equivariance cannot be
+repaired downstream. No conditional distribution or kernel identity appears here; those belong to
+the kernel unit, and every such identity there is almost-everywhere under a named law.
 
 ## Contents
 
@@ -35,12 +40,13 @@ Equivariance cannot be repaired downstream, so it is established first.
 * `enrichedPollingMap_naturality` — **one global square** covering the structure, the original
   latents, the pooled latents and the clusters simultaneously. Stated generically in the cluster
   index, so genuinely mixed and all-spare indices are both covered.
-* `enrichedPollingLaw_map_austinBaseRelabel` — exact invariance of the pushed enriched law,
-  derived from that square together with the extension's own invariance.
-
-The adapter spaces `EnrichedLowerSpace` and `EnrichedBoundarySpace` are introduced here only so
-that their standard-Borel structure is available; their maps and commuting laws belong to the
-bundle that follows.
+* `enrichedPollingLaw_map_enrichedAction` — exact invariance of the pushed enriched law, derived
+  from that square together with the extension's own invariance.
+* `AustinEnrichedObject` and `austinEnrichedObject` — the **bundle**: a base-extended law over the
+  existing signature, constructed as the exact pushforward of `enrichedPollingLaw` along the
+  compression that drops the redundant original-latent coordinate.
+* `enrichedLowerMap`, `enrichedBoundaryMap`, `enrichedLayerMap`, `enrichedExactMap` and their four
+  commuting laws — the **adapter** into the coherent-basis factor API, for an arbitrary basis.
 -/
 
 open MeasureTheory ProbabilityTheory
@@ -55,9 +61,10 @@ variable {S : RelSignature} [Countable S.Srt] [Countable S.Rel]
 /-! ### The auxiliary base -/
 
 variable (S n) in
-/-- **The Austin base**: pooled lower-rank latents together with the mixed clusters. The
-equivariant lower-rank base of the construction; it carries no rank-`n` block, since every pooled
-latent index has cardinality `< n` and every cluster index carries a spare vertex. -/
+/-- **The Austin base**: pooled lower-rank latents together with the mixed clusters. The latent
+component carries no rank-`n` latent — every pooled index has cardinality `< n` — while the cluster
+component deliberately carries rank-`n` blocks at supports that are not wholly original. The base
+is therefore lower-rank in its latent part only; its cluster part is structural polling data. -/
 abbrev AustinBaseSpace := PooledRankLatentSpace S n × ClusterSpace S n
 
 instance : StandardBorelSpace (AustinBaseSpace S n) := inferInstance
@@ -467,7 +474,7 @@ open scoped Classical in
 /-- **The bundle exists.** The law is the exact pushforward of the enriched polling law; the four
 laws are transports of results already established, and the mutual conditional independence is the
 unit-1 witness moved forward by the route-local transport rather than reproved. -/
-noncomputable def austinEnrichedObject [Fintype S.Srt] {C : M.RankRepresentation n}
+noncomputable def austinEnrichedObject {C : M.RankRepresentation n}
     (Q : PooledRankExtension C) (W : PooledPollingWitness C Q) :
     AustinEnrichedObject C where
   law := (enrichedPollingLaw Q).map compressEnriched
@@ -539,7 +546,7 @@ instance (B : CoherentBasis M) (m : ℕ) (A : Finset (Σ s : S.Srt, Vinfinite S
 
 For an arbitrary coherent basis: selecting one via `nonempty_coherentBasis` is what would introduce
 `[Fintype S.Srt]`, and that is deliberately not done here. The four commuting laws are exact, and
-the last is the unit-2 regression for eventual exact truncation. -/
+the last is a prerequisite for eventual exact truncation rather than that statement itself. -/
 
 variable (B : CoherentBasis M)
 
@@ -587,8 +594,11 @@ theorem measurable_enrichedLayerMap (m : ℕ) : Measurable (enrichedLayerMap B m
   (B.measurable_rankLayerMap m).comp measurable_fst
 
 /-- **Third commuting law**: forgetting the auxiliary base from the joint lower/layer observation
-returns the corresponding pushforward of `M.law`. The base carries no structural information — it
-is the lower-rank randomness the structure is read against. -/
+returns the corresponding pushforward of `M.law`.
+
+This asserts nothing about independence, and the base is *not* free of structural information — the
+clusters are correlated structural polling data. What the identity says is only that the
+structural factor law is recovered once the base is discarded, which is what the adapter needs. -/
 theorem map_forget_base {C : M.RankRepresentation n} (O : AustinEnrichedObject C) :
     (O.law.map fun p => ((enrichedLowerMap B n p).1, enrichedLayerMap B n p)) =
       (M.law : Measure (RelStructure S (Vinfinite S))).map
@@ -602,12 +612,13 @@ theorem map_forget_base {C : M.RankRepresentation n} (O : AustinEnrichedObject C
       (fun X => (B.lowerFactorMap n X, B.rankLayerMap n X)) ∘ Prod.fst from rfl,
     ← Measure.map_map hjoint measurable_fst, O.map_fst]
 
-/-- **The unit-2 regression for exact truncation**: recombining the lower and layer coordinates
-through `lowerFactorSpaceSuccEquiv.symm` returns the rank-`(n+1)` lower-factor law, on the nose.
+/-- **Factor-side recombination**: recombining the lower and layer coordinates through
+`lowerFactorSpaceSuccEquiv.symm` returns the rank-`(n+1)` lower-factor law, on the nose — an
+equality of pushed measures with the auxiliary base forgotten, with no almost-everywhere weakening.
 
-This is an equality of pushed measures with the auxiliary base **forgotten** and no
-almost-everywhere weakening: an a.e. version, or one retaining a base coordinate, would not
-constrain the successor construction where it has to be constrained. -/
+It is a **prerequisite** for exact truncation, not that statement itself: it mentions neither `C.P`
+nor `rankLatentProjection`, so it does not pin `RankSuccessor.truncation`. Exact truncation will
+come from `map_original` together with the source-splitting identity of the assembly unit. -/
 theorem map_recombine {C : M.RankRepresentation n} (O : AustinEnrichedObject C) :
     ((O.law.map fun p => ((enrichedLowerMap B n p).1, enrichedLayerMap B n p)).map
         (B.lowerFactorSpaceSuccEquiv n).symm) =
diff --git a/Graphon/RelAustinPolling.lean b/Graphon/RelAustinPolling.lean
index 808ea47..2f1ab37 100644
--- a/Graphon/RelAustinPolling.lean
+++ b/Graphon/RelAustinPolling.lean
@@ -262,7 +262,9 @@ variable (S n) in
 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. 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. -/
+factor. Every pooled *latent* index has cardinality `< n`, so the latent component reveals no
+rank-`n` block; the clusters, by contrast, are rank-`n` blocks at supports that are not wholly
+original, and carrying them is the point of the poll. -/
 abbrev EnrichedSpace :=
   (RelStructure S (Vinfinite S) × RankLatentSpace S n) ×
     (PooledRankLatentSpace S n × ClusterSpace S n)

From 95777388b0c814c76de31781495605e9ba6de782 Mon Sep 17 00:00:00 2001
From: Cameron Freer <cameronfreer@gmail.com>
Date: Mon, 31 Aug 2026 15:30:07 +0000
Subject: [PATCH 5/5] docs: title the module for unit 2's full scope (#197)

The heading still read "law-free checkpoint", which described the module before the
bundle and adapter were added to it. It now names what the module actually contains.

No statement or proof changes.
---
 Graphon/RelAustinEnriched.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Graphon/RelAustinEnriched.lean b/Graphon/RelAustinEnriched.lean
index 1e9d166..ae94d4c 100644
--- a/Graphon/RelAustinEnriched.lean
+++ b/Graphon/RelAustinEnriched.lean
@@ -9,7 +9,7 @@ import Graphon.RelFactorLaws
 import Graphon.RelRankSuccessor
 
 /-!
-# The Austin base and its action: unit 2, law-free checkpoint (R4 converse, #107, #197)
+# The Austin base, its action, and the base-extended bundle: unit 2 (R4 converse, #107, #197)
 
 Route **A** (Austin) only. No Kallenberg machinery, and nothing here asserts that the two routes'
 outputs agree.