Joint invariance under sortwise self-injections (R4 converse, #107)

The isolated proof risk of the pooled-latent extension gate: RankRepresentation.invariant is stated for finitely supported permutations, but the cheap poolVertexEquiv construction of a pooled object needs the joint law to be invariant under arbitrary sortwise self-injections. This file closes that gap by finite-cylinder extensionality, once and for all, so that full mixed pooled invariance later costs no additional mathematics.

Contents

• rankLatentIndexInj / rankLatentReindex — the latent action of a sortwise self-injection. Only injectivity is used (a support keeps its cardinality), so this extends rankLatentIndexEquiv / rankLatentRelabel from permutations to injections; on a permutation the two agree (rankLatentReindex_toEmbedding).
• exists_finSuppPerm_agree_on_finset — a sortwise self-injection agrees with some finitely supported permutation on any finite set of tagged vertices.
• ext_of_prod_cylinders — joint extensionality: two finite measures on RelStructure × RankLatentSpace agreeing on all rectangles of coordinate cylinders are equal.
• RankRepresentation.map_prodMap_restrict_self — the theorem: the joint law is invariant under the diagonal action of any sortwise self-injection.

No finiteness hypothesis beyond ambient countability

Testing measure equality on coordinate cylinders — finitely many RelCoords and finitely many RankLatentIndexes — is what keeps [Fintype S.Srt] out of this file; nothing here is assumed about the sort type beyond RankRepresentation's ambient [Countable S.Srt]. Their combined vertex support is a single finite Finset (Σ s, Vinfinite S s), so only finitely many sorts are active, and a self-injection is matched there by a finitely supported permutation: extend it separately on each active sort, take the identity elsewhere, and take the maximum of the finitely many support bounds. The coarser cylinders S family would not do — a cylinder there is an arbitrary measurable event after restrictFin m, whose finite level can still involve every sort, forcing a uniform all-sort bound that no self-injection need admit.

The latent action of a sortwise self-injection

noncomputable def RelSignature.rankLatentIndexInj {S : RelSignature} (ι : (s : S.Srt) → S.Vinfinite s ↪ S.Vinfinite s) (n : ℕ) : S.RankLatentIndex n → S.RankLatentIndex n

The index action of a sortwise self-injection: push a support forward. Injectivity alone preserves cardinality, so this lands in the same rank.

Equations

• RelSignature.rankLatentIndexInj ι n A = ⟨Finset.image (Sigma.map id fun (s : S.Srt) => ⇑(ι s)) ↑A, ⋯⟩

@[simp]

theorem RelSignature.rankLatentIndexInj_coe {S : RelSignature} (ι : (s : S.Srt) → S.Vinfinite s ↪ S.Vinfinite s) (n : ℕ) (A : S.RankLatentIndex n) : ↑(rankLatentIndexInj ι n A) = Finset.image (Sigma.map id fun (s : S.Srt) => ⇑(ι s)) ↑A

noncomputable def RelSignature.rankLatentReindex {S : RelSignature} (ι : (s : S.Srt) → S.Vinfinite s ↪ S.Vinfinite s) (n : ℕ) : S.RankLatentSpace n → S.RankLatentSpace n

The latent action of a sortwise self-injection: reindex the cube by pushing supports forward. For a permutation this is rankLatentRelabel.

Equations

• RelSignature.rankLatentReindex ι n ω A = ω (RelSignature.rankLatentIndexInj ι n A)

theorem RelSignature.measurable_rankLatentReindex {S : RelSignature} (ι : (s : S.Srt) → S.Vinfinite s ↪ S.Vinfinite s) (n : ℕ) : Measurable (rankLatentReindex ι n)

Agreement of an injection with a permutation on a finite support

theorem RelSignature.rankLatentIndexInj_eq_of_agree {S : RelSignature} {ι : (s : S.Srt) → S.Vinfinite s ↪ S.Vinfinite s} {σ : ↥S.FinSuppPerm} {n : ℕ} {A : S.RankLatentIndex n} (h : ∀ v ∈ ↑A, (ι v.fst) v.snd = (↑σ v.fst) v.snd) : rankLatentIndexInj ι n A = (rankLatentIndexEquiv σ n) A

If a sortwise self-injection and a permutation agree on every vertex of a support, they send that support to the same index.

@[simp]

theorem RelSignature.rankLatentReindex_toEmbedding {S : RelSignature} (σ : ↥S.FinSuppPerm) (n : ℕ) : rankLatentReindex (fun (s : S.Srt) => Equiv.toEmbedding (↑σ s)) n = ⇑(rankLatentRelabel σ n)

theorem RelSignature.exists_finSuppPerm_agree_on_finset {S : RelSignature} (ι : (s : S.Srt) → S.Vinfinite s ↪ S.Vinfinite s) (V : Finset ((s : S.Srt) × S.Vinfinite s)) : ∃ (σ : ↥S.FinSuppPerm), ∀ v ∈ V, (↑σ v.fst) v.snd = (ι v.fst) v.snd

Finite-support agreement: a sortwise self-injection agrees with some finitely supported permutation on any finite set of tagged vertices. Only the finitely many sorts occurring in that set are active; every other sort takes the identity, so the support bounds to be maximized are finite in number — no finiteness hypothesis on the sort type is needed.

Joint cylinder extensionality

@[reducible, inline]

abbrev RelSignature.structureCylinders (S : RelSignature) : Set (Set (S.RelStructure S.Vinfinite))

The coordinate cylinders of the structure cube: finitely many RelCoords constrained.

Equations

• S.structureCylinders = MeasureTheory.measurableCylinders fun (x : S.RelCoord S.Vinfinite) => Bool

@[reducible, inline]

abbrev RelSignature.latentCylinders (S : RelSignature) (n : ℕ) : Set (Set (S.RankLatentSpace n))

The coordinate cylinders of the latent cube: finitely many latent indices constrained.

Equations

• S.latentCylinders n = MeasureTheory.measurableCylinders fun (x : S.RankLatentIndex n) => ℝ

theorem RelSignature.isCountablySpanning_structureCylinders {S : RelSignature} : IsCountablySpanning S.structureCylinders

theorem RelSignature.isCountablySpanning_latentCylinders {S : RelSignature} (n : ℕ) : IsCountablySpanning (S.latentCylinders n)

theorem RelSignature.ext_of_prod_cylinders {S : RelSignature} {n : ℕ} {μ ν : MeasureTheory.Measure (S.RelStructure S.Vinfinite × S.RankLatentSpace n)} [MeasureTheory.IsFiniteMeasure μ] (h : ∀ A ∈ S.structureCylinders, ∀ B ∈ S.latentCylinders n, μ (A ×ˢ B) = ν (A ×ˢ B)) (huniv : μ Set.univ = ν Set.univ) : μ = ν

Joint extensionality: two finite measures on the structure–latent product agreeing on every rectangle of coordinate cylinders are equal.

The theorem

theorem RelSignature.InfiniteRelExchangeableLaw.RankRepresentation.map_prodMap_restrict_self {S : RelSignature} [Countable S.Srt] [Countable S.Rel] {M : S.InfiniteRelExchangeableLaw} {n : ℕ} (C : M.RankRepresentation n) (ι : (s : S.Srt) → S.Vinfinite s ↪ S.Vinfinite s) : MeasureTheory.Measure.map (Prod.map (RelStructure.restrict ι) (rankLatentReindex ι n)) C.P = C.P

Joint invariance under an arbitrary sortwise self-injection. RankRepresentation.invariant gives this only for finitely supported permutations; finite-cylinder extensionality upgrades it to every self-injection, because on any single joint coordinate cylinder the injection agrees with some finitely supported permutation. No finiteness hypothesis beyond RankRepresentation's ambient [Countable S.Srt]: the cylinder's combined vertex support is finite, hence touches only finitely many sorts. This is the theorem the cheap pooled construction rests on.

Bridge to the carrier-parametric core

theorem RelSignature.rankLatentIndexInj_eq_latentIndexEmbed {S : RelSignature} (ι : (s : S.Srt) → S.Vinfinite s ↪ S.Vinfinite s) (n : ℕ) (A : S.RankLatentIndex n) : rankLatentIndexInj ι n A = latentIndexEmbed ι n A

theorem RelSignature.rankLatentReindex_eq_latentRestrictOver {S : RelSignature} (ι : (s : S.Srt) → S.Vinfinite s ↪ S.Vinfinite s) (n : ℕ) : rankLatentReindex ι n = latentRestrictOver ι n

Bridge: the self-injection reindexing of Graphon.RelRankInjectionInvariance is restriction along that injection in the carrier-parametric core. This is where #194's invariance theorem meets the generic pooled API.