The stationary extension (R4 converse, #107)

Layer 2 of the approved contract: the extended law on the pooled carrier. The primitive is an extended law, not an independent joining — the pool observations remain jointly distributed with the original array through the same structure, and no relative-independence claim of any kind is made (an independent pool would recreate the defect of the rejected factor coupling: nothing correlated to offer).

Contents

• StationaryExtension — the minimal structure: a probability law on the pooled structure space whose original restriction is the law and which is invariant under every sortwise permutation of the pooled carrier (mixed permutations included — the load-bearing quantifier);
• StationaryExtension.law_map_restrict_window — the exact mixed-window marginal: the restriction along any sortwise finite embedding into the pooled carrier has the rank-n marginal of the original law. The explicit acceptance test of the contract; this is what the polling and successor consumers cite;
• StationaryExtension.extensionCoupling with exact map_fst / map_snd — the induced coupling of the original restriction with the whole extended array. The shared-array property is definitional;
• InfiniteRelExchangeableLaw.nonempty_stationaryExtension — the cheap existence theorem: both summands together are again a countably infinite carrier, so the law transports along poolVertexEquiv. Existence is deliberately cheap and is not the induction step: the hard theorem is extracting correlated auxiliary latents with recovery and screening from an extension, and that theorem is not touched here.

All measure identities in this file are exact; nothing is almost-everywhere.

The stationary extension

structure RelSignature.StationaryExtension {S : RelSignature} (M : S.InfiniteRelExchangeableLaw) : Type u

A stationary extension of an exchangeable law: a probability law on the pooled structure space whose restriction to the original vertices is the law, invariant under every sortwise permutation of the pooled carrier — mixed permutations included, which is the load-bearing quantifier for polling.

Deliberately minimal. Latent recovery, screening, conditional independence, a coherent basis, RankRepresentation, and any independence of the pool from the original array are all excluded: they belong to the theorem extracting higher-rank latents from an extension, and an independence clause would recreate the defect of the rejected relative-factor coupling.

• law : MeasureTheory.ProbabilityMeasure (S.RelStructure S.PoolVertex)

  The extended law on the pooled structure space.

• map_restrictOriginal : MeasureTheory.Measure.map S.restrictOriginal ↑self.law = ↑M.law

  Its restriction to the original vertices is the law.

• invariant (ρ : (s : S.Srt) → Equiv.Perm (S.PoolVertex s)) : MeasureTheory.Measure.map (RelStructure.relabel ρ) ↑self.law = ↑self.law

  Invariance under every sortwise permutation of the pooled carrier — including permutations moving vertices between the original and pool halves.

theorem RelSignature.StationaryExtension.law_map_restrict_window {S : RelSignature} {M : S.InfiniteRelExchangeableLaw} (E : StationaryExtension M) {n : S.Srt → ℕ} (e : (s : S.Srt) → Fin (n s) ↪ S.PoolVertex s) : MeasureTheory.Measure.map (RelStructure.restrict e) ↑E.law = MeasureTheory.Measure.map (RelStructure.restrictFin n) ↑M.law

The exact mixed-window marginal — the contract's explicit acceptance test: the restriction of the extension along any sortwise finite embedding into the pooled carrier — windows mixing original and pool vertices freely — is the rank-n marginal of the original law. Proof: a permutation of the pooled carrier moves the window into the original half (restrict_relabel, the moved-window law), invariance absorbs it, and the original restriction then computes the marginal by law_map_restrict.

The induced coupling

noncomputable def RelSignature.StationaryExtension.extensionCoupling {S : RelSignature} {M : S.InfiniteRelExchangeableLaw} (E : StationaryExtension M) : MeasureTheory.ProbabilityMeasure (S.RelStructure S.Vinfinite × S.RelStructure S.PoolVertex)

The induced coupling of the original restriction with the whole extended array. The shared-array property is definitional: both coordinates are read off the same structure. No independence between them is claimed — that exclusion is the point of the design.

Equations

• E.extensionCoupling = ⟨MeasureTheory.Measure.map (fun (X : S.RelStructure S.PoolVertex) => (S.restrictOriginal X, X)) ↑E.law, ⋯⟩

theorem RelSignature.StationaryExtension.extensionCoupling_map_fst {S : RelSignature} {M : S.InfiniteRelExchangeableLaw} (E : StationaryExtension M) : MeasureTheory.Measure.map Prod.fst ↑E.extensionCoupling = ↑M.law

The first marginal of the induced coupling is the original law. Exact.

theorem RelSignature.StationaryExtension.extensionCoupling_map_snd {S : RelSignature} {M : S.InfiniteRelExchangeableLaw} (E : StationaryExtension M) : MeasureTheory.Measure.map Prod.snd ↑E.extensionCoupling = ↑E.law

The second marginal of the induced coupling is the extended law. Exact.

The cheap existence theorem

theorem RelSignature.InfiniteRelExchangeableLaw.nonempty_stationaryExtension {S : RelSignature} (M : S.InfiniteRelExchangeableLaw) : Nonempty (StationaryExtension M)

Every exchangeable law has a stationary extension — deliberately cheap: both summands together are again a countably infinite carrier, so the law transports along the fixed sortwise identification. This is not the induction step. The hard theorem is extracting correlated auxiliary latents with recovery and screening from an extension; nothing here touches it, and mistaking this construction for progress on the induction would repeat the RankCoding failure.