Relational signatures and their structure carriers (AHK umbrella #103, R0 design checkpoint)

A deliberately small, dependency-light checkpoint (issue #110) that locks the carrier design for the generic Aldous–Hoover–Kallenberg program before R1/R2 build size vectors, sortwise embeddings, topology, and measure theory on top of it. There is no topology, no probability, no projective extension, and no extremality here — only the data design and the sortwise-map machinery that the later layers will reuse, so the carrier decision stays easy to revise.

Contents

• RelSignature — a purely relational, multi-sorted signature (no function symbols, no constants): a type of sort labels, a type of relation symbols, an arity, and the sort of each argument position;
• RelCoord / RelStructure — the coordinate type of a structure over a sort-indexed value family, and a Boolean-valued structure on those coordinates;
• NoNullary — the arity-positivity hypothesis, kept external (a predicate, not a field of RelSignature) so nullary relations can be admitted later without redesigning the signature;
• Vfinite / Vinfinite — the finite (size-vector) and infinite (ℕ) value carriers;
• RelCoord.map / RelStructure.comap — the action of a sortwise family of maps ∀ s, V s → W s on coordinates and on structures (the exact machinery R1/R2 relabelling and consistency will rely on);
• worked Examples: the one-sort binary digraph signature, the two-sort binary bipartite signature, and a one-sort ternary signature with a repeated-coordinate tuple (i, i, j) — the latter exercises the equality-pattern design that is the genuinely new difficulty at arbitrary arity.

Design decisions locked here

• Sort-label field name. Sort is a reserved token in Lean 4, so the field is named Srt (accessed as S.Srt). This is the only cosmetic deviation from the Σ.Sort notation used in the issue discussion.
• Universes. The sort-label type and the relation-symbol type share a single universe Type u (RelSignature : Type (u+1)); the value carrier V : S.Srt → Type v uses an independent universe v. A split Type u/Type u' for sorts vs. relations is possible but unnecessary (it only ever appears as max u u') and trips the checkUnivs linter, so it is deferred. The worked examples all live in Type (universe 0).
• Boolean relations. RelStructure is RelCoord → Bool. Finite-valued relations are a later extension; Boolean is already the full campaign.
• Nullary relations. Admitted structurally (an arity R = 0 relation is legal data), but the intended theorems assume NoNullary; the empty-tag / global-latent ξ_∅ behaviour is restored only in R5 (#108).

External representation theorem this program targets (R0 acceptance item)

The functional representation formalized in R4 (#107) is the Aldous–Hoover–Kallenberg theorem. In Kallenberg, Probabilistic Symmetries and Invariance Principles (Springer, 2005), §7.5: Theorem 7.22 is the jointly exchangeable representation of an array X : ℕ^d → E as X_J = f((ξ_{J'})_{J' ⊆ J}) (measurable f, i.i.d. U[0,1] latents ξ indexed by the subsets J' ⊆ J), and Corollary 7.23 is its separately exchangeable, fixed-dimensional consequence. The general multi-sorted action here mixes joint and separate symmetries, so it is not literally either single statement — R1/R2 make the exact mixture explicit. For relational structures the latents are indexed by finite subsets of tagged vertices Σ s : S.Srt, ℕ; R4 formalizes the dissociated specialization without the empty-subset latent ξ_∅, and R5 (#108) restores the full general-law form with ξ_∅. Locating and confirming these exact statements against the printing is part of R0's acceptance.

structure RelSignature : Type (u + 1)

A purely relational, multi-sorted signature: sort labels Srt, relation symbols Rel, an arity for each relation, and the sort argSort R i of each argument position i of R. No function symbols or constants. (The field is Srt because Sort is a reserved token in Lean 4.)

• Srt : Type u

  The type of sort labels.

• Rel : Type u

  The type of relation symbols.

• arity : self.Rel → ℕ

  The arity of each relation symbol.

• argSort (R : self.Rel) : Fin (self.arity R) → self.Srt

  The sort of each argument position of each relation.

@[reducible, inline]

abbrev RelSignature.RelCoord (S : RelSignature) (V : S.Srt → Type v) : Type (max v u_1)

A coordinate of a relational structure over the sort-indexed value family V: a relation symbol R together with a value V (argSort R i) in each argument position i.

Equations

• S.RelCoord V = ((R : S.Rel) × ((i : Fin (S.arity R)) → V (S.argSort R i)))

@[reducible, inline]

abbrev RelSignature.RelStructure (S : RelSignature) (V : S.Srt → Type v) : Type (max v u_1)

A relational structure over the value family V: a Boolean value at every coordinate (whether the tuple stands in the relation). Reducible so that it transparently inherits the Boolean-product topology and measurable-space structure (R1b).

Equations

• S.RelStructure V = (S.RelCoord V → Bool)

def RelSignature.NoNullary (S : RelSignature) : Prop

Arity positivity, kept as an external predicate rather than a field of RelSignature, so nullary relations can be added later without changing the signature.

Equations

• S.NoNullary = ∀ (R : S.Rel), 0 < S.arity R

@[reducible, inline]

abbrev RelSignature.Vfinite {S : RelSignature} (n : S.Srt → ℕ) : S.Srt → Type

The finite value carrier for a size vector n : S.Srt → ℕ: sort s has n s vertices.

Equations

• RelSignature.Vfinite n s = Fin (n s)

@[reducible, inline]

abbrev RelSignature.Vinfinite (S : RelSignature) : S.Srt → Type

The infinite value carrier: every sort has vertex set ℕ.

Equations

• S.Vinfinite x✝ = ℕ

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

The action of a sortwise family of maps f : ∀ s, V s → W s on coordinates: relabel each argument by the map for its sort, keeping the relation symbol. This is the coordinate half of the relabelling / consistency machinery R1 and R2 will build on.

Equations

• RelSignature.RelCoord.map f c = ⟨c.fst, fun (i : Fin (S.arity c.fst)) => f (S.argSort c.fst i) (c.snd i)⟩

def RelSignature.RelStructure.comap {S : RelSignature} {V : S.Srt → Type u_1} {W : S.Srt → Type u_2} (f : (s : S.Srt) → V s → W s) : S.RelStructure W → S.RelStructure V

The pullback of a structure along a sortwise family of maps: comap f g asks whether the f-image tuple stands in g. (For a sortwise permutation this is the generic relabelling action.)

Equations

• RelSignature.RelStructure.comap f g c = g (RelSignature.RelCoord.map f c)

@[simp]

theorem RelSignature.RelStructure.comap_apply {S : RelSignature} {V : S.Srt → Type u_1} {W : S.Srt → Type u_2} (f : (s : S.Srt) → V s → W s) (g : S.RelStructure W) (c : S.RelCoord V) : comap f g c = g (RelCoord.map f c)

@[simp]

theorem RelSignature.RelCoord.map_fst {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).fst = c.fst

Worked examples

The example signatures are abbrevs (reducible) so that the acceptance checks reduce by rfl; R1 will introduce its own opaque definitions.

@[reducible, inline]

abbrev RelSignature.Examples.digraphSig : RelSignature

Directed graphs: one sort, one binary relation, ordered arguments, diagonal allowed (the R1 instance underlying #85).

Equations

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

@[reducible, inline]

abbrev RelSignature.Examples.bipartiteSig : RelSignature

Bipartite / separately exchangeable: two sorts, one binary relation whose first argument is the first sort and second argument the second sort.

Equations

• RelSignature.Examples.bipartiteSig = { Srt := Bool, Rel := Unit, arity := fun (x : Unit) => 2, argSort := fun (x : Unit) => ![false, true] }

@[reducible, inline]

abbrev RelSignature.Examples.ternarySig : RelSignature

A one-sort ternary relation — the smallest signature that exercises repeated argument coordinates (the equality-pattern design of R4/#107).

Equations

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

@[reducible, inline]

abbrev RelSignature.Examples.ternaryRepeated (i j : ℕ) : ternarySig.RelCoord ternarySig.Vinfinite

A ternary coordinate (i, i, j) with the first two arguments equal — the design admits repeated coordinates, and their equality pattern is intrinsic to the tuple.

Equations

• RelSignature.Examples.ternaryRepeated i j = ⟨(), ![i, i, j]⟩

@[reducible, inline]

abbrev RelSignature.Examples.bipartiteEdge (a b : ℕ) : bipartiteSig.RelCoord bipartiteSig.Vinfinite

An example bipartite coordinate: the ordered pair (a, b) with a in the first sort and b in the second.

Equations

• RelSignature.Examples.bipartiteEdge a b = ⟨(), ![a, b]⟩