The joint restriction theorem for a pooled rank extension (R4 converse, #107)

Stage 3 of the pooled-latent extension gate, organizing result:

PooledRankExtension.map_restrict_embedding — for every sortwise embedding e : ∀ s, Vinfinite S s ↪ PoolVertex S s, restricting the extension jointly along e returns the representation exactly:

Q.law.map (Prod.map (RelStructure.restrict e) (latentRestrictOver e n)) = C.P

This is joint, not a structure marginal: the structure and the latents are restricted along the same embedding, so it recovers the joint (X, U_{<n}) law and says strictly more than a structure-only window theorem.

Cancelling that restriction at the canonical embedding gives PooledRankExtension.law_eq, a uniqueness theorem: every pooled rank extension is the cheap one, (C.pooledExtension). The four route-neutral consequences of the gate are transports through that single identity:

• PooledRankExtension.map_snd — the pooled latent marginal is the pooled i.i.d. source;
• PooledRankExtension.toStationaryExtension — the structure marginal is a StationaryExtension M;
• PooledRankExtension.lower_recovers — local recovery on every pooled support below rank n, the decoder conjugated through the local and block measurable equivalences;
• PooledRankExtension.screening — screening on every pooled support of rank n, assembled from condIndepFun_comp_measurePreserving, CondIndepFun.comp on the codomains, and CondIndepFun.congr_cond with comap_measurableEquiv_comp on the conditioning algebra.

Nothing route-specific appears: no fresh rank-n latent extraction and nothing at rank n + 1.

The joint restriction theorem is proved by joint-cylinder extensionality together with finite agreement by a mixed pooled permutation. On a joint cylinder the combined vertex support is finite; the partial assignment originalVertex v ↦ e v on it is a finite partial injection of the pooled carrier, since both embeddings are injective, so it extends to a pooled permutation ρ with ρ (ov v) = e v there. Both restrictions then read the same moved coordinates, and the full mixed invariance of the extension absorbs ρ. Choosing ρ separately on each sort is exactly what the full action permits — no finite-support or uniform-bound issue arises.

theorem RelSignature.InfiniteRelExchangeableLaw.exists_poolPerm_agree {S : RelSignature} (e : (s : S.Srt) → S.Vinfinite s ↪ S.PoolVertex s) (V : Finset ((s : S.Srt) × S.Vinfinite s)) : ∃ (ρ : (s : S.Srt) → Equiv.Perm (S.PoolVertex s)), ∀ v ∈ V, (ρ v.fst) ((S.originalVertex v.fst) v.snd) = (e v.fst) v.snd

Finite agreement by a pooled permutation: any sortwise embedding into the pooled carrier agrees with a pooled permutation composed with the original embedding, on any finite set of original vertices. The permutation is chosen independently on each sort, which the full mixed action allows.

theorem RelSignature.InfiniteRelExchangeableLaw.PooledRankExtension.map_restrict_embedding {S : RelSignature} [Countable S.Srt] [Countable S.Rel] {M : S.InfiniteRelExchangeableLaw} {n : ℕ} {C : M.RankRepresentation n} (Q : PooledRankExtension C) (e : (s : S.Srt) → S.Vinfinite s ↪ S.PoolVertex s) : MeasureTheory.Measure.map (Prod.map (RelStructure.restrict e) (latentRestrictOver e n)) ↑Q.law = C.P

The joint restriction theorem. Restricting a pooled rank extension along any sortwise embedding into the pooled carrier — structure and latents together — returns the representation exactly. Mixed windows are included: the embedding may land anywhere in the pooled carrier.

The transport characterization

theorem RelSignature.InfiniteRelExchangeableLaw.PooledRankExtension.map_poolVertexEquiv {S : RelSignature} [Countable S.Srt] [Countable S.Rel] {M : S.InfiniteRelExchangeableLaw} {n : ℕ} {C : M.RankRepresentation n} (Q : PooledRankExtension C) : MeasureTheory.Measure.map (Prod.map (RelStructure.restrict fun (s : S.Srt) => (S.poolVertexEquiv s).symm.toEmbedding) (latentRestrictOver (fun (s : S.Srt) => (S.poolVertexEquiv s).symm.toEmbedding) n)) ↑Q.law = C.P

Transport characterization: identifying the pooled carrier with the original one by poolVertexEquiv carries any pooled rank extension back to the representation, jointly. This is the organizing theorem at the canonical embedding, and it is stated before recovery or screening deliberately — it isolates the map directions while the claim is still just an equality of joint laws.

The canonical law identity

noncomputable def RelSignature.InfiniteRelExchangeableLaw.pooledJointEquiv (S : RelSignature) (n : ℕ) : S.RelStructure S.PoolVertex × S.PooledRankLatentSpace n ≃ᵐ S.RelStructure S.Vinfinite × S.RankLatentSpace n

The canonical joint identification of the pooled objects with the original ones, bundled as a measurable equivalence: poolVertexEquiv on the structure and its latent transport. Its forward map is exactly the restriction appearing in map_poolVertexEquiv, which is what lets that theorem be cancelled rather than merely stated.

Equations

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

theorem RelSignature.InfiniteRelExchangeableLaw.pooledJointEquiv_coe {S : RelSignature} {n : ℕ} : ⇑(pooledJointEquiv S n) = Prod.map (RelStructure.restrict fun (s : S.Srt) => (S.poolVertexEquiv s).symm.toEmbedding) (latentRestrictOver (fun (s : S.Srt) => (S.poolVertexEquiv s).symm.toEmbedding) n)

theorem RelSignature.InfiniteRelExchangeableLaw.pooledJointEquiv_symm_coe {S : RelSignature} {n : ℕ} : ⇑(pooledJointEquiv S n).symm = RankRepresentation.pooledTransport

theorem RelSignature.InfiniteRelExchangeableLaw.PooledRankExtension.law_eq {S : RelSignature} [Countable S.Srt] [Countable S.Rel] {M : S.InfiniteRelExchangeableLaw} {n : ℕ} {C : M.RankRepresentation n} (Q : PooledRankExtension C) : ↑Q.law = ↑C.pooledExtension.law

The canonical law identity: a pooled rank extension is determined — it is the cheap one. Every marginal, StationaryExtension, recovery and screening statement about a pooled extension is therefore a transport of the corresponding statement about C.P, rather than a separate measure argument.

theorem RelSignature.InfiniteRelExchangeableLaw.PooledRankExtension.measurePreserving_pooledJointEquiv {S : RelSignature} [Countable S.Srt] [Countable S.Rel] {M : S.InfiniteRelExchangeableLaw} {n : ℕ} {C : M.RankRepresentation n} (Q : PooledRankExtension C) : MeasureTheory.MeasurePreserving (⇑(pooledJointEquiv S n)) (↑Q.law) C.P

The canonical identification is measure-preserving from a pooled extension to the representation. This is the handle for transporting conditional-independence statements: composing with a measure-preserving map pulls C.P-statements back to Q.law, so nothing has to be pushed forward and no further conditional-expectation theorem is needed.

Consequence 1: the pooled latent marginal

theorem RelSignature.InfiniteRelExchangeableLaw.PooledRankExtension.map_snd {S : RelSignature} [Countable S.Srt] [Countable S.Rel] {M : S.InfiniteRelExchangeableLaw} {n : ℕ} {C : M.RankRepresentation n} (Q : PooledRankExtension C) : MeasureTheory.Measure.map Prod.snd ↑Q.law = S.pooledRankLatentSource n

The pooled latent marginal is the pooled i.i.d. source. A transport of C.map_snd through the canonical identity, with the source transport doing the work on the latent factor.

Consequence 2: the structure marginal is a stationary extension

noncomputable def RelSignature.InfiniteRelExchangeableLaw.PooledRankExtension.toStationaryExtension {S : RelSignature} [Countable S.Srt] [Countable S.Rel] {M : S.InfiniteRelExchangeableLaw} {n : ℕ} {C : M.RankRepresentation n} (Q : PooledRankExtension C) : StationaryExtension M

The structure marginal of a pooled rank extension is a stationary extension of the law. Both fields are the corresponding pooled field composed with Prod.fst.

Equations

• Q.toStationaryExtension = { law := ⟨MeasureTheory.Measure.map Prod.fst ↑Q.law, ⋯⟩, map_restrictOriginal := ⋯, invariant := ⋯ }

Consequence 3: local recovery on pooled supports

theorem RelSignature.InfiniteRelExchangeableLaw.PooledRankExtension.lower_recovers {S : RelSignature} [Countable S.Srt] [Countable S.Rel] {M : S.InfiniteRelExchangeableLaw} {n : ℕ} {C : M.RankRepresentation n} (Q : PooledRankExtension C) (A : Finset ((s : S.Srt) × S.PoolVertex s)) (hA : A.card < n) : ∃ (g : LocalLatentSpaceOver S.PoolVertex A n → BlockSpaceOver S.PoolVertex A), Measurable g ∧ blockMapOver A ∘ Prod.fst =ᵐ[↑Q.law] g ∘ localLatentsOver A n ∘ Prod.snd

Local recovery holds on every pooled support below rank n — mixed supports included. C.lower_recovers is pulled back along the canonical identification, and the decoder is conjugated through the local and block measurable equivalences. The only almost-everywhere step is the transported identity itself.

Consequence 4: screening on pooled supports

theorem RelSignature.InfiniteRelExchangeableLaw.PooledRankExtension.screening {S : RelSignature} [Countable S.Srt] [Countable S.Rel] {M : S.InfiniteRelExchangeableLaw} {n : ℕ} {C : M.RankRepresentation n} (Q : PooledRankExtension C) (A : Finset ((s : S.Srt) × S.PoolVertex s)) (hA : A.card = n) : ProbabilityTheory.CondIndepFun (MeasurableSpace.comap (localLatentsOver A n ∘ Prod.snd) inferInstance) ⋯ (blockMapOver A ∘ Prod.fst) (restObservationOver n A) ↑Q.law

Screening holds on every pooled support of rank n — mixed supports included. Pure assembly: pull C.screening back through the canonical identification, strip the output equivalences with CondIndepFun.comp, and straighten the conditioning algebra with CondIndepFun.congr_cond. No conditional-expectation reasoning appears.