Umbrella: Aldous–Hoover–Kallenberg for multi-sorted relational structures

[cameronfreer]

A generic AHK program for purely relational languages (no function symbols, no constants), separate from the graph (#33-closed) and directed (#84) campaigns. Existing issues cover graph and (upcoming) digraph specializations but not the generic relational-structure / arbitrary-arity program. Deliberately a NEW umbrella — do not broaden #84 until it becomes unmanageable.

Why a separate umbrella

• P1 (arbitrary-arity jointly / separately exchangeable arrays): only partial infra in D1: directed graph foundations (InfiniteDigraph space) #85 / D2: finite and infinite exchangeable digraph laws #86 and the bipartite note in Umbrella: Directed Diaconis–Janson and digraphons (DJ §9, Cai–Ackerman–Freer) #84; abstract kernel randomization in AH-final 1: abstract randomization of the graphon-class kernel #61. No relational signature, arbitrary arity, multi-sorted carriers, generic exchangeable laws, or general AHK subset-latent representation is tracked.
• P2 (dissociation ↔ ergodicity / extremality for arrays): the graph case is complete — restriction-independence / tail / dissociation (Complete DJ Theorem 5.5: restriction-independence and vertex-tail formulations (child of #59) #91) and the invariant-σ-algebra / ergodicity form (Invariant σ-algebra and ergodic-decomposition form of extremality #59). No generic theorem for exchangeable relational structures.
• Scoping: explicit functional Aldous–Hoover formula (architecture; split into #61–#64) #60–AH-final 3: the literal U₀, Uᵢ, Uᵢⱼ functional formula #63 are not generic AHK coverage: they concern symmetric binary graph arrays + graphon representative selection.

Signature (purely relational)

structure RelSignature where
  Sort : Type
  Rel : Type
  arity : Rel → ℕ
  argSort : (R : Rel) → Fin (arity R) → Sort

• one sort ⟹ jointly exchangeable arrays;
• two sorts + a binary relation ⟹ separately exchangeable / bipartite arrays;
• several relation symbols ⟹ heterogeneous random relational structures;
• directed graphs ⟹ one binary relation, ordered arguments, diagonals permitted.

Scope assumptions (for compact Polish infinite-structure spaces): [Fintype Sort], [Countable Rel], arity finite (supplied by Nat). Nullary relations: keep 0 < arity R as an external hypothesis supplied where needed — NOT a field of RelSignature (see #110) — so nullary relations, which introduce global bits and special dissociated-representation behavior, can be added later without redesigning the signature.

Children

R0 design checkpoint (#110); R1 finite / infinite structures (carrier / coordinate / cylinder / extensionality — #104); R2 exchangeable laws (size-vector marginals, sortwise consistency, compactness extension, invariant-law equivalence — #105); R3 generic extremality characterization (exact structure laws, NOT Möbius — #106); R4 dissociated functional AHK (subset-of-tagged-vertex latents + equality patterns — #107); R5 general mixture (ergodic decomposition + functional representation — #108); R6 specialization equivalences (#109).

Interaction with the directed campaign

Adjusted near-term order: #59 → R0 → R1 → D1 (#85) as an R1 bridge → R2 → D2 (#86) as a thin R2 bridge → D3 (#87). Build the compact-product / projective-extension machinery once in R1 / R2. D3 stays concrete (five-component CAF digraphon + categorical sampler are genuinely directed-specific).