diff --git a/Graphon.lean b/Graphon.lean
index 727e043..6e063ab 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**: 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
new file mode 100644
index 0000000..ae94d4c
--- /dev/null
+++ b/Graphon/RelAustinEnriched.lean
@@ -0,0 +1,640 @@
+/-
+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, 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.
+
+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 base over which the enriched kernel will
+later be built.
+
+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
+
+* `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_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
+
+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 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
+
+/-! ### 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 σ)]
+
+/-! ### 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 {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
+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
+
+/-! ### 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 a prerequisite for eventual exact truncation rather than that statement itself. -/
+
+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`.
+
+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
+        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]
+
+/-- **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.
+
+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) =
+      (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 5f1dae3..2f1ab37 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:
@@ -257,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)
@@ -584,11 +591,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 +647,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
@@ -679,11 +691,11 @@ 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
-    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
diff --git a/scripts/axiom_audit.lean b/scripts/axiom_audit.lean
index ae31984..c32f096 100644
--- a/scripts/axiom_audit.lean
+++ b/scripts/axiom_audit.lean
@@ -347,6 +347,17 @@ 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 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
+#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..5feff1d 100644
--- a/scripts/check_census_and_axioms.py
+++ b/scripts/check_census_and_axioms.py
@@ -307,6 +307,15 @@
     "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",
+    "RelSignature.InfiniteRelExchangeableLaw.enrichedPollingLaw_map_enrichedAction",
     "RelSignature.InfiniteRelExchangeableLaw.pollingClusters",
     "RelSignature.InfiniteRelExchangeableLaw.PooledRankExtension.iCondIndepFun_originalBlock_sourcePollingCond",
     "RelSignature.InfiniteRelExchangeableLaw.pooledPollingWitness",