The split-equivariant extension lift (R4 converse, #107)

The joint law of a rank-n representation and a stationary extension, glued over their common structure marginal: (X, U_{<n}) from the representation, X⁺ from the extension, coupled by the relative joining over X.

This lift is split-equivariant, and only split-equivariant. The invariance proved here is under the split diagonal action — σ on X, rankLatentRelabel σ n on the old latents, Equiv.sumCongr (σ s) 1 on X⁺. Mixed pooled permutations do not act on this object: for a boundary-crossing ρ, restrictOriginal (relabel ρ X⁺) reads pool vertices and is not relabel σ (restrictOriginal X⁺) for any original-carrier σ — the factor square of the two-sided transport does not exist — and RankLatentSpace S n indexes latents by original-carrier supports only, so a boundary-crossing permutation has no action on the old latents at all. Obtaining a pooled latent law with a genuine mixed action is the separate pooled-latent extension gate on #107, not this file.

The joining's conditional clause (X, U_{<n}) ⊥⊥ X⁺ ∣ σ(X) is recorded; it does not manufacture correlated latents (guard 3): whatever the pool knows beyond X is untouched, and whatever U_{<n} encodes beyond X says nothing about X⁺.

Recovery and screening need no new transfer infrastructure: both are statements about the (X, U_{<n})-marginal, that marginal is exactly the representation's coupling (extensionLift_map_fst), and consumers transport along Prod.fst with the existing measure-preserving/comap machinery.

noncomputable def RelSignature.InfiniteRelExchangeableLaw.RankRepresentation.extensionLift {S : RelSignature} [Countable S.Srt] [Countable S.Rel] {M : S.InfiniteRelExchangeableLaw} {n : ℕ} (C : M.RankRepresentation n) (E : StationaryExtension M) : MeasureTheory.Measure ((S.RelStructure S.Vinfinite × S.RankLatentSpace n) × S.RelStructure S.PoolVertex)

The extension lift: the representation's coupling and the extended law, glued by the relative joining over their common structure marginal.

Equations

• C.extensionLift E = ProbabilityTheory.relativeFactorCoupling C.P (↑E.law) Prod.fst S.restrictOriginal

theorem RelSignature.InfiniteRelExchangeableLaw.RankRepresentation.extensionLift_factor_eq {S : RelSignature} [Countable S.Srt] [Countable S.Rel] {M : S.InfiniteRelExchangeableLaw} {n : ℕ} (C : M.RankRepresentation n) (E : StationaryExtension M) : MeasureTheory.Measure.map S.restrictOriginal ↑E.law = MeasureTheory.Measure.map Prod.fst C.P

The common-factor identity: both inputs have the law as their structure marginal.

theorem RelSignature.InfiniteRelExchangeableLaw.RankRepresentation.extensionLift_map_fst {S : RelSignature} [Countable S.Srt] [Countable S.Rel] {M : S.InfiniteRelExchangeableLaw} {n : ℕ} (C : M.RankRepresentation n) (E : StationaryExtension M) : MeasureTheory.Measure.map Prod.fst (C.extensionLift E) = C.P

The first marginal of the lift is the representation's coupling. Recovery and screening pull back through this identity — no new transfer infrastructure is needed; consumers use the existing measure-preserving/comap transport along Prod.fst.

theorem RelSignature.InfiniteRelExchangeableLaw.RankRepresentation.extensionLift_map_snd {S : RelSignature} [Countable S.Srt] [Countable S.Rel] {M : S.InfiniteRelExchangeableLaw} {n : ℕ} (C : M.RankRepresentation n) (E : StationaryExtension M) : MeasureTheory.Measure.map Prod.snd (C.extensionLift E) = ↑E.law

The second marginal of the lift is the extended law.

instance RelSignature.InfiniteRelExchangeableLaw.RankRepresentation.instIsProbabilityMeasureProdRelStructureVinfiniteRankLatentSpacePoolVertexExtensionLift {S : RelSignature} [Countable S.Srt] [Countable S.Rel] {M : S.InfiniteRelExchangeableLaw} {n : ℕ} (C : M.RankRepresentation n) (E : StationaryExtension M) : MeasureTheory.IsProbabilityMeasure (C.extensionLift E)

theorem RelSignature.InfiniteRelExchangeableLaw.RankRepresentation.extensionLift_commonFactor {S : RelSignature} [Countable S.Srt] [Countable S.Rel] {M : S.InfiniteRelExchangeableLaw} {n : ℕ} (C : M.RankRepresentation n) (E : StationaryExtension M) : Prod.fst ∘ Prod.fst =ᵐ[C.extensionLift E] S.restrictOriginal ∘ Prod.snd

The common-factor identity — the defining "glued over the same X" law: the structure read off the representation pair agrees almost everywhere with the original restriction of the extended array. Exact marginals plus conditional independence do not expose this; it is the clause that says both coordinates carry one and the same X.

theorem RelSignature.InfiniteRelExchangeableLaw.RankRepresentation.extensionLift_map_split {S : RelSignature} [Countable S.Srt] [Countable S.Rel] {M : S.InfiniteRelExchangeableLaw} {n : ℕ} (C : M.RankRepresentation n) (E : StationaryExtension M) (σ : ↥S.FinSuppPerm) : MeasureTheory.Measure.map (Prod.map (Prod.map (RelStructure.relabel ↑σ) ⇑(rankLatentRelabel σ n)) (RelStructure.relabel fun (s : S.Srt) => Equiv.sumCongr (↑σ s) 1)) (C.extensionLift E) = C.extensionLift E

Split-diagonal invariance — and deliberately nothing stronger: σ acts on the structure, on the old latents, and on the original half of the pooled carrier, fixing the pool half. Mixed pooled permutations do not act on this object; see the module header.

theorem RelSignature.InfiniteRelExchangeableLaw.RankRepresentation.condIndepFun_fst_snd_extensionLift {S : RelSignature} [Countable S.Srt] [Countable S.Rel] {M : S.InfiniteRelExchangeableLaw} {n : ℕ} (C : M.RankRepresentation n) (E : StationaryExtension M) : ProbabilityTheory.CondIndepFun (MeasurableSpace.comap (Prod.fst ∘ Prod.fst) inferInstance) ⋯ Prod.fst Prod.snd (C.extensionLift E)

The joining's conditional clause: the representation pair and the extended array are conditionally independent given the common structure factor — a variable on the lift space. This does not manufacture correlated latents: it says the pool's surplus over X and the old latents' surplus over X are mutually uninformative, nothing more.