Carrier-parametric latent geometry (R4 converse, #107)

Law-free latent geometry over an arbitrary sortwise carrier V : S.Srt → Type*: supports of cardinality below the working rank, the latent cube they index, its i.i.d. uniform source, the action of a sortwise permutation family, and restriction along a sortwise embedding of carriers.

Nothing here mentions a law, a measure on structures, a representation, recovery, screening, or a coupling. The two intended carriers are Vinfinite S (the original vertices) and PoolVertex S (the pooled vertices); restriction along the original embedding is what relates them.

The action is by the full permutation family ∀ s, Equiv.Perm (V s). Finite support is a property of a particular carrier's automorphisms, not of latent cubes: any sortwise permutation reindexes finite supports bijectively and preserves cardinality, so it acts on the index type and preserves the i.i.d. source. Users needing a finitely supported subgroup restrict this action rather than the other way round.

Supports, the latent cube, and its source

def RelSignature.LatentIndexOver (S : RelSignature) (V : S.Srt → Type v) (n : ℕ) : Type (max 0 u v)

Supports of cardinality below n over a sortwise carrier.

Equations

• S.LatentIndexOver V n = { A : Finset ((s : S.Srt) × V s) // A.card < n }

instance RelSignature.instCountableLatentIndexOverOfSrt {S : RelSignature} {V : S.Srt → Type v} [Countable S.Srt] [∀ (s : S.Srt), Countable (V s)] (n : ℕ) : Countable (S.LatentIndexOver V n)

@[reducible, inline]

abbrev RelSignature.LatentSpaceOver (S : RelSignature) (V : S.Srt → Type v) (n : ℕ) : Type (max v u)

The latent cube over a carrier: one real coordinate per support below the rank.

Equations

• S.LatentSpaceOver V n = (S.LatentIndexOver V n → ℝ)

noncomputable def RelSignature.latentSourceOver (S : RelSignature) (V : S.Srt → Type v) (n : ℕ) : MeasureTheory.Measure (S.LatentSpaceOver V n)

The i.i.d. uniform latent source over a carrier.

Equations

• S.latentSourceOver V n = MeasureTheory.iidUniformSource (S.LatentIndexOver V n)

instance RelSignature.instIsProbabilityMeasureLatentSpaceOverLatentSourceOver {S : RelSignature} {V : S.Srt → Type v} (n : ℕ) : MeasureTheory.IsProbabilityMeasure (S.latentSourceOver V n)

The action of a sortwise permutation family

noncomputable def RelSignature.latentIndexPerm {S : RelSignature} {V : S.Srt → Type v} (ρ : (s : S.Srt) → Equiv.Perm (V s)) (n : ℕ) : S.LatentIndexOver V n ≃ S.LatentIndexOver V n

A sortwise permutation family permutes the supports below each rank. Bijectivity of each ρ s preserves cardinality, so the rank is unchanged.

Equations

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

@[simp]

theorem RelSignature.latentIndexPerm_apply_coe {S : RelSignature} {V : S.Srt → Type v} (ρ : (s : S.Srt) → Equiv.Perm (V s)) (n : ℕ) (A : S.LatentIndexOver V n) : ↑((latentIndexPerm ρ n) A) = Finset.image (Sigma.map id fun (s : S.Srt) => ⇑(ρ s)) ↑A

@[simp]

theorem RelSignature.latentIndexPerm_one {S : RelSignature} {V : S.Srt → Type v} (n : ℕ) : latentIndexPerm (fun (x : S.Srt) => 1) n = Equiv.refl (S.LatentIndexOver V n)

@[simp]

theorem RelSignature.latentIndexPerm_comp {S : RelSignature} {V : S.Srt → Type v} (ρ τ : (s : S.Srt) → Equiv.Perm (V s)) (n : ℕ) : latentIndexPerm (fun (s : S.Srt) => ρ s * τ s) n = (latentIndexPerm τ n).trans (latentIndexPerm ρ n)

noncomputable def RelSignature.latentRelabelOver {S : RelSignature} {V : S.Srt → Type v} (ρ : (s : S.Srt) → Equiv.Perm (V s)) (n : ℕ) : S.LatentSpaceOver V n ≃ᵐ S.LatentSpaceOver V n

The action on the latent cube: reindex the coordinates.

Equations

• RelSignature.latentRelabelOver ρ n = { toEquiv := (RelSignature.latentIndexPerm ρ n).symm.arrowCongr (Equiv.refl ℝ), measurable_toFun := ⋯, measurable_invFun := ⋯ }

@[simp]

theorem RelSignature.latentRelabelOver_apply {S : RelSignature} {V : S.Srt → Type v} (ρ : (s : S.Srt) → Equiv.Perm (V s)) (n : ℕ) (ω : S.LatentSpaceOver V n) (A : S.LatentIndexOver V n) : (latentRelabelOver ρ n) ω A = ω ((latentIndexPerm ρ n) A)

theorem RelSignature.latentSourceOver_map_latentRelabelOver {S : RelSignature} {V : S.Srt → Type v} [Countable S.Srt] [∀ (s : S.Srt), Countable (V s)] (ρ : (s : S.Srt) → Equiv.Perm (V s)) (n : ℕ) : MeasureTheory.Measure.map (⇑(latentRelabelOver ρ n)) (S.latentSourceOver V n) = S.latentSourceOver V n

Exact invariance of the source. The action permutes coordinates of an i.i.d. cube.

Restriction along a sortwise embedding of carriers

noncomputable def RelSignature.latentIndexEmbed {S : RelSignature} {V W : S.Srt → Type v} (e : (s : S.Srt) → V s ↪ W s) (n : ℕ) : S.LatentIndexOver V n → S.LatentIndexOver W n

A sortwise embedding of carriers pushes supports forward, preserving the rank.

Equations

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

@[simp]

theorem RelSignature.latentIndexEmbed_coe {S : RelSignature} {V W : S.Srt → Type v} (e : (s : S.Srt) → V s ↪ W s) (n : ℕ) (A : S.LatentIndexOver V n) : ↑(latentIndexEmbed e n A) = Finset.image (Sigma.map id fun (s : S.Srt) => ⇑(e s)) ↑A

noncomputable def RelSignature.latentRestrictOver {S : RelSignature} {V W : S.Srt → Type v} (e : (s : S.Srt) → V s ↪ W s) (n : ℕ) : S.LatentSpaceOver W n → S.LatentSpaceOver V n

Restriction of a latent assignment along a sortwise embedding of carriers: read the coordinates indexed by the embedded supports.

Equations

• RelSignature.latentRestrictOver e n ω A = ω (RelSignature.latentIndexEmbed e n A)

theorem RelSignature.measurable_latentRestrictOver {S : RelSignature} {V W : S.Srt → Type v} (e : (s : S.Srt) → V s ↪ W s) (n : ℕ) : Measurable (latentRestrictOver e n)

@[simp]

theorem RelSignature.latentRestrictOver_apply {S : RelSignature} {V W : S.Srt → Type v} (e : (s : S.Srt) → V s ↪ W s) (n : ℕ) (ω : S.LatentSpaceOver W n) (A : S.LatentIndexOver V n) : latentRestrictOver e n ω A = ω (latentIndexEmbed e n A)

theorem RelSignature.latentRestrictOver_latentRelabelOver {S : RelSignature} {V W : S.Srt → Type v} (e : (s : S.Srt) → V s ↪ W s) (ρ : (s : S.Srt) → Equiv.Perm (W s)) (n : ℕ) : latentRestrictOver e n ∘ ⇑(latentRelabelOver ρ n) = latentRestrictOver (fun (s : S.Srt) => (e s).trans (Equiv.toEmbedding (ρ s))) n

The moved-window law, the honest naturality for a carrier permutation: restricting after relabeling the larger carrier is restriction along the moved embedding. A permutation that crosses the image of e does not commute with restriction along e — no such law is stated, and this one holds for every permutation, mixed ones included.

theorem RelSignature.latentIndexPerm_latentIndexEmbed {S : RelSignature} {V W : S.Srt → Type v} (e : (s : S.Srt) → V s ↪ W s) (ρ : (s : S.Srt) → Equiv.Perm (W s)) (τ : (s : S.Srt) → Equiv.Perm (V s)) (h : ∀ (s : S.Srt) (x : V s), (ρ s) ((e s) x) = (e s) ((τ s) x)) (n : ℕ) (A : S.LatentIndexOver V n) : (latentIndexPerm ρ n) (latentIndexEmbed e n A) = latentIndexEmbed e n ((latentIndexPerm τ n) A)

Naturality of the index maps: an embedding of carriers intertwining two permutation families intertwines the induced index actions. Stated here, with abstract carriers, so that instantiating at a concrete carrier never has to manipulate Finset.image under a derived DecidableEq.

theorem RelSignature.latentRestrictOver_latentRelabelOver_of_intertwines {S : RelSignature} {V W : S.Srt → Type v} (e : (s : S.Srt) → V s ↪ W s) (ρ : (s : S.Srt) → Equiv.Perm (W s)) (τ : (s : S.Srt) → Equiv.Perm (V s)) (h : ∀ (s : S.Srt) (x : V s), (ρ s) ((e s) x) = (e s) ((τ s) x)) (n : ℕ) : latentRestrictOver e n ∘ ⇑(latentRelabelOver ρ n) = ⇑(latentRelabelOver τ n) ∘ latentRestrictOver e n

The cube-level form of latentIndexPerm_latentIndexEmbed.

theorem RelSignature.latentIndexEmbed_comp {S : RelSignature} {V W Z : S.Srt → Type v} (e : (s : S.Srt) → V s ↪ W s) (f : (s : S.Srt) → W s ↪ Z s) (n : ℕ) (A : S.LatentIndexOver V n) : latentIndexEmbed f n (latentIndexEmbed e n A) = latentIndexEmbed (fun (s : S.Srt) => (e s).trans (f s)) n A

Index-level functoriality of restriction along carrier embeddings.

theorem RelSignature.latentRestrictOver_comp {S : RelSignature} {V W Z : S.Srt → Type v} (e : (s : S.Srt) → V s ↪ W s) (f : (s : S.Srt) → W s ↪ Z s) (n : ℕ) : latentRestrictOver e n ∘ latentRestrictOver f n = latentRestrictOver (fun (s : S.Srt) => (e s).trans (f s)) n

Functoriality of restriction: restricting along f and then along e is restricting along the composite embedding.

theorem RelSignature.latentRestrictOver_toEmbedding {S : RelSignature} {V : S.Srt → Type v} (ρ : (s : S.Srt) → Equiv.Perm (V s)) (n : ℕ) : latentRestrictOver (fun (s : S.Srt) => Equiv.toEmbedding (ρ s)) n = ⇑(latentRelabelOver ρ n)

Restriction along a permutation-as-embedding is that permutation's action.

theorem RelSignature.latentIndexEmbed_eq_of_agree {S : RelSignature} {V W : S.Srt → Type v} {e f : (s : S.Srt) → V s ↪ W s} {ρ : (s : S.Srt) → Equiv.Perm (W s)} {n : ℕ} {A : S.LatentIndexOver V n} (h : ∀ v ∈ ↑A, (ρ v.fst) ((e v.fst) v.snd) = (f v.fst) v.snd) : latentIndexEmbed f n A = (latentIndexPerm ρ n) (latentIndexEmbed e n A)

Support-wise agreement: if a permutation of the target carrier carries one embedding to another on every vertex of a support, the two induced index maps agree there. Stated with abstract carriers, so instantiating never manipulates Finset.image under a derived DecidableEq.

theorem RelSignature.latentIndexEmbed_refl {S : RelSignature} {V : S.Srt → Type v} (n : ℕ) (A : S.LatentIndexOver V n) : latentIndexEmbed (fun (s : S.Srt) => Function.Embedding.refl (V s)) n A = A

Restriction along the identity embedding is the identity.

noncomputable def RelSignature.latentIndexCongr {S : RelSignature} {V W : S.Srt → Type v} (e : (s : S.Srt) → V s ≃ W s) (n : ℕ) : S.LatentIndexOver V n ≃ S.LatentIndexOver W n

The index bijection induced by a carrier equivalence.

Equations

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

noncomputable def RelSignature.latentCongrOver {S : RelSignature} {V W : S.Srt → Type v} (e : (s : S.Srt) → V s ≃ W s) (n : ℕ) : S.LatentSpaceOver W n ≃ᵐ S.LatentSpaceOver V n

Transport of the latent cube along a carrier equivalence, as a measurable equivalence. Its forward map is restriction along the equivalence, so the organizing restriction theorem can be cancelled rather than merely stated.

Equations

• RelSignature.latentCongrOver e n = { toEquiv := (RelSignature.latentIndexCongr e n).symm.arrowCongr (Equiv.refl ℝ), measurable_toFun := ⋯, measurable_invFun := ⋯ }

@[simp]

theorem RelSignature.latentCongrOver_apply {S : RelSignature} {V W : S.Srt → Type v} (e : (s : S.Srt) → V s ≃ W s) (n : ℕ) (ω : S.LatentSpaceOver W n) : (latentCongrOver e n) ω = latentRestrictOver (fun (s : S.Srt) => (e s).toEmbedding) n ω

@[simp]

theorem RelSignature.latentCongrOver_symm_apply {S : RelSignature} {V W : S.Srt → Type v} (e : (s : S.Srt) → V s ≃ W s) (n : ℕ) (ω : S.LatentSpaceOver V n) : (latentCongrOver e n).symm ω = latentRestrictOver (fun (s : S.Srt) => (e s).symm.toEmbedding) n ω

theorem RelSignature.latentSourceOver_map_latentCongrOver {S : RelSignature} {V W : S.Srt → Type v} [Countable S.Srt] [∀ (s : S.Srt), Countable (V s)] [∀ (s : S.Srt), Countable (W s)] (e : (s : S.Srt) → V s ≃ W s) (n : ℕ) : MeasureTheory.Measure.map (⇑(latentCongrOver e n)) (S.latentSourceOver W n) = S.latentSourceOver V n

Exact source transport along a carrier equivalence. The same infinite-product coordinate-equivalence argument as source invariance, with the index bijection now coming from an equivalence of carriers rather than a permutation of one.

theorem RelSignature.latentRestrictOver_latentRelabelOver_conj {S : RelSignature} {V W : S.Srt → Type v} (e : (s : S.Srt) → V s ≃ W s) (ρ : (s : S.Srt) → Equiv.Perm (V s)) (n : ℕ) : latentRestrictOver (fun (s : S.Srt) => (e s).toEmbedding) n ∘ ⇑(latentRelabelOver (fun (s : S.Srt) => (e s).symm.trans (Equiv.trans (ρ s) (e s))) n) = ⇑(latentRelabelOver ρ n) ∘ latentRestrictOver (fun (s : S.Srt) => (e s).toEmbedding) n

The conjugation square for a carrier equivalence — the latent-side mirror of RelStructure.congrCarrier_relabel. Transporting along e intertwines a permutation of the source carrier with its conjugate on the target. Proved carrier-generically, so instantiating at a concrete carrier never manipulates Finset.image under a derived DecidableEq.