Rank-indexed latent sources (R4 converse piece 3, #107)

The latent-side infrastructure for the coupled rank induction. At rank n the source has one independent uniform coordinate for every finite tagged support of cardinality strictly below n (so the empty support appears exactly when 0 < n). This is deliberately separate from CoherentBasis.LowerFactorSpace: the latent space is an ℝ-valued cube indexed by tagged supports, whereas the factor space is a Bool-valued cube indexed by basis expressions. A rank coding is the later map relating the two.

The nesting maps and their cocycle are definitional. Sortwise relabelings act through genuine index equivalences and preserve the i.i.d. source. Rank one is identified measurably and measure-preservingly with a single uniform. Finally, the successor source splits into the old latents and the fresh rank-n layer; this split is included here so the coherent-randomization step does not have to rediscover the latent-side decomposition.

@[reducible]

def RelSignature.RankLatentIndex (S : RelSignature) (n : ℕ) : Type u_1

Finite tagged supports of cardinality strictly below n; this includes the empty support when 0 < n.

Equations

• S.RankLatentIndex n = S.LatentIndexOver S.Vinfinite n

instance RelSignature.instCountableRankLatentIndexOfSrt {S : RelSignature} [Countable S.Srt] (n : ℕ) : Countable (S.RankLatentIndex n)

def RelSignature.rankLatentEmpty {S : RelSignature} : S.RankLatentIndex 1

The empty support, regarded as the unique rank-one latent index.

Equations

• RelSignature.rankLatentEmpty = ⟨∅, RelSignature.rankLatentEmpty._proof_1⟩

@[implicit_reducible]

instance RelSignature.instUniqueRankLatentIndexOfNatNat {S : RelSignature} : Unique (S.RankLatentIndex 1)

Equations

• RelSignature.instUniqueRankLatentIndexOfNatNat = { default := RelSignature.rankLatentEmpty, uniq := ⋯ }

@[reducible, inline]

abbrev RelSignature.RankLatentSpace (S : RelSignature) (n : ℕ) : Type u_1

The rank-n latent space: one real-valued coordinate per support of rank below n.

Equations

• S.RankLatentSpace n = (S.RankLatentIndex n → ℝ)

instance RelSignature.instStandardBorelSpaceRankLatentSpaceOfCountableSrt {S : RelSignature} [Countable S.Srt] (n : ℕ) : StandardBorelSpace (S.RankLatentSpace n)

noncomputable def RelSignature.rankLatentSource (S : RelSignature) (n : ℕ) : MeasureTheory.Measure (S.RankLatentSpace n)

The rank-n latent source: independent uniform01 coordinates on all supports below n.

Equations

• S.rankLatentSource n = MeasureTheory.iidUniformSource (S.RankLatentIndex n)

instance RelSignature.instIsProbabilityMeasureRankLatentSpaceRankLatentSource {S : RelSignature} (n : ℕ) : MeasureTheory.IsProbabilityMeasure (S.rankLatentSource n)

Rank nesting

def RelSignature.rankLatentIndexEmbedding {S : RelSignature} {n m : ℕ} (h : n ≤ m) : S.RankLatentIndex n → S.RankLatentIndex m

Inclusion of the supports below rank n among those below rank m.

Equations

• RelSignature.rankLatentIndexEmbedding h A = ⟨↑A, ⋯⟩

def RelSignature.rankLatentProjection {S : RelSignature} {n m : ℕ} (h : n ≤ m) : S.RankLatentSpace m → S.RankLatentSpace n

Restriction of a rank-m latent assignment to ranks below n.

Equations

• RelSignature.rankLatentProjection h ω = ω ∘ RelSignature.rankLatentIndexEmbedding h

theorem RelSignature.measurable_rankLatentProjection {S : RelSignature} [Countable S.Srt] {n m : ℕ} (h : n ≤ m) : Measurable (rankLatentProjection h)

theorem RelSignature.rankLatentProjection_apply {S : RelSignature} {n m : ℕ} (h : n ≤ m) (ω : S.RankLatentSpace m) (A : S.RankLatentIndex n) : rankLatentProjection h ω A = ω (rankLatentIndexEmbedding h A)

Rank restriction reads the same coordinates on the source.

theorem RelSignature.rankLatentProjection_comp {S : RelSignature} {n m k : ℕ} (hnm : n ≤ m) (hmk : m ≤ k) : rankLatentProjection hnm ∘ rankLatentProjection hmk = rankLatentProjection ⋯

The rank projections form a strict cocycle.

Relabeling action

noncomputable def RelSignature.rankLatentIndexEquiv {S : RelSignature} (σ : ↥S.FinSuppPerm) (n : ℕ) : S.RankLatentIndex n ≃ S.RankLatentIndex n

A finitely supported sortwise relabeling permutes the supports below each rank.

Equations

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

@[simp]

theorem RelSignature.rankLatentIndexEquiv_apply_coe {S : RelSignature} (σ : ↥S.FinSuppPerm) (n : ℕ) (A : S.RankLatentIndex n) : ↑((rankLatentIndexEquiv σ n) A) = Finset.image (Sigma.map id fun (s : S.Srt) => ⇑(↑σ s)) ↑A

@[simp]

theorem RelSignature.rankLatentIndexEquiv_one {S : RelSignature} (n : ℕ) : rankLatentIndexEquiv 1 n = Equiv.refl (S.RankLatentIndex n)

@[simp]

theorem RelSignature.rankLatentIndexEquiv_mul {S : RelSignature} (σ τ : ↥S.FinSuppPerm) (n : ℕ) : rankLatentIndexEquiv (σ * τ) n = (rankLatentIndexEquiv τ n).trans (rankLatentIndexEquiv σ n)

noncomputable def RelSignature.rankLatentRelabel {S : RelSignature} (σ : ↥S.FinSuppPerm) (n : ℕ) : S.RankLatentSpace n ≃ᵐ S.RankLatentSpace n

Relabeling of a latent assignment, by coordinate reindexing.

Equations

• RelSignature.rankLatentRelabel σ n = { toEquiv := (RelSignature.rankLatentIndexEquiv σ n).symm.arrowCongr (Equiv.refl ℝ), measurable_toFun := ⋯, measurable_invFun := ⋯ }

@[simp]

theorem RelSignature.rankLatentRelabel_apply {S : RelSignature} (σ : ↥S.FinSuppPerm) (n : ℕ) (ω : S.RankLatentSpace n) (A : S.RankLatentIndex n) : (rankLatentRelabel σ n) ω A = ω ((rankLatentIndexEquiv σ n) A)

@[simp]

theorem RelSignature.rankLatentRelabel_one {S : RelSignature} (n : ℕ) : rankLatentRelabel 1 n = MeasurableEquiv.refl (S.RankLatentSpace n)

@[simp]

theorem RelSignature.rankLatentRelabel_one_eq {S : RelSignature} (σ : ↥S.FinSuppPerm) (ω : S.RankLatentSpace 1) : (rankLatentRelabel σ 1) ω = ω

At rank one every latent relabeling is the identity. RankLatentIndex S 1 is the single support ∅, so any permutation of it is trivial — which is why the rank-one equivariance clause says only that the factor equivalence fixes the coding map almost everywhere.

@[simp]

theorem RelSignature.rankLatentRelabel_mul {S : RelSignature} (σ τ : ↥S.FinSuppPerm) (n : ℕ) : rankLatentRelabel (σ * τ) n = (rankLatentRelabel σ n).trans (rankLatentRelabel τ n)

theorem RelSignature.rankLatentProjection_rankLatentRelabel {S : RelSignature} (σ : ↥S.FinSuppPerm) {n m : ℕ} (h : n ≤ m) : rankLatentProjection h ∘ ⇑(rankLatentRelabel σ m) = ⇑(rankLatentRelabel σ n) ∘ rankLatentProjection h

Rank projection commutes definitionally with relabeling.

theorem RelSignature.rankLatentSource_map_rankLatentRelabel {S : RelSignature} (σ : ↥S.FinSuppPerm) (n : ℕ) : MeasureTheory.Measure.map (⇑(rankLatentRelabel σ n)) (S.rankLatentSource n) = S.rankLatentSource n

The i.i.d. latent source is invariant under sortwise relabeling.

Rank one

noncomputable def RelSignature.rankLatentOneEquiv {S : RelSignature} : S.RankLatentSpace 1 ≃ᵐ ℝ

Evaluation at the unique empty-support coordinate.

Equations

• RelSignature.rankLatentOneEquiv = MeasurableEquiv.piUnique fun (x : S.RankLatentIndex 1) => ℝ

@[simp]

theorem RelSignature.rankLatentOneEquiv_apply {S : RelSignature} (ω : S.RankLatentSpace 1) : rankLatentOneEquiv ω = ω rankLatentEmpty

theorem RelSignature.rankLatentSource_map_rankLatentOneEquiv {S : RelSignature} : MeasureTheory.Measure.map (⇑rankLatentOneEquiv) (S.rankLatentSource 1) = MeasureTheory.uniform01

The rank-one latent source is exactly one uniform01 random variable.

Successor split

def RelSignature.rankLatentIndexSuccEquiv {S : RelSignature} (n : ℕ) : S.RankLatentIndex (n + 1) ≃ S.RankLatentIndex n ⊕ S.RankSupport n

Rank below n+1 means rank below n or rank exactly n.

Equations

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

noncomputable def RelSignature.rankLatentSpaceSuccEquiv {S : RelSignature} (n : ℕ) : S.RankLatentSpace (n + 1) ≃ᵐ S.RankLatentSpace n × (S.RankSupport n → ℝ)

The successor split of the latent space into old and fresh coordinates.

Equations

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

theorem RelSignature.fst_rankLatentSpaceSuccEquiv {S : RelSignature} (n : ℕ) (ω : S.RankLatentSpace (n + 1)) : ((rankLatentSpaceSuccEquiv n) ω).1 = rankLatentProjection ⋯ ω

The first component of the successor split is the existing rank projection.

theorem RelSignature.rankLatentSource_map_rankLatentSpaceSuccEquiv {S : RelSignature} (n : ℕ) : MeasureTheory.Measure.map (⇑(rankLatentSpaceSuccEquiv n)) (S.rankLatentSource (n + 1)) = (S.rankLatentSource n).prod (MeasureTheory.iidUniformSource (S.RankSupport n))

The successor split also splits the source: the old lower-rank latents and the fresh rank-n latents are independent i.i.d. uniform families.

noncomputable def RelSignature.rankSupportLatentRelabel {S : RelSignature} (σ : ↥S.FinSuppPerm) (n : ℕ) : (S.RankSupport n → ℝ) ≃ᵐ (S.RankSupport n → ℝ)

Relabeling of the fresh rank-n latent layer, again by coordinate reindexing.

Equations

• RelSignature.rankSupportLatentRelabel σ n = { toEquiv := (RelSignature.rankSupportEquiv σ n).symm.arrowCongr (Equiv.refl ℝ), measurable_toFun := ⋯, measurable_invFun := ⋯ }

@[simp]

theorem RelSignature.rankSupportLatentRelabel_apply {S : RelSignature} (σ : ↥S.FinSuppPerm) (n : ℕ) (ω : S.RankSupport n → ℝ) (A : S.RankSupport n) : (rankSupportLatentRelabel σ n) ω A = ω ((rankSupportEquiv σ n) A)

@[simp]

theorem RelSignature.rankSupportLatentRelabel_one {S : RelSignature} (n : ℕ) : rankSupportLatentRelabel 1 n = MeasurableEquiv.refl (S.RankSupport n → ℝ)

@[simp]

theorem RelSignature.rankSupportLatentRelabel_mul {S : RelSignature} (σ τ : ↥S.FinSuppPerm) (n : ℕ) : rankSupportLatentRelabel (σ * τ) n = (rankSupportLatentRelabel σ n).trans (rankSupportLatentRelabel τ n)

theorem RelSignature.rankLatentIndexSuccEquiv_rankLatentIndexEquiv {S : RelSignature} (σ : ↥S.FinSuppPerm) (n : ℕ) : ⇑(rankLatentIndexSuccEquiv n) ∘ ⇑(rankLatentIndexEquiv σ (n + 1)) = Sum.map ⇑(rankLatentIndexEquiv σ n) ⇑(rankSupportEquiv σ n) ∘ ⇑(rankLatentIndexSuccEquiv n)

The successor index split is natural under relabeling.

theorem RelSignature.rankLatentSpaceSuccEquiv_rankLatentRelabel {S : RelSignature} (σ : ↥S.FinSuppPerm) (n : ℕ) : ⇑(rankLatentSpaceSuccEquiv n) ∘ ⇑(rankLatentRelabel σ (n + 1)) = ⇑((rankLatentRelabel σ n).prodCongr (rankSupportLatentRelabel σ n)) ∘ ⇑(rankLatentSpaceSuccEquiv n)

The successor latent split is equivariant. As on the factor side, the space-level square is definitional even though the forward index split branches on a cardinality test.

theorem RelSignature.rankLatentSource_eq_latentSourceOver (S : RelSignature) (n : ℕ) : S.rankLatentSource n = S.latentSourceOver S.Vinfinite n

Bridge to the carrier-parametric core

The rank-indexed operations were built before the carrier-parametric core and choose their own Decidable instances; they agree with the generic ones extensionally but not by rfl.

theorem RelSignature.rankLatentIndexEquiv_eq_latentIndexPerm {S : RelSignature} (σ : ↥S.FinSuppPerm) (n : ℕ) (A : S.RankLatentIndex n) : (rankLatentIndexEquiv σ n) A = (latentIndexPerm (fun (s : S.Srt) => ↑σ s) n) A

theorem RelSignature.rankLatentRelabel_eq_latentRelabelOver {S : RelSignature} (σ : ↥S.FinSuppPerm) (n : ℕ) : rankLatentRelabel σ n = latentRelabelOver (fun (s : S.Srt) => ↑σ s) n

Bridge: the rank-indexed relabeling is the carrier-parametric action at Vinfinite S.