Pooled latent geometry and the mixed action (R4 converse, #107)

Stage 1 of the pooled-latent extension gate: the law-free latent geometry over the pooled carrier. Everything here is the carrier-parametric core of Graphon.RelLatentGeometry instantiated at PoolVertex S, plus the restriction to the original-support latents that relates the pooled cube to the rank-n cube.

Contents

• PooledRankLatentIndex / PooledRankLatentSpace / pooledRankLatentSource — pooled supports below the rank, their cube, and its i.i.d. uniform source;
• pooledRankLatentRelabel — the action of the full pooled permutation family ∀ s, Equiv.Perm (PoolVertex S s), with identity and composition laws and exact source invariance;
• restrictOriginalLatents — the measurable restriction to latents indexed by original supports;
• restrictOriginalLatents_pooledRankLatentRelabel — the honest moved-window naturality: a mixed permutation does not commute with restriction to the original latents; what holds is that restricting after relabeling is restriction along the moved embedding. The split case is the corollary restrictOriginalLatents_sumCongr.

Deliberately absent: any law, RankRepresentation, recovery, screening, or coupling. Those enter at stages 2 and 3 of the gate.

The pooled latent cube

@[reducible, inline]

abbrev RelSignature.PooledRankLatentIndex (S : RelSignature) (n : ℕ) : Type u

Pooled supports of cardinality below n: supports drawn from the pooled carrier, mixing original and pool vertices freely.

Equations

• S.PooledRankLatentIndex n = S.LatentIndexOver S.PoolVertex n

@[reducible, inline]

abbrev RelSignature.PooledRankLatentSpace (S : RelSignature) (n : ℕ) : Type u

The pooled latent cube.

Equations

• S.PooledRankLatentSpace n = S.LatentSpaceOver S.PoolVertex n

noncomputable def RelSignature.pooledRankLatentSource (S : RelSignature) (n : ℕ) : MeasureTheory.Measure (S.PooledRankLatentSpace n)

The pooled latent source: independent uniforms on all pooled supports below n.

Equations

• S.pooledRankLatentSource n = S.latentSourceOver S.PoolVertex n

instance RelSignature.instIsProbabilityMeasurePooledRankLatentSpacePooledRankLatentSource {S : RelSignature} (n : ℕ) : MeasureTheory.IsProbabilityMeasure (S.pooledRankLatentSource n)

The full mixed action

noncomputable def RelSignature.pooledRankLatentRelabel {S : RelSignature} (ρ : (s : S.Srt) → Equiv.Perm (S.PoolVertex s)) (n : ℕ) : S.PooledRankLatentSpace n ≃ᵐ S.PooledRankLatentSpace n

The mixed pooled action on the latent cube, by the full sortwise permutation family of the pooled carrier — permutations moving vertices between the two halves included.

Equations

• RelSignature.pooledRankLatentRelabel ρ n = RelSignature.latentRelabelOver ρ n

@[simp]

theorem RelSignature.pooledRankLatentRelabel_apply {S : RelSignature} (ρ : (s : S.Srt) → Equiv.Perm (S.PoolVertex s)) (n : ℕ) (ω : S.PooledRankLatentSpace n) (A : S.PooledRankLatentIndex n) : (pooledRankLatentRelabel ρ n) ω A = ω ((latentIndexPerm ρ n) A)

@[simp]

theorem RelSignature.pooledRankLatentRelabel_one {S : RelSignature} (n : ℕ) : pooledRankLatentRelabel (fun (x : S.Srt) => 1) n = MeasurableEquiv.refl (S.PooledRankLatentSpace n)

theorem RelSignature.pooledRankLatentRelabel_comp {S : RelSignature} (ρ τ : (s : S.Srt) → Equiv.Perm (S.PoolVertex s)) (n : ℕ) : pooledRankLatentRelabel (fun (s : S.Srt) => ρ s * τ s) n = (pooledRankLatentRelabel ρ n).trans (pooledRankLatentRelabel τ n)

theorem RelSignature.pooledRankLatentSource_map_pooledRankLatentRelabel {S : RelSignature} [Countable S.Srt] (ρ : (s : S.Srt) → Equiv.Perm (S.PoolVertex s)) (n : ℕ) : MeasureTheory.Measure.map (⇑(pooledRankLatentRelabel ρ n)) (S.pooledRankLatentSource n) = S.pooledRankLatentSource n

Exact invariance of the pooled source under the full mixed action.

Restriction to the original-support latents

noncomputable def RelSignature.restrictOriginalLatents (S : RelSignature) (n : ℕ) : S.PooledRankLatentSpace n → S.RankLatentSpace n

Restriction to the original latents: read the pooled coordinates indexed by supports drawn from the original half. Its codomain is the rank-n cube itself, since RankLatentIndex is the carrier-parametric index at Vinfinite S.

Equations

• S.restrictOriginalLatents n = RelSignature.latentRestrictOver (fun (s : S.Srt) => S.originalVertex s) n

theorem RelSignature.measurable_restrictOriginalLatents {S : RelSignature} (n : ℕ) : Measurable (S.restrictOriginalLatents n)

@[simp]

theorem RelSignature.restrictOriginalLatents_apply {S : RelSignature} (n : ℕ) (ω : S.PooledRankLatentSpace n) (A : S.RankLatentIndex n) : S.restrictOriginalLatents n ω A = ω (latentIndexEmbed (fun (s : S.Srt) => S.originalVertex s) n A)

theorem RelSignature.restrictOriginalLatents_pooledRankLatentRelabel {S : RelSignature} (ρ : (s : S.Srt) → Equiv.Perm (S.PoolVertex s)) (n : ℕ) : S.restrictOriginalLatents n ∘ ⇑(pooledRankLatentRelabel ρ n) = latentRestrictOver (fun (s : S.Srt) => (S.originalVertex s).trans (Equiv.toEmbedding (ρ s))) n

The moved-window naturality. Restricting to the original latents after a pooled relabeling is restriction along the moved embedding. This holds for every pooled permutation, mixed ones included — and it is the honest statement: a permutation carrying original vertices into the pool half does not commute with restriction to the original latents, and no such law is available.

theorem RelSignature.restrictOriginalLatents_sumCongr {S : RelSignature} (σ : (s : S.Srt) → Equiv.Perm (S.Vinfinite s)) (n : ℕ) : S.restrictOriginalLatents n ∘ ⇑(pooledRankLatentRelabel (fun (s : S.Srt) => Equiv.sumCongr (σ s) (Equiv.refl (S.Vinfinite s))) n) = ⇑(latentRelabelOver σ n) ∘ S.restrictOriginalLatents n

The split corollary: a permutation of the original half alone commutes with restriction to the original latents, acting there through the carrier-parametric action at Vinfinite S.