Carrier-parametric observation layer (R4 converse, #107)

The observations used by recovery and screening — local latents, blocks of raw relation coordinates, and the rank-truncated remainder — over an arbitrary sortwise carrier. The Vinfinite-indexed originals become compatibility aliases, and the pooled statements instantiate this core rather than introducing parallel pooled definitions.

The transport boundary

The three observations do not transport equally well, and the difference is a matter of truth, not of proof effort:

• localLatentsOver and blockMapOver are local — they read only coordinates supported inside a given finite set — so they admit naturality along an arbitrary sortwise embedding of carriers: an embedding restricts to a bijection between the supports inside A and those inside its image.
• restObservationOver is global: its remainder ranges over every rank-≤ n coordinate of the ambient carrier other than the one at A. Along an embedding into a larger carrier the target remainder sees coordinates outside the image, which the source remainder cannot, so an embedding-level commuting law would be false. It transports only along a carrier equivalence.

Screening therefore transports along the canonical poolVertexEquiv, which the pooled uniqueness identity makes available; recovery, being local, is free to use embeddings.

Local latents

def RelSignature.LocalLatentIndexOver {S : RelSignature} (V : S.Srt → Type v) (A : Finset ((s : S.Srt) × V s)) (n : ℕ) : Type (max 0 u v)

The latent coordinates visible at A: supports contained in A.

Equations

• RelSignature.LocalLatentIndexOver V A n = { B : S.LatentIndexOver V n // ↑B ⊆ A }

instance RelSignature.instCountableLocalLatentIndexOverOfSrt {S : RelSignature} {V : S.Srt → Type v} [Countable S.Srt] [∀ (s : S.Srt), Countable (V s)] (A : Finset ((s : S.Srt) × V s)) (n : ℕ) : Countable (LocalLatentIndexOver V A n)

@[reducible, inline]

abbrev RelSignature.LocalLatentSpaceOver {S : RelSignature} (V : S.Srt → Type v) (A : Finset ((s : S.Srt) × V s)) (n : ℕ) : Type (max v u)

The local latent space at A.

Equations

• RelSignature.LocalLatentSpaceOver V A n = (RelSignature.LocalLatentIndexOver V A n → ℝ)

def RelSignature.localLatentsOver {S : RelSignature} {V : S.Srt → Type v} (A : Finset ((s : S.Srt) × V s)) (n : ℕ) : S.LatentSpaceOver V n → LocalLatentSpaceOver V A n

Restriction of the latent array to the coordinates visible at A.

Equations

• RelSignature.localLatentsOver A n ω B = ω ↑B

theorem RelSignature.measurable_localLatentsOver {S : RelSignature} {V : S.Srt → Type v} (A : Finset ((s : S.Srt) × V s)) (n : ℕ) : Measurable (localLatentsOver A n)

Blocks of raw relation coordinates

def RelSignature.BlockIndexOver {S : RelSignature} (V : S.Srt → Type v) (A : Finset ((s : S.Srt) × V s)) : Type (max 0 u v)

Raw relation coordinates whose tagged support is exactly A.

Equations

• RelSignature.BlockIndexOver V A = { c : S.RelCoord V // c.support = A }

instance RelSignature.instCountableBlockIndexOverOfRel {S : RelSignature} {V : S.Srt → Type v} [Countable S.Rel] [∀ (s : S.Srt), Countable (V s)] (A : Finset ((s : S.Srt) × V s)) : Countable (BlockIndexOver V A)

@[reducible, inline]

abbrev RelSignature.BlockSpaceOver {S : RelSignature} (V : S.Srt → Type v) (A : Finset ((s : S.Srt) × V s)) : Type (max v u)

The block of the structure at A.

Equations

• RelSignature.BlockSpaceOver V A = (RelSignature.BlockIndexOver V A → Bool)

def RelSignature.blockMapOver {S : RelSignature} {V : S.Srt → Type v} (A : Finset ((s : S.Srt) × V s)) : S.RelStructure V → BlockSpaceOver V A

Read the block at A off a structure.

Equations

• RelSignature.blockMapOver A X c = X ↑c

theorem RelSignature.measurable_blockMapOver {S : RelSignature} {V : S.Srt → Type v} [Countable S.Rel] [∀ (s : S.Srt), Countable (V s)] (A : Finset ((s : S.Srt) × V s)) : Measurable (blockMapOver A)

The rank-truncated remainder

Global, hence transportable only along carrier equivalences — see the module header.

def RelSignature.RestIndexOver {S : RelSignature} (V : S.Srt → Type v) (n : ℕ) (A : Finset ((s : S.Srt) × V s)) : Type (max 0 u v)

Coordinates of rank at most n other than those at A.

Equations

• RelSignature.RestIndexOver V n A = { c : S.RelCoord V // c.support.card ≤ n ∧ c.support ≠ A }

instance RelSignature.instCountableRestIndexOverOfRel {S : RelSignature} {V : S.Srt → Type v} [Countable S.Rel] [∀ (s : S.Srt), Countable (V s)] (n : ℕ) (A : Finset ((s : S.Srt) × V s)) : Countable (RestIndexOver V n A)

@[reducible, inline]

abbrev RelSignature.RestSpaceOver {S : RelSignature} (V : S.Srt → Type v) (n : ℕ) (A : Finset ((s : S.Srt) × V s)) : Type (max v u)

The remaining rank-≤ n structure.

Equations

• RelSignature.RestSpaceOver V n A = (RelSignature.RestIndexOver V n A → Bool)

def RelSignature.restObservationOver {S : RelSignature} {V : S.Srt → Type v} (n : ℕ) (A : Finset ((s : S.Srt) × V s)) : S.RelStructure V × S.LatentSpaceOver V n → RestSpaceOver V n A × S.LatentSpaceOver V n

The rank-truncated remainder observation over a carrier: the other blocks of rank at most n, together with the whole latent array.

Equations

• RelSignature.restObservationOver n A p = (fun (c : RelSignature.RestIndexOver V n A) => p.1 ↑c, p.2)

theorem RelSignature.measurable_restObservationOver {S : RelSignature} {V : S.Srt → Type v} [Countable S.Rel] [∀ (s : S.Srt), Countable (V s)] (n : ℕ) (A : Finset ((s : S.Srt) × V s)) : Measurable (restObservationOver n A)

Reindexing does not move the conditioning algebra

Screening conditions on a σ-algebra generated by an observation map. Transporting the observation through a measurable equivalence of codomains leaves that σ-algebra unchanged — measurability in both directions is exactly what makes the comap survive. Named here so the screening assembly can straighten a transported conditioning map without a further probabilistic lemma.

theorem RelSignature.comap_measurableEquiv_comp {Ω : Type u_1} {α : Type u_2} {β : Type u_3} [MeasurableSpace α] [MeasurableSpace β] (φ : α ≃ᵐ β) (f : Ω → α) : MeasurableSpace.comap (⇑φ ∘ f) inferInstance = MeasurableSpace.comap f inferInstance

Postcomposition with a measurable equivalence does not change the generated σ-algebra.

Coordinate transport along a carrier equivalence

The coordinate mirror of RelStructure.congrCarrier, bundled once here: the remainder index is global, so its transport needs a genuine equivalence of coordinates rather than an embedding.

def RelSignature.RelCoord.congrCarrier {S : RelSignature} {V W : S.Srt → Type v} (e : (s : S.Srt) → V s ≃ W s) : S.RelCoord V ≃ S.RelCoord W

Transport of relation coordinates along a sortwise equivalence of carriers, bundled.

Equations

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

@[simp]

theorem RelSignature.RelCoord.congrCarrier_apply {S : RelSignature} {V W : S.Srt → Type v} (e : (s : S.Srt) → V s ≃ W s) (c : S.RelCoord V) : (congrCarrier e) c = map (fun (s : S.Srt) => ⇑(e s)) c

@[simp]

theorem RelSignature.RelCoord.congrCarrier_symm_apply {S : RelSignature} {V W : S.Srt → Type v} (e : (s : S.Srt) → V s ≃ W s) (c : S.RelCoord W) : (congrCarrier e).symm c = map (fun (s : S.Srt) => ⇑(e s).symm) c

Support and index transport

Equivalences first, with pointwise _apply lemmas; the function-level naturality laws are derived from these. Keeping the bijections primitive is what limits coercion and DecidableEq friction.

noncomputable def RelSignature.supportImage {S : RelSignature} {V W : S.Srt → Type v} (e : (s : S.Srt) → V s ↪ W s) (A : Finset ((s : S.Srt) × V s)) : Finset ((s : S.Srt) × W s)

The image of a support under a sortwise embedding of carriers.

Equations

• RelSignature.supportImage e A = Finset.image (Sigma.map id fun (s : S.Srt) => ⇑(e s)) A

theorem RelSignature.mem_supportImage_iff {S : RelSignature} {V W : S.Srt → Type v} (e : (s : S.Srt) → V s ↪ W s) (A : Finset ((s : S.Srt) × V s)) (v : (s : S.Srt) × W s) : v ∈ supportImage e A ↔ ∃ w ∈ A, Sigma.map id (fun (s : S.Srt) => ⇑(e s)) w = v

Membership in a support image, stated without an image in the type so that no DecidableEq instance appears in it. Over a carrier with a natural instance — PoolVertex, whose Sum gives one — that instance is not definitionally the classical one used to form the image, which makes image-shaped rewriting unusable there; this form is not.

theorem RelSignature.injective_sigmaMap {S : RelSignature} {V W : S.Srt → Type v} (e : (s : S.Srt) → V s ↪ W s) : Function.Injective (Sigma.map id fun (s : S.Srt) => ⇑(e s))

theorem RelSignature.supportImage_injective {S : RelSignature} {V W : S.Srt → Type v} (e : (s : S.Srt) → V s ↪ W s) : Function.Injective (supportImage e)

theorem RelSignature.supportImage_support {S : RelSignature} {V W : S.Srt → Type v} (e : (s : S.Srt) → V s ↪ W s) (d : S.RelCoord V) : supportImage e d.support = (RelCoord.map (fun (s : S.Srt) => ⇑(e s)) d).support

The image of a coordinate's support is the support of the transported coordinate.

@[simp]

theorem RelSignature.mem_supportImage_map {S : RelSignature} {V W : S.Srt → Type v} {e : (s : S.Srt) → V s ↪ W s} {A : Finset ((s : S.Srt) × V s)} {v : (s : S.Srt) × V s} : Sigma.map id (fun (s : S.Srt) => ⇑(e s)) v ∈ supportImage e A ↔ v ∈ A

theorem RelSignature.latentIndexEmbed_subset_supportImage_iff {S : RelSignature} {V W : S.Srt → Type v} (e : (s : S.Srt) → V s ↪ W s) {A : Finset ((s : S.Srt) × V s)} {n : ℕ} (B : S.LatentIndexOver V n) : ↑(latentIndexEmbed e n B) ⊆ supportImage e A ↔ ↑B ⊆ A

A support lies inside A exactly when its image lies inside the image of A. This is the bijection underlying local naturality: an embedding restricts to a bijection between the supports inside A and those inside its image.

theorem RelSignature.RelCoord.support_congrCarrier {S : RelSignature} {V W : S.Srt → Type v} (e : (s : S.Srt) → V s ≃ W s) (c : S.RelCoord V) : ((congrCarrier e) c).support = supportImage (fun (s : S.Srt) => (e s).toEmbedding) c.support

Transporting a coordinate carries its support to the image of that support.

Local latents transport along an embedding

Index equivalence, then the space-level measurable equivalence, then the pointwise lemma, then the exact naturality theorem against localLatentsOver. The inverse needs no Finset.preimage: a support inside the image of A is the image of the sub-support of A that lands in it.

theorem RelSignature.image_filter_mem {S : RelSignature} {V W : S.Srt → Type v} (e : (s : S.Srt) → V s ↪ W s) {A : Finset ((s : S.Srt) × V s)} {B : Finset ((s : S.Srt) × W s)} (h : B ⊆ supportImage e A) : Finset.image (Sigma.map id fun (s : S.Srt) => ⇑(e s)) ({v ∈ A | Sigma.map id (fun (s : S.Srt) => ⇑(e s)) v ∈ B}) = B

A support inside supportImage e A is the image of the part of A that lands in it.

noncomputable def RelSignature.localLatentIndexCongr {S : RelSignature} {V W : S.Srt → Type v} (e : (s : S.Srt) → V s ↪ W s) (A : Finset ((s : S.Srt) × V s)) (n : ℕ) : LocalLatentIndexOver V A n ≃ LocalLatentIndexOver W (supportImage e A) n

The local latent index transports along an embedding.

Equations

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

noncomputable def RelSignature.localLatentSpaceCongr {S : RelSignature} {V W : S.Srt → Type v} (e : (s : S.Srt) → V s ↪ W s) (A : Finset ((s : S.Srt) × V s)) (n : ℕ) : LocalLatentSpaceOver W (supportImage e A) n ≃ᵐ LocalLatentSpaceOver V A n

The local latent space equivalence induced by an embedding, as a measurable equivalence.

Equations

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

@[simp]

theorem RelSignature.localLatentSpaceCongr_apply {S : RelSignature} {V W : S.Srt → Type v} (e : (s : S.Srt) → V s ↪ W s) (A : Finset ((s : S.Srt) × V s)) (n : ℕ) (x : LocalLatentSpaceOver W (supportImage e A) n) (B : LocalLatentIndexOver V A n) : (localLatentSpaceCongr e A n) x B = x ((localLatentIndexCongr e A n) B)

theorem RelSignature.localLatentsOver_latentRestrictOver {S : RelSignature} {V W : S.Srt → Type v} (e : (s : S.Srt) → V s ↪ W s) (A : Finset ((s : S.Srt) × V s)) (n : ℕ) : localLatentsOver A n ∘ latentRestrictOver e n = ⇑(localLatentSpaceCongr e A n) ∘ localLatentsOver (supportImage e A) n

Exact naturality of the local latents against an embedding. Reading the latents visible at A after restricting along e is reading those visible at the image of A and transporting.

theorem RelSignature.supportImage_symm_supportImage {S : RelSignature} {V W : S.Srt → Type v} (e : (s : S.Srt) → V s ≃ W s) (A : Finset ((s : S.Srt) × V s)) : supportImage (fun (s : S.Srt) => (e s).symm.toEmbedding) (supportImage (fun (s : S.Srt) => (e s).toEmbedding) A) = A

Transporting a support along a carrier equivalence and back is the identity.

theorem RelSignature.card_supportImage {S : RelSignature} {V W : S.Srt → Type v} (e : (s : S.Srt) → V s ↪ W s) (A : Finset ((s : S.Srt) × V s)) : (supportImage e A).card = A.card

The transported support has the same cardinality.

Blocks transport along an embedding

The inverse is the delicate point and is kept local to the exact-support subtype: a coordinate whose support is exactly supportImage e A has every argument in the image of e, which supplies the range witness for each argument. Nothing pretends e is globally surjective.

theorem RelSignature.exists_preimage_of_block {S : RelSignature} {V W : S.Srt → Type v} (e : (s : S.Srt) → V s ↪ W s) {A : Finset ((s : S.Srt) × V s)} (c : BlockIndexOver W (supportImage e A)) (i : Fin (S.arity (↑c).fst)) : ∃ (v : V (S.argSort (↑c).fst i)), (e (S.argSort (↑c).fst i)) v = (↑c).snd i

Every argument of a coordinate with support exactly supportImage e A lies in the range of the embedding — the range witness the inverse needs, available only on this subtype.

noncomputable def RelSignature.blockPreimage {S : RelSignature} {V W : S.Srt → Type v} (e : (s : S.Srt) → V s ↪ W s) {A : Finset ((s : S.Srt) × V s)} (c : BlockIndexOver W (supportImage e A)) (i : Fin (S.arity (↑c).fst)) : V (S.argSort (↑c).fst i)

The chosen preimage of an argument.

Equations

• RelSignature.blockPreimage e c i = ⋯.choose

@[simp]

theorem RelSignature.blockPreimage_spec {S : RelSignature} {V W : S.Srt → Type v} (e : (s : S.Srt) → V s ↪ W s) {A : Finset ((s : S.Srt) × V s)} (c : BlockIndexOver W (supportImage e A)) (i : Fin (S.arity (↑c).fst)) : (e (S.argSort (↑c).fst i)) (blockPreimage e c i) = (↑c).snd i

theorem RelSignature.map_blockPreimage {S : RelSignature} {V W : S.Srt → Type v} (e : (s : S.Srt) → V s ↪ W s) {A : Finset ((s : S.Srt) × V s)} (c : BlockIndexOver W (supportImage e A)) : RelCoord.map (fun (s : S.Srt) => ⇑(e s)) ⟨(↑c).fst, blockPreimage e c⟩ = ↑c

noncomputable def RelSignature.blockIndexCongr {S : RelSignature} {V W : S.Srt → Type v} (e : (s : S.Srt) → V s ↪ W s) (A : Finset ((s : S.Srt) × V s)) : BlockIndexOver V A ≃ BlockIndexOver W (supportImage e A)

The block index transports along an embedding.

Equations

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

noncomputable def RelSignature.blockSpaceCongr {S : RelSignature} {V W : S.Srt → Type v} (e : (s : S.Srt) → V s ↪ W s) (A : Finset ((s : S.Srt) × V s)) : BlockSpaceOver W (supportImage e A) ≃ᵐ BlockSpaceOver V A

The block space equivalence induced by an embedding, as a measurable equivalence.

Equations

• RelSignature.blockSpaceCongr e A = { toEquiv := (RelSignature.blockIndexCongr e A).symm.arrowCongr (Equiv.refl Bool), measurable_toFun := ⋯, measurable_invFun := ⋯ }

@[simp]

theorem RelSignature.blockSpaceCongr_apply {S : RelSignature} {V W : S.Srt → Type v} (e : (s : S.Srt) → V s ↪ W s) (A : Finset ((s : S.Srt) × V s)) (x : BlockSpaceOver W (supportImage e A)) (c : BlockIndexOver V A) : (blockSpaceCongr e A) x c = x ((blockIndexCongr e A) c)

theorem RelSignature.blockMapOver_restrict {S : RelSignature} {V W : S.Srt → Type v} (e : (s : S.Srt) → V s ↪ W s) (A : Finset ((s : S.Srt) × V s)) : blockMapOver A ∘ RelStructure.restrict e = ⇑(blockSpaceCongr e A) ∘ blockMapOver (supportImage e A)

Exact naturality of the block against an embedding.

The remainder transports along a carrier equivalence

Bundled as a measurable equivalence, not merely an index bijection, so that the screening assembly can straighten the transported remainder codomain directly.

noncomputable def RelSignature.restIndexCongr {S : RelSignature} {V W : S.Srt → Type v} (e : (s : S.Srt) → V s ≃ W s) (n : ℕ) (A : Finset ((s : S.Srt) × V s)) : RestIndexOver V n A ≃ RestIndexOver W n (supportImage (fun (s : S.Srt) => (e s).toEmbedding) A)

The remainder index transports along a carrier equivalence. An equivalence is required: the remainder ranges over every rank-≤ n coordinate of the ambient carrier, so an embedding into a larger carrier would leave coordinates outside its image unmatched.

Equations

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

noncomputable def RelSignature.restSpaceCongr {S : RelSignature} {V W : S.Srt → Type v} (e : (s : S.Srt) → V s ≃ W s) (n : ℕ) (A : Finset ((s : S.Srt) × V s)) : RestSpaceOver W n (supportImage (fun (s : S.Srt) => (e s).toEmbedding) A) ≃ᵐ RestSpaceOver V n A

The remainder space equivalence induced by a carrier equivalence, as a measurable equivalence.

Equations

• RelSignature.restSpaceCongr e n A = { toEquiv := (RelSignature.restIndexCongr e n A).symm.arrowCongr (Equiv.refl Bool), measurable_toFun := ⋯, measurable_invFun := ⋯ }

@[simp]

theorem RelSignature.restSpaceCongr_apply {S : RelSignature} {V W : S.Srt → Type v} (e : (s : S.Srt) → V s ≃ W s) (n : ℕ) (A : Finset ((s : S.Srt) × V s)) (x : RestSpaceOver W n (supportImage (fun (s : S.Srt) => (e s).toEmbedding) A)) (c : RestIndexOver V n A) : (restSpaceCongr e n A) x c = x ((restIndexCongr e n A) c)

theorem RelSignature.restObservationOver_congrCarrier {S : RelSignature} {V W : S.Srt → Type v} (e : (s : S.Srt) → V s ≃ W s) (n : ℕ) (A : Finset ((s : S.Srt) × V s)) : restObservationOver n A ∘ Prod.map (RelStructure.restrict fun (s : S.Srt) => (e s).toEmbedding) (latentRestrictOver (fun (s : S.Srt) => (e s).toEmbedding) n) = Prod.map ⇑(restSpaceCongr e n A) ⇑(latentCongrOver e n) ∘ restObservationOver n (supportImage (fun (s : S.Srt) => (e s).toEmbedding) A)

Exact naturality of the remainder against a carrier equivalence. Observing after transporting the whole joint object from W back to V is observing on W and reindexing both remainder outputs. An equivalence throughout — the remainder is global.