The measurable kernel evaluator over pattern-local latents (R4 evaluator layer, #107)

The second R4 layer, on the settled #137 interface: a kernel family assigns to every relation symbol and every abstract equality pattern a measurable Boolean function of the pattern-local latents; the evaluator reads each coordinate of the infinite structure off the global latent source through its local window. No latent source measure, sampler pushforward, dissociation, or representation theorem here — those are the subsequent layers; this file settles the evaluator and its equivariance.

• RelKernelFamily S — the label-free representing kernels f_{r,π}, measurable on the finite product PatternLatentIndex π → ℝ;
• RelCoord.localLatents — the local latent window of a coordinate: the global source restricted along patternLatentIndexEquivCoord and the canonical projection;
• RelKernelFamily.evalStructure — the evaluated infinite structure, measurable in the global source;
• RelKernelFamily.evalStructure_relabel — equivariance: relabeling the evaluated structure is evaluating at the relabeled latents — the statement that will make exchangeability of the evaluated law a coordinatewise check.

Kernel families

structure RelSignature.RelKernelFamily (S : RelSignature) : Type u_1

A representing kernel family: for every relation symbol and every abstract equality pattern, a measurable Boolean function of the pattern-local latents. Label-free by construction — the kernel sees only the pattern and its blocks, never vertex labels.

• toFun (r : S.Rel) (π : S.EqualityPattern r) : (PatternLatentIndex π → ℝ) → Bool

  The kernel at a relation symbol and pattern.

• measurable (r : S.Rel) (π : S.EqualityPattern r) : Measurable (self.toFun r π)

  Each kernel is measurable on the finite latent product.

The local latent window

noncomputable def RelSignature.RelCoord.localLatents {S : RelSignature} (c : S.RelCoord S.Vinfinite) (ω : S.LatentIndex S.Vinfinite → ℝ) : PatternLatentIndex c.equalityPattern → ℝ

The local latent window of a coordinate: the global latent source read through the coordinate's pattern-local indices (via the canonical equivalence and projection).

Equations

• c.localLatents ω A = ω ((RelSignature.patternLatentIndexEquivCoord c) A).toLatentIndex

theorem RelSignature.RelCoord.measurable_localLatents {S : RelSignature} (c : S.RelCoord S.Vinfinite) : Measurable fun (ω : S.LatentIndex S.Vinfinite → ℝ) => c.localLatents ω

The evaluator

noncomputable def RelSignature.RelKernelFamily.evalStructure {S : RelSignature} (F : S.RelKernelFamily) (ω : S.LatentIndex S.Vinfinite → ℝ) : S.RelStructure S.Vinfinite

The evaluated infinite structure: each coordinate is its kernel applied to its local latent window.

Equations

• F.evalStructure ω c = F.toFun c.fst c.equalityPattern (c.localLatents ω)

@[simp]

theorem RelSignature.RelKernelFamily.evalStructure_apply {S : RelSignature} (F : S.RelKernelFamily) (ω : S.LatentIndex S.Vinfinite → ℝ) (c : S.RelCoord S.Vinfinite) : F.evalStructure ω c = F.toFun c.fst c.equalityPattern (c.localLatents ω)

theorem RelSignature.RelKernelFamily.measurable_evalStructure {S : RelSignature} (F : S.RelKernelFamily) : Measurable F.evalStructure

The evaluator is measurable in the global latent source.

Equivariance

theorem RelSignature.RelCoord.patternQuotientEquivSupport_mk {S : RelSignature} {V : S.Srt → Type u_1} (c : S.RelCoord V) (i : Fin (S.arity c.fst)) : ↑(c.patternQuotientEquivSupport ⟦i⟧) = c.taggedValue i

The value of a support block (definitional): patternQuotientEquivSupport sends the block of position i to the sort-tagged value at i.

theorem RelSignature.mem_patternLatentIndexEquivCoord {S : RelSignature} {V : S.Srt → Type u_1} (c : S.RelCoord V) (A : PatternLatentIndex c.equalityPattern) {v : (s : S.Srt) × V s} : v ∈ ↑((patternLatentIndexEquivCoord c) A) ↔ ∃ q ∈ ↑A, ↑(c.patternQuotientEquivSupport q) = v

Membership characterization of the labeled avatar of a block-set: a tagged value lies in patternLatentIndexEquivCoord c A iff it is the support value of one of the blocks in A.

theorem RelSignature.CoordLatentIndex.mem_congrMap {S : RelSignature} {V : S.Srt → Type u_1} {W : S.Srt → Type u_2} {f : (s : S.Srt) → V s → W s} (hf : ∀ (s : S.Srt), Function.Injective (f s)) (c : S.RelCoord V) (A : CoordLatentIndex c) {w : (s : S.Srt) × W s} : w ∈ ↑((congrMap hf c) A) ↔ ∃ v ∈ ↑A, Sigma.map id (fun (s : S.Srt) => f s) v = w

Membership characterization of the relabeling equivalence: the forward direction of CoordLatentIndex.congrMap is the image under Sigma.map id.

@[simp]

theorem RelSignature.PatternLatentIndex.congr_rfl {S : RelSignature} {r : S.Rel} {π : S.EqualityPattern r} : congr ⋯ = Equiv.refl (PatternLatentIndex π)

Transport of pattern-local indices along rfl is the identity.

theorem RelSignature.PatternLatentIndex.congr_mem_mk {S : RelSignature} {r : S.Rel} {π π' : S.EqualityPattern r} (h : π = π') (A : PatternLatentIndex π) (i : Fin (S.arity r)) : ⟦i⟧ ∈ ↑((congr h) A) ↔ ⟦i⟧ ∈ ↑A

Cast taming: membership of a block in a transported pattern-local index reduces to membership in the original — both sides typecheck because the two patterns share the positions Fin (S.arity r).

theorem RelSignature.patternLatentIndexEquivCoord_map {S : RelSignature} {V : S.Srt → Type u_1} {W : S.Srt → Type u_2} {f : (s : S.Srt) → V s → W s} (hf : ∀ (s : S.Srt), Function.Injective (f s)) (c : S.RelCoord V) (A' : PatternLatentIndex (RelCoord.map f c).equalityPattern) : (patternLatentIndexEquivCoord (RelCoord.map f c)) A' = (CoordLatentIndex.congrMap hf c) ((patternLatentIndexEquivCoord c) ((PatternLatentIndex.congr ⋯) A'))

The transport square: the labeled avatar of a block-set of the relabeled coordinate is the relabeling (CoordLatentIndex.congrMap) of the labeled avatar of the same block-set read through the pattern identification RelCoord.equalityPattern_map.

theorem RelSignature.RelCoord.localLatents_map {S : RelSignature} {f : (s : S.Srt) → S.Vinfinite s → S.Vinfinite s} (hf : ∀ (s : S.Srt), Function.Injective (f s)) (c : S.RelCoord S.Vinfinite) (ω : S.LatentIndex S.Vinfinite → ℝ) (A' : PatternLatentIndex (map f c).equalityPattern) : (map f c).localLatents ω A' = c.localLatents (fun (A : S.LatentIndex S.Vinfinite) => ω (LatentIndex.map f A)) ((PatternLatentIndex.congr ⋯) A')

The local latent window is equivariant: the window of the relabeled coordinate at a block-set is the window of the original coordinate, read off the source precomposed with the global latent-index action, at the transported block-set.

theorem RelSignature.RelKernelFamily.toFun_congr {S : RelSignature} (F : S.RelKernelFamily) {r : S.Rel} {π₁ π₂ : S.EqualityPattern r} (h : π₁ = π₂) {ℓ₁ : PatternLatentIndex π₁ → ℝ} {ℓ₂ : PatternLatentIndex π₂ → ℝ} (hℓ : ∀ (A : PatternLatentIndex π₁), ℓ₁ A = ℓ₂ ((PatternLatentIndex.congr h) A)) : F.toFun r π₁ ℓ₁ = F.toFun r π₂ ℓ₂

Kernel applications transport along pattern equalities: if the patterns agree and the latent arguments correspond under PatternLatentIndex.congr, the kernel values agree.

theorem RelSignature.RelKernelFamily.evalStructure_relabel {S : RelSignature} (F : S.RelKernelFamily) (σ : S.Srt → Equiv.Perm ℕ) (ω : S.LatentIndex S.Vinfinite → ℝ) : RelStructure.relabel σ (F.evalStructure ω) = F.evalStructure fun (A : S.LatentIndex S.Vinfinite) => ω (LatentIndex.map (fun (s : S.Srt) => ⇑(σ s)) A)

Equivariance of the evaluator: relabeling the evaluated structure by a sortwise family of permutations is evaluating at the source precomposed with the latent-index action of the permutations. Orientation: relabel σ reads coordinate c at RelCoord.map σ c, so the source is precomposed with LatentIndex.map σ (the forward action, not σ⁻¹) — relabeling the structure = precomposing the latent source with the latent-index action.