Equality patterns, supports, and subset latent indices (R4 design checkpoint, #107)

The design layer of the functional Aldous–Hoover–Kallenberg representation: the vocabulary in which the dissociated representation's sampler and representation theorem will be stated. This file deliberately contains no sampler and no representation theorem — it fixes the interface (a review checkpoint) before those are built.

Design decisions, made explicit:

• Sort-tagging. The atom of the design is RelCoord.taggedValue c i : Σ s, V s — the value at position i tagged with its sort. All downstream notions factor through it, so equality of raw vertex values across different sorts never counts: vertex 3 of sort A and vertex 3 of sort B are distinct tagged values.
• The equality pattern is a kernel. RelCoord.pattern c := Setoid.ker c.taggedValue — positions are equivalent exactly when they carry the same sort-tagged value. No choice of canonical representative is made; the pattern's blocks are canonically the support (patternQuotientEquivSupport).
• The support is a finset of tagged values, RelCoord.support c ⊆ Σ s, V s — the "vertices the coordinate actually reads", abstractly (not positions).
• Latent indices are nonempty finite sets of tagged values: LatentIndex S V. The eventual dissociated representation reads the coordinate at c off latents U_A for A ⊆ c.support nonempty; one latent source indexed by LatentIndex S (Vinfinite S) will serve every coordinate. Nonemptiness excludes a global (U_∅) latent — the dissociated normal form.
• Patterns are bundled independently of coordinates. EqualityPattern S r packages a setoid on the positions of r together with sort compatibility (equivalent positions have equal argSort), so an abstract pattern π exists without any labeled coordinate; RelCoord.equalityPattern extracts the bundled pattern of a coordinate, and EqualityPattern.blockSort is the induced sort of each block — per-sort counts are derived, never stored (no coherence obligations).
• Local latent indices are bundled per pattern and per coordinate. PatternLatentIndex π (nonempty finite subsets of the blocks) is the label-free, order-free domain the representing kernel f_{r,π} will consume; CoordLatentIndex c (nonempty subsets of the support) is its labeled avatar, with the canonical equivalence patternLatentIndexEquivCoord and the two-way relabeling equivalence CoordLatentIndex.congrMap along sortwise injections.
• Transport is by Sigma.map id. A sortwise map f : ∀ s, V s → W s acts on tagged values, supports, and latent indices through Sigma.map id f; all equivariance statements are phrased through this single action. Sortwise injective maps preserve patterns (pattern_map), act injectively on latent indices, and carry subset-latents of a support to subset-latents of the image support — the equivariance the representation theorem needs so that exchangeability can be checked coordinatewise.

The examples section instantiates a local one-sort binary signature (off-diagonal and diagonal coordinates), a ternary signature with a repeated entry, and a two-sort bipartite signature where equal raw values in different sorts are not identified — all namespaced, with no dependency on the directed development.

Sort-tagged values, patterns, and supports

def RelSignature.RelCoord.taggedValue {S : RelSignature} {V : S.Srt → Type u_1} (c : S.RelCoord V) (i : Fin (S.arity c.fst)) : (s : S.Srt) × V s

The sort-tagged value at a position of a coordinate: the value together with its sort. The atom through which patterns, supports, and latent indices all factor.

Equations

• c.taggedValue i = ⟨S.argSort c.fst i, c.snd i⟩

def RelSignature.RelCoord.pattern {S : RelSignature} {V : S.Srt → Type u_1} (c : S.RelCoord V) : Setoid (Fin (S.arity c.fst))

The equality pattern of a coordinate: the kernel of the sort-tagged value map — positions are equivalent exactly when they carry the same value of the same sort.

Equations

• c.pattern = Setoid.ker c.taggedValue

theorem RelSignature.RelCoord.pattern_iff {S : RelSignature} {V : S.Srt → Type u_1} (c : S.RelCoord V) (i j : Fin (S.arity c.fst)) : c.pattern i j ↔ c.taggedValue i = c.taggedValue j

noncomputable def RelSignature.RelCoord.support {S : RelSignature} {V : S.Srt → Type u_1} (c : S.RelCoord V) : Finset ((s : S.Srt) × V s)

The support of a coordinate: the finite set of sort-tagged values it reads.

Equations

• c.support = Finset.image c.taggedValue Finset.univ

theorem RelSignature.RelCoord.mem_support_iff {S : RelSignature} {V : S.Srt → Type u_1} (c : S.RelCoord V) (v : (s : S.Srt) × V s) : v ∈ c.support ↔ ∃ (i : Fin (S.arity c.fst)), c.taggedValue i = v

theorem RelSignature.RelCoord.card_support_le {S : RelSignature} {V : S.Srt → Type u_1} (c : S.RelCoord V) : c.support.card ≤ S.arity c.fst

The support is no larger than the arity: it is the image of the finitely many positions. Stated over an abstract carrier, where no natural DecidableEq competes with the classical instance used to form the image.

theorem RelSignature.RelCoord.support_nonempty {S : RelSignature} {V : S.Srt → Type u_1} (c : S.RelCoord V) (h : 0 < S.arity c.fst) : c.support.Nonempty

A coordinate of a positive-arity relation has nonempty support.

noncomputable def RelSignature.RelCoord.patternQuotientEquivSupport {S : RelSignature} {V : S.Srt → Type u_1} (c : S.RelCoord V) : Quotient c.pattern ≃ ↥c.support

The pattern's blocks are the support: the quotient by the equality pattern is canonically the set of sort-tagged values read — the "abstract support blocks".

Equations

• c.patternQuotientEquivSupport = (Setoid.quotientKerEquivRange c.taggedValue).trans ((Equiv.refl ((s : S.Srt) × V s)).subtypeEquiv ⋯)

Subset latent indices

@[reducible, inline]

abbrev RelSignature.LatentIndex (S : RelSignature) (V : S.Srt → Type u_4) : Type (max u_4 u_5)

A latent index: a nonempty finite set of sort-tagged vertices. The dissociated functional representation attaches one uniform latent to every such index; the coordinate at c reads only the latents indexed by nonempty subsets of c.support.

Equations

• S.LatentIndex V = { A : Finset ((s : S.Srt) × V s) // A.Nonempty }

noncomputable def RelSignature.LatentIndex.map {S : RelSignature} {V : S.Srt → Type u_1} {W : S.Srt → Type u_2} (f : (s : S.Srt) → V s → W s) (A : S.LatentIndex V) : S.LatentIndex W

The action of a sortwise map on latent indices, through Sigma.map id.

Equations

• RelSignature.LatentIndex.map f A = ⟨Finset.image (Sigma.map id f) ↑A, ⋯⟩

@[simp]

theorem RelSignature.LatentIndex.map_coe {S : RelSignature} {V : S.Srt → Type u_1} {W : S.Srt → Type u_2} (f : (s : S.Srt) → V s → W s) (A : S.LatentIndex V) : ↑(map f A) = Finset.image (Sigma.map id f) ↑A

Transport and equivariance

theorem RelSignature.RelCoord.taggedValue_map {S : RelSignature} {V : S.Srt → Type u_1} {W : S.Srt → Type u_2} (f : (s : S.Srt) → V s → W s) (c : S.RelCoord V) (i : Fin (S.arity c.fst)) : (map f c).taggedValue i = Sigma.map id (fun (s : S.Srt) => f s) (c.taggedValue i)

Tagged values transport along sortwise maps through Sigma.map id (definitional).

theorem RelSignature.injective_sigmaMap_of_sortwise {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)) : Function.Injective (Sigma.map id fun (s : S.Srt) => f s)

Sigma.map id of a sortwise injective family is injective.

theorem RelSignature.RelCoord.pattern_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) : (map f c).pattern = c.pattern

Patterns are invariant under sortwise injections: relabeling by an injective sortwise map neither merges nor splits equality-pattern blocks.

theorem RelSignature.RelCoord.support_map {S : RelSignature} {V : S.Srt → Type u_1} {W : S.Srt → Type u_2} (f : (s : S.Srt) → V s → W s) (c : S.RelCoord V) : (map f c).support = Finset.image (Sigma.map id fun (s : S.Srt) => f s) c.support

Supports transport covariantly: the support of the relabeled coordinate is the image of the support.

theorem RelSignature.LatentIndex.map_map {S : RelSignature} {V : S.Srt → Type u_1} {W : S.Srt → Type u_2} {X : S.Srt → Type u_3} (f : (s : S.Srt) → V s → W s) (g : (s : S.Srt) → W s → X s) (A : S.LatentIndex V) : map g (map f A) = map (fun (s : S.Srt) => g s ∘ f s) A

The latent-index action is functorial: composition.

theorem RelSignature.LatentIndex.map_id {S : RelSignature} {V : S.Srt → Type u_1} (A : S.LatentIndex V) : map (fun (x : S.Srt) => id) A = A

The latent-index action is functorial: identity.

theorem RelSignature.LatentIndex.map_injective {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)) : Function.Injective (map f)

Sortwise injections act injectively on latent indices — the equivariance that lets the eventual sampler pull one latent source back along any relabeling.

theorem RelSignature.LatentIndex.map_subset_support {S : RelSignature} {V : S.Srt → Type u_1} {W : S.Srt → Type u_2} {f : (s : S.Srt) → V s → W s} {c : S.RelCoord V} {A : S.LatentIndex V} (hA : ↑A ⊆ c.support) : ↑(map f A) ⊆ (RelCoord.map f c).support

Subset-latents transport into subset-latents: a nonempty subset of the support of c maps to a nonempty subset of the support of the relabeled coordinate.

noncomputable def RelSignature.LatentIndex.relabelEquiv {S : RelSignature} {V : S.Srt → Type u_1} {W : S.Srt → Type u_2} (σ : (s : S.Srt) → V s ≃ W s) : S.LatentIndex V ≃ S.LatentIndex W

The relabeling equivalence of latent indices along a sortwise family of equivalences: LatentIndex.map packaged as an Equiv, with inverse the action of the sortwise inverses — the bijectivity the latent source's exchangeability pulls back along.

Equations

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

@[simp]

theorem RelSignature.LatentIndex.relabelEquiv_apply {S : RelSignature} {V : S.Srt → Type u_1} {W : S.Srt → Type u_2} (σ : (s : S.Srt) → V s ≃ W s) (A : S.LatentIndex V) : (relabelEquiv σ) A = map (fun (s : S.Srt) => ⇑(σ s)) A

@[simp]

theorem RelSignature.LatentIndex.relabelEquiv_symm_apply {S : RelSignature} {V : S.Srt → Type u_1} {W : S.Srt → Type u_2} (σ : (s : S.Srt) → V s ≃ W s) (A : S.LatentIndex W) : (relabelEquiv σ).symm A = map (fun (s : S.Srt) => ⇑(σ s).symm) A

theorem RelSignature.LatentIndex.map_ne_map_of_disjoint {S : RelSignature} {V : S.Srt → Type u_1} {W : S.Srt → Type u_2} {U : S.Srt → Type u_4} {f : (s : S.Srt) → V s → W s} {g : (s : S.Srt) → U s → W s} (hd : ∀ (s : S.Srt) (x : V s) (y : U s), f s x ≠ g s y) (A : S.LatentIndex V) (B : S.LatentIndex U) : map f A ≠ map g B

Sortwise-disjoint ranges give disjoint latent-index images: latent indices are nonempty, so images under sortwise maps whose ranges are disjoint in every sort can never coincide — the combinatorial heart of dissociation of the evaluated law.

Bundled patterns

structure RelSignature.EqualityPattern (S : RelSignature) (r : S.Rel) : Type

An abstract equality pattern for the relation symbol r: a setoid on the positions together with sort compatibility — equivalent positions carry the same sort. This is the label-free datum the representing kernel f_{r,π} is indexed by; a labeled coordinate only ever enters through RelCoord.equalityPattern.

• toSetoid : Setoid (Fin (S.arity r))

  The equivalence of positions.

• sort_eq ⦃i j : Fin (S.arity r)⦄ : self.toSetoid i j → S.argSort r i = S.argSort r j

  Equivalent positions have equal sorts.

theorem RelSignature.EqualityPattern.ext {S : RelSignature} {r : S.Rel} {x y : S.EqualityPattern r} (toSetoid : x.toSetoid = y.toSetoid) : x = y

theorem RelSignature.EqualityPattern.ext_iff {S : RelSignature} {r : S.Rel} {x y : S.EqualityPattern r} : x = y ↔ x.toSetoid = y.toSetoid

def RelSignature.RelCoord.equalityPattern {S : RelSignature} {V : S.Srt → Type u_1} (c : S.RelCoord V) : S.EqualityPattern c.fst

The bundled equality pattern of a labeled coordinate.

Equations

• c.equalityPattern = { toSetoid := c.pattern, sort_eq := ⋯ }

@[simp]

theorem RelSignature.RelCoord.equalityPattern_toSetoid {S : RelSignature} {V : S.Srt → Type u_1} (c : S.RelCoord V) : c.equalityPattern.toSetoid = c.pattern

theorem RelSignature.RelCoord.equalityPattern_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) : (map f c).equalityPattern = c.equalityPattern

Bundled patterns are invariant under sortwise injections.

def RelSignature.EqualityPattern.blockSort {S : RelSignature} {r : S.Rel} (π : S.EqualityPattern r) : Quotient π.toSetoid → S.Srt

The sort of a block: argSort descends to the pattern's quotient by sort compatibility. Per-sort block counts or multisets are derived from this, not stored.

Equations

• π.blockSort = Quotient.lift (S.argSort r) ⋯

@[simp]

theorem RelSignature.EqualityPattern.blockSort_mk {S : RelSignature} {r : S.Rel} (π : S.EqualityPattern r) (i : Fin (S.arity r)) : π.blockSort ⟦i⟧ = S.argSort r i

Local latent indices

@[reducible, inline]

abbrev RelSignature.PatternLatentIndex {S : RelSignature} {r : S.Rel} (π : S.EqualityPattern r) : Type

The pattern-local latent indices: nonempty finite subsets of the blocks of an abstract pattern — the label-free, order-free argument domain of the representing kernel f_{r,π} : (PatternLatentIndex π → I) → ….

Equations

• RelSignature.PatternLatentIndex π = { A : Finset (Quotient π.toSetoid) // A.Nonempty }

@[implicit_reducible]

noncomputable instance RelSignature.instFintypeQuotientFinArityToSetoid {S : RelSignature} {r : S.Rel} (π : S.EqualityPattern r) : Fintype (Quotient π.toSetoid)

The blocks of a pattern form a finite type (positions are Fin; classical decidability of the setoid).

Equations

• RelSignature.instFintypeQuotientFinArityToSetoid π = Quotient.fintype π.toSetoid

@[implicit_reducible]

noncomputable instance RelSignature.instFintypePatternLatentIndex {S : RelSignature} {r : S.Rel} (π : S.EqualityPattern r) : Fintype (PatternLatentIndex π)

Pattern-local latent indices form a finite type — the local latent source of a single coordinate is a finite product, as the evaluator layer requires.

Equations

• RelSignature.instFintypePatternLatentIndex π = Subtype.fintype Finset.Nonempty

instance RelSignature.instFinitePatternLatentIndex {S : RelSignature} {r : S.Rel} (π : S.EqualityPattern r) : Finite (PatternLatentIndex π)

@[reducible, inline]

abbrev RelSignature.CoordLatentIndex {S : RelSignature} {V : S.Srt → Type u_1} (c : S.RelCoord V) : Type (max u_1 u_4)

The coordinate-local latent indices: nonempty subsets of the support — the labeled avatar of PatternLatentIndex, and the sub-collection of the global LatentIndex a single coordinate reads (canonical projection CoordLatentIndex.toLatentIndex).

Equations

• RelSignature.CoordLatentIndex c = { A : Finset ((s : S.Srt) × V s) // A.Nonempty ∧ A ⊆ c.support }

def RelSignature.CoordLatentIndex.toLatentIndex {S : RelSignature} {V : S.Srt → Type u_1} {c : S.RelCoord V} (A : CoordLatentIndex c) : S.LatentIndex V

The canonical projection into the global latent indices: forget the support bound.

Equations

• A.toLatentIndex = ⟨↑A, ⋯⟩

@[simp]

theorem RelSignature.CoordLatentIndex.toLatentIndex_coe {S : RelSignature} {V : S.Srt → Type u_1} {c : S.RelCoord V} (A : CoordLatentIndex c) : ↑A.toLatentIndex = ↑A

theorem RelSignature.CoordLatentIndex.toLatentIndex_injective {S : RelSignature} {V : S.Srt → Type u_1} (c : S.RelCoord V) : Function.Injective toLatentIndex

noncomputable def RelSignature.patternLatentIndexEquivCoord {S : RelSignature} {V : S.Srt → Type u_1} (c : S.RelCoord V) : PatternLatentIndex c.equalityPattern ≃ CoordLatentIndex c

The canonical equivalence between pattern-local and coordinate-local latent indices, through patternQuotientEquivSupport: the kernel's order-free domain is the labeled coordinate's subset-latent collection.

Equations

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

def RelSignature.PatternLatentIndex.congr {S : RelSignature} {r : S.Rel} {π π' : S.EqualityPattern r} (h : π = π') : PatternLatentIndex π ≃ PatternLatentIndex π'

Transport of pattern-local indices along an equality of patterns.

Equations

• RelSignature.PatternLatentIndex.congr h = h ▸ Equiv.refl (RelSignature.PatternLatentIndex π)

noncomputable def RelSignature.CoordLatentIndex.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) : CoordLatentIndex c ≃ CoordLatentIndex (RelCoord.map f c)

The two-way relabeling equivalence of coordinate-local latent indices along a sortwise injection — not merely the one-way map_subset_support: the forward direction is the image under Sigma.map id (so it agrees with the global LatentIndex.map, CoordLatentIndex.congrMap_toLatentIndex), and the inverse is the preimage, well-defined because the image support bounds the target.

Equations

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

@[simp]

theorem RelSignature.CoordLatentIndex.congrMap_toLatentIndex {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) : ((congrMap hf c) A).toLatentIndex = LatentIndex.map f A.toLatentIndex

Coherence with the global action: the local relabeling equivalence projects to the global LatentIndex.map — the two transports never disagree.

Examples: binary, diagonal, ternary, bipartite

@[reducible, inline]

abbrev RelSignature.PatternExamples.binarySig : RelSignature

A local one-sort binary signature (kept local so this generic file does not depend on the directed development; the directed digraphSig has the same shape).

Equations

• RelSignature.PatternExamples.binarySig = { Srt := Unit, Rel := Unit, arity := fun (x : Unit) => 2, argSort := fun (x : Unit) (x_1 : Fin 2) => () }

@[reducible]

def RelSignature.PatternExamples.binaryExample (i j : ℕ) : binarySig.RelCoord fun (x : binarySig.Srt) => ℕ

The binary coordinate at an ordered pair.

Equations

• RelSignature.PatternExamples.binaryExample i j = ⟨(), ![i, j]⟩

@[reducible, inline]

abbrev RelSignature.PatternExamples.ternarySig : RelSignature

A one-sort ternary signature.

Equations

• RelSignature.PatternExamples.ternarySig = { Srt := Unit, Rel := Unit, arity := fun (x : Unit) => 3, argSort := fun (x : Unit) (x_1 : Fin 3) => () }

@[reducible]

def RelSignature.PatternExamples.ternaryExample : ternarySig.RelCoord fun (x : ternarySig.Srt) => ℕ

The running ternary coordinate (0, 1, 0): a repeated entry.

Equations

• RelSignature.PatternExamples.ternaryExample = ⟨(), ![0, 1, 0]⟩

@[reducible, inline]

abbrev RelSignature.PatternExamples.bipartiteSig : RelSignature

A two-sort bipartite binary signature: position 0 is a left vertex, position 1 a right vertex.

Equations

• RelSignature.PatternExamples.bipartiteSig = { Srt := Bool, Rel := Unit, arity := fun (x : Unit) => 2, argSort := fun (x : Unit) (i : Fin 2) => decide (i = 1) }

@[reducible]

def RelSignature.PatternExamples.bipartiteExample (n : ℕ) : bipartiteSig.RelCoord fun (x : bipartiteSig.Srt) => ℕ

The running bipartite coordinate with equal raw values in both positions.

Equations

• RelSignature.PatternExamples.bipartiteExample n = ⟨(), ![n, n]⟩