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.

The auxiliary base

@[reducible, inline]

abbrev RelSignature.InfiniteRelExchangeableLaw.AustinBaseSpace (S : RelSignature) (n : ℕ) : Type u_1

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.

Equations

• RelSignature.InfiniteRelExchangeableLaw.AustinBaseSpace S n = (S.PooledRankLatentSpace n × RelSignature.InfiniteRelExchangeableLaw.ClusterSpace S n)

instance RelSignature.InfiniteRelExchangeableLaw.instStandardBorelSpaceAustinBaseSpace {S : RelSignature} [Countable S.Srt] [Countable S.Rel] {n : ℕ} : StandardBorelSpace (AustinBaseSpace S n)

The split lift

def RelSignature.InfiniteRelExchangeableLaw.poolLift {S : RelSignature} (σ : ↥S.FinSuppPerm) (s : S.Srt) : Equiv.Perm (S.PoolVertex s)

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.

Equations

• RelSignature.InfiniteRelExchangeableLaw.poolLift σ s = Equiv.sumCongr (↑σ s) (Equiv.refl (S.Vinfinite s))

@[simp]

theorem RelSignature.InfiniteRelExchangeableLaw.isRight_poolLift {S : RelSignature} (σ : ↥S.FinSuppPerm) (s : S.Srt) (x : S.PoolVertex s) : Sum.isRight ((poolLift σ s) x) = Sum.isRight x

The split lift preserves the spare half, which is what keeps mixed clusters mixed.

@[simp]

theorem RelSignature.InfiniteRelExchangeableLaw.poolLift_one {S : RelSignature} (s : S.Srt) : poolLift 1 s = Equiv.refl (S.PoolVertex s)

theorem RelSignature.InfiniteRelExchangeableLaw.poolLift_mul {S : RelSignature} (σ τ : ↥S.FinSuppPerm) (s : S.Srt) : poolLift (σ * τ) s = poolLift σ s * poolLift τ s

The induced action on cluster indices

noncomputable def RelSignature.InfiniteRelExchangeableLaw.mixedClusterLift {S : RelSignature} (σ : ↥S.FinSuppPerm) (n : ℕ) : MixedClusterIndex S n ≃ MixedClusterIndex S n

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.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem RelSignature.InfiniteRelExchangeableLaw.mixedClusterLift_coe {S : RelSignature} (σ : ↥S.FinSuppPerm) (n : ℕ) (A : MixedClusterIndex S n) : ↑((mixedClusterLift σ n) A) = supportImage (fun (s : S.Srt) => Equiv.toEmbedding (poolLift σ s)) ↑A

@[simp]

theorem RelSignature.InfiniteRelExchangeableLaw.mixedClusterLift_one {S : RelSignature} (n : ℕ) : mixedClusterLift 1 n = Equiv.refl (MixedClusterIndex S n)

theorem RelSignature.InfiniteRelExchangeableLaw.mixedClusterLift_mul {S : RelSignature} (σ τ : ↥S.FinSuppPerm) (n : ℕ) : mixedClusterLift (σ * τ) n = (mixedClusterLift τ n).trans (mixedClusterLift σ n)

The action on the base

noncomputable def RelSignature.InfiniteRelExchangeableLaw.austinBaseRelabel {S : RelSignature} (σ : ↥S.FinSuppPerm) (n : ℕ) : AustinBaseSpace S n → AustinBaseSpace S n

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.

Equations

• One or more equations did not get rendered due to their size.

theorem RelSignature.InfiniteRelExchangeableLaw.measurable_austinBaseRelabel {S : RelSignature} (σ : ↥S.FinSuppPerm) (n : ℕ) : Measurable (austinBaseRelabel σ n)

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 σ.

theorem RelSignature.InfiniteRelExchangeableLaw.pollingClusters_relabel {S : RelSignature} {n : ℕ} (σ : ↥S.FinSuppPerm) (p : S.RelStructure S.PoolVertex × S.PooledRankLatentSpace n) (A : MixedClusterIndex S n) (c : BlockIndexOver S.PoolVertex ↑A) : pollingClusters (Prod.map (RelStructure.relabel (poolLift σ)) (⇑(pooledRankLatentRelabel (poolLift σ) n)) p) A c = pollingClusters p ((mixedClusterLift σ n) A) ((blockIndexCongr (fun (s : S.Srt) => Equiv.toEmbedding (poolLift σ s)) ↑A) c)

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 RelSignature.InfiniteRelExchangeableLaw.austinBaseRelabel_apply_cluster {S : RelSignature} (σ : ↥S.FinSuppPerm) (n : ℕ) (z : AustinBaseSpace S n) (A : MixedClusterIndex S n) (c : BlockIndexOver S.PoolVertex ↑A) : (austinBaseRelabel σ n z).2 A c = z.2 ((mixedClusterLift σ n) A) ((blockIndexCongr (fun (s : S.Srt) => Equiv.toEmbedding (poolLift σ s)) ↑A) c)

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 RelSignature.InfiniteRelExchangeableLaw.austinBaseRelabel_apply_cluster_one {S : RelSignature} (n : ℕ) (z : AustinBaseSpace S n) (A : MixedClusterIndex S n) (c : BlockIndexOver S.PoolVertex ↑A) : (austinBaseRelabel 1 n z).2 A c = z.2 A c

Identity law, pointwise.

theorem RelSignature.InfiniteRelExchangeableLaw.austinBaseRelabel_apply_cluster_mul {S : RelSignature} (σ τ : ↥S.FinSuppPerm) (n : ℕ) (z : AustinBaseSpace S n) (A : MixedClusterIndex S n) (c : BlockIndexOver S.PoolVertex ↑A) : (austinBaseRelabel (σ * τ) n z).2 A c = (austinBaseRelabel τ n (austinBaseRelabel σ n z)).2 A c

Composition law, pointwise, in the contravariant orientation forced by pooledRankLatentRelabel_comp.

The function-level laws

@[simp]

theorem RelSignature.InfiniteRelExchangeableLaw.austinBaseRelabel_one {S : RelSignature} (n : ℕ) : austinBaseRelabel 1 n = id

theorem RelSignature.InfiniteRelExchangeableLaw.austinBaseRelabel_mul {S : RelSignature} (σ τ : ↥S.FinSuppPerm) (n : ℕ) : austinBaseRelabel (σ * τ) n = austinBaseRelabel τ n ∘ austinBaseRelabel σ n

The global naturality square, and the invariance it yields

noncomputable def RelSignature.InfiniteRelExchangeableLaw.pooledAction (S : RelSignature) (n : ℕ) (σ : ↥S.FinSuppPerm) : S.RelStructure S.PoolVertex × S.PooledRankLatentSpace n → S.RelStructure S.PoolVertex × S.PooledRankLatentSpace n

The action on the pooled objects by the split lift.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def RelSignature.InfiniteRelExchangeableLaw.enrichedAction (S : RelSignature) (n : ℕ) (σ : ↥S.FinSuppPerm) : EnrichedSpace S n → EnrichedSpace S n

The action on the enriched objects: the representation coordinates move by σ, the auxiliary base by austinBaseRelabel.

Equations

• One or more equations did not get rendered due to their size.

theorem RelSignature.InfiniteRelExchangeableLaw.measurable_enrichedAction {S : RelSignature} (σ : ↥S.FinSuppPerm) (n : ℕ) : Measurable (enrichedAction S n σ)

theorem RelSignature.InfiniteRelExchangeableLaw.measurable_pooledAction {S : RelSignature} (σ : ↥S.FinSuppPerm) (n : ℕ) : Measurable (pooledAction S n σ)

theorem RelSignature.InfiniteRelExchangeableLaw.enrichedPollingMap_naturality {S : RelSignature} (σ : ↥S.FinSuppPerm) (n : ℕ) : enrichedPollingMap ∘ pooledAction S n σ = enrichedAction S n σ ∘ enrichedPollingMap

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 RelSignature.InfiniteRelExchangeableLaw.enrichedPollingLaw_map_enrichedAction {S : RelSignature} [Countable S.Srt] [Countable S.Rel] {M : S.InfiniteRelExchangeableLaw} {n : ℕ} {C : M.RankRepresentation n} (Q : PooledRankExtension C) (σ : ↥S.FinSuppPerm) : MeasureTheory.Measure.map (enrichedAction S n σ) (enrichedPollingLaw Q) = enrichedPollingLaw Q

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.

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.

noncomputable def RelSignature.InfiniteRelExchangeableLaw.compressEnriched {S : RelSignature} {n : ℕ} : EnrichedSpace S n → S.RelStructure S.Vinfinite × AustinBaseSpace S n

Forget the redundant original-latent coordinate.

Equations

• RelSignature.InfiniteRelExchangeableLaw.compressEnriched q = (q.1.1, q.2)

theorem RelSignature.InfiniteRelExchangeableLaw.measurable_compressEnriched {S : RelSignature} {n : ℕ} : Measurable compressEnriched

structure RelSignature.InfiniteRelExchangeableLaw.AustinEnrichedObject {S : RelSignature} [Countable S.Srt] [Countable S.Rel] {M : S.InfiniteRelExchangeableLaw} {n : ℕ} (C : M.RankRepresentation n) : Type u_1

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.

• law : MeasureTheory.Measure (S.RelStructure S.Vinfinite × AustinBaseSpace S n)

  The joint law of the structure and the auxiliary base.

• isProbabilityMeasure_law : MeasureTheory.IsProbabilityMeasure self.law

  It is a probability measure.

• map_fst : MeasureTheory.Measure.map Prod.fst self.law = ↑M.law

  Its structure marginal is the exchangeable law.

• map_original : MeasureTheory.Measure.map (fun (p : S.RelStructure S.Vinfinite × AustinBaseSpace S n) => (p.1, S.restrictOriginalLatents n p.2.1)) self.law = C.P

  Recovery of the representation: reading the structure together with the original-support latents of the pooled array returns C.P exactly.

• invariant (σ : ↥S.FinSuppPerm) : MeasureTheory.Measure.map (Prod.map (RelStructure.relabel ↑σ) (austinBaseRelabel σ n)) self.law = self.law

  Invariance under the diagonal action.

• mutualCondIndep : ProbabilityTheory.iCondIndepFun (MeasurableSpace.comap Prod.snd inferInstance) ⋯ (fun (A : S.RankSupport n) => blockMap ↑A ∘ Prod.fst) self.law

  Mutual conditional independence of the whole rank-n block family given the base.

noncomputable def RelSignature.InfiniteRelExchangeableLaw.pooledToEnrichedObject {S : RelSignature} {n : ℕ} : S.RelStructure S.PoolVertex × S.PooledRankLatentSpace n → S.RelStructure S.Vinfinite × AustinBaseSpace S n

The compressed observation, read directly on the pooled space.

Equations

• RelSignature.InfiniteRelExchangeableLaw.pooledToEnrichedObject p = (S.restrictOriginal p.1, p.2, RelSignature.InfiniteRelExchangeableLaw.pollingClusters p)

theorem RelSignature.InfiniteRelExchangeableLaw.compressEnriched_comp_enrichedPollingMap {S : RelSignature} {n : ℕ} : compressEnriched ∘ enrichedPollingMap = pooledToEnrichedObject

theorem RelSignature.InfiniteRelExchangeableLaw.measurable_pooledToEnrichedObject {S : RelSignature} [Countable S.Rel] {n : ℕ} : Measurable pooledToEnrichedObject

noncomputable def RelSignature.InfiniteRelExchangeableLaw.austinEnrichedObject {S : RelSignature} [Countable S.Srt] [Countable S.Rel] {M : S.InfiniteRelExchangeableLaw} {n : ℕ} {C : M.RankRepresentation n} (Q : PooledRankExtension C) (W : PooledPollingWitness C Q) : AustinEnrichedObject C

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.

Equations

• One or more equations did not get rendered due to their size.

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.

@[reducible, inline]

abbrev RelSignature.InfiniteRelExchangeableLaw.EnrichedLowerSpace {S : RelSignature} {M : S.InfiniteRelExchangeableLaw} (B : CoherentBasis M) (m : ℕ) : Type u_1

The lower-factor space extended by the Austin base.

Equations

• RelSignature.InfiniteRelExchangeableLaw.EnrichedLowerSpace B m = (B.LowerFactorSpace m × RelSignature.InfiniteRelExchangeableLaw.AustinBaseSpace S m)

@[reducible, inline]

abbrev RelSignature.InfiniteRelExchangeableLaw.EnrichedBoundarySpace {S : RelSignature} {M : S.InfiniteRelExchangeableLaw} (B : CoherentBasis M) (m : ℕ) (A : Finset ((s : S.Srt) × S.Vinfinite s)) : Type u_1

The boundary space at A extended by the Austin base.

Equations

• RelSignature.InfiniteRelExchangeableLaw.EnrichedBoundarySpace B m A = (B.BoundarySpace A × RelSignature.InfiniteRelExchangeableLaw.AustinBaseSpace S m)

instance RelSignature.InfiniteRelExchangeableLaw.instStandardBorelSpaceEnrichedLowerSpace {S : RelSignature} [Countable S.Srt] [Countable S.Rel] {M : S.InfiniteRelExchangeableLaw} (B : CoherentBasis M) (m : ℕ) : StandardBorelSpace (EnrichedLowerSpace B m)

instance RelSignature.InfiniteRelExchangeableLaw.instStandardBorelSpaceEnrichedBoundarySpace {S : RelSignature} [Countable S.Srt] [Countable S.Rel] {M : S.InfiniteRelExchangeableLaw} (B : CoherentBasis M) (m : ℕ) (A : Finset ((s : S.Srt) × S.Vinfinite s)) : StandardBorelSpace (EnrichedBoundarySpace B m A)

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.

noncomputable def RelSignature.InfiniteRelExchangeableLaw.enrichedLowerMap {S : RelSignature} {M : S.InfiniteRelExchangeableLaw} (B : CoherentBasis M) (m : ℕ) : S.RelStructure S.Vinfinite × AustinBaseSpace S m → EnrichedLowerSpace B m

The lower factor, extended by the base.

Equations

• RelSignature.InfiniteRelExchangeableLaw.enrichedLowerMap B m p = (B.lowerFactorMap m p.1, p.2)

noncomputable def RelSignature.InfiniteRelExchangeableLaw.enrichedBoundaryMap {S : RelSignature} {M : S.InfiniteRelExchangeableLaw} (B : CoherentBasis M) (m : ℕ) (A : Finset ((s : S.Srt) × S.Vinfinite s)) : S.RelStructure S.Vinfinite × AustinBaseSpace S m → EnrichedBoundarySpace B m A

The boundary at A, extended by the base.

Equations

• RelSignature.InfiniteRelExchangeableLaw.enrichedBoundaryMap B m A p = (B.boundaryMap A p.1, p.2)

noncomputable def RelSignature.InfiniteRelExchangeableLaw.enrichedLayerMap {S : RelSignature} {M : S.InfiniteRelExchangeableLaw} (B : CoherentBasis M) (m : ℕ) : S.RelStructure S.Vinfinite × AustinBaseSpace S m → B.RankLayerSpace m

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.

Equations

• RelSignature.InfiniteRelExchangeableLaw.enrichedLayerMap B m p = B.rankLayerMap m p.1

noncomputable def RelSignature.InfiniteRelExchangeableLaw.enrichedExactMap {S : RelSignature} {M : S.InfiniteRelExchangeableLaw} (B : CoherentBasis M) (m : ℕ) (A : Finset ((s : S.Srt) × S.Vinfinite s)) : S.RelStructure S.Vinfinite × AustinBaseSpace S m → B.ExactSpace A

The exact-anchor layer at A.

Equations

• RelSignature.InfiniteRelExchangeableLaw.enrichedExactMap B m A p = B.exactMap A p.1

theorem RelSignature.InfiniteRelExchangeableLaw.lowerToBoundary_comp_enrichedLowerMap {S : RelSignature} {M : S.InfiniteRelExchangeableLaw} (B : CoherentBasis M) {m : ℕ} {A : Finset ((s : S.Srt) × S.Vinfinite s)} (hA : A.card = m) : Prod.map (B.lowerToBoundaryProjection hA) id ∘ enrichedLowerMap B m = enrichedBoundaryMap B m A

First commuting law: projecting the extended lower factor to the boundary, leaving the base untouched, is the extended boundary map.

theorem RelSignature.InfiniteRelExchangeableLaw.rankLayerToExact_comp_enrichedLayerMap {S : RelSignature} {M : S.InfiniteRelExchangeableLaw} (B : CoherentBasis M) {m : ℕ} {A : Finset ((s : S.Srt) × S.Vinfinite s)} (hA : A.card = m) : B.rankLayerToExactProjection hA ∘ enrichedLayerMap B m = enrichedExactMap B m A

Second commuting law: the exact-anchor layer factors through the rank-m layer.

theorem RelSignature.InfiniteRelExchangeableLaw.measurable_enrichedLowerMap {S : RelSignature} {M : S.InfiniteRelExchangeableLaw} (B : CoherentBasis M) (m : ℕ) : Measurable (enrichedLowerMap B m)

theorem RelSignature.InfiniteRelExchangeableLaw.measurable_enrichedLayerMap {S : RelSignature} {M : S.InfiniteRelExchangeableLaw} (B : CoherentBasis M) (m : ℕ) : Measurable (enrichedLayerMap B m)

theorem RelSignature.InfiniteRelExchangeableLaw.map_forget_base {S : RelSignature} [Countable S.Srt] [Countable S.Rel] {M : S.InfiniteRelExchangeableLaw} {n : ℕ} (B : CoherentBasis M) {C : M.RankRepresentation n} (O : AustinEnrichedObject C) : MeasureTheory.Measure.map (fun (p : S.RelStructure S.Vinfinite × AustinBaseSpace S n) => ((enrichedLowerMap B n p).1, enrichedLayerMap B n p)) O.law = MeasureTheory.Measure.map (fun (X : S.RelStructure S.Vinfinite) => (B.lowerFactorMap n X, B.rankLayerMap n X)) ↑M.law

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 RelSignature.InfiniteRelExchangeableLaw.map_recombine {S : RelSignature} [Countable S.Srt] [Countable S.Rel] {M : S.InfiniteRelExchangeableLaw} {n : ℕ} (B : CoherentBasis M) {C : M.RankRepresentation n} (O : AustinEnrichedObject C) : MeasureTheory.Measure.map (⇑(B.lowerFactorSpaceSuccEquiv n).symm) (MeasureTheory.Measure.map (fun (p : S.RelStructure S.Vinfinite × AustinBaseSpace S n) => ((enrichedLowerMap B n p).1, enrichedLayerMap B n p)) O.law) = MeasureTheory.Measure.map (B.lowerFactorMap (n + 1)) ↑M.law

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.