R4: dissociated functional AHK for relational structures (AHK umbrella #103)

[cameronfreer]

Child of #103; depends on R3 (#106). The functional AHK representation of a dissociated exchangeable relational structure: a measurable function of subset-indexed i.i.d. latents. This is the Aldous–Hoover–Kallenberg core.

Tagged latents — indexed by nonempty finite sets of tagged vertices, not subsets of sorts — implemented in #137 as

LatentIndex S (Vinfinite S)  -- {A : Finset (Σ s : S.Srt, ℕ) // A.Nonempty}

• for each latent index A : LatentIndex S (Vinfinite S), an i.i.d. latent ξ_A (uniform on [0,1]);
• a relation coordinate has a tagged support (RelCoord.support — its argument vertices, each carrying its sort); its representing kernel f_{r,π} reads the value from the latents ξ_A over the nonempty subsets A of that coordinate's tagged support (CoordLatentIndex, canonically identified with the label-free PatternLatentIndex via patternLatentIndexEquivCoord);
• the equality pattern π (EqualityPattern — a setoid on argument positions compatible with argSort: two positions may coincide only if same-sort) folds coincident arguments into the diagonal terms. feat: R4 design checkpoint — equality patterns, supports, subset latent indices #137/feat: R4 evaluator layer (#107) — measurable kernels over pattern-local latents #138 handle patterns and diagonals uniformly, so distinct-coordinate vs diagonal is not a project boundary.

The dissociated theorem omits ξ_∅ (the global / empty-tag latent — hence the Nonempty constraint in the index type); R5 (#108) restores it for the general mixture.

Milestones:

1. feat: R4 design checkpoint — equality patterns, supports, subset latent indices #137 interface (equality patterns, supports, pattern/coordinate latent indices) — done.
2. feat: R4 evaluator layer (#107) — measurable kernels over pattern-local latents #138 measurable evaluator + equivariance (RelKernelFamily, evalStructure, evalStructure_relabel) — done.
3. feat: R4 sampler layer (#107) — latent source + exchangeable, dissociated evaluated law #139 i.i.d. latent source + evaluated exchangeable, dissociated law (latentSource, RelKernelFamily.evalLaw, evalLaw_isDissociated) — done.
4. Converse infrastructure: adapt Mathlib's kernel randomization theorem (ProbabilityTheory.Kernel.exists_measurable_map_eq_unitInterval, Mathlib.Probability.Kernel.Representation) to the project's uniform01 (small adapter PR — via unitInterval.measurePreserving_coe + Set.projIcc — plus standard-Borel instances for the countable Boolean bundles to be randomized); then the relative-independence factor σ-algebras.
5. Converse representation + finite-law identification + graph/digraph regressions.

Pin exactly one external theorem — the specific Kallenberg (Probabilistic Symmetries and Invariance Principles) representation of jointly / separately exchangeable arrays, with its precise subset-indexed-latent indexing convention — before implementing milestone 4. R0 (#110) carries "locate and cite the exact theorem + convention" as an acceptance item; note the mixed multi-sorted action is not literally covered by Kallenberg 7.22/7.23, so the citation should record the delta.

[cameronfreer]

The hard converse: the evaluator construction is universal for dissociated exchangeable laws

With the R4 evaluator layer merged (#138) and the sampler layer merged (#139: the latent
source and the exchangeable, dissociated evaluated law), the remaining content of this issue
is the converse representation theorem. Formally, the target is
essentially:

theorem exists_kernelFamily_of_isDissociated [Fintype S.Srt] [Countable S.Rel]
    (L : InfiniteRelExchangeableLaw S)
    (hL : L.IsDissociated) :
    ∃ F : RelKernelFamily S,
      (iidUniformSource (LatentIndex S (Vinfinite S))).map F.evalStructure = L.law

The instance assumptions match the R2 scope ([Fintype S.Srt] [Countable S.Rel] throughout
the law equivalence). One open statement decision: either assume NoNullary S (matching the
R0 scope) or explicitly support nullary symbols by proving that dissociation makes them
deterministic.

The easy direction —

kernel family + independent subset latents → exchangeable, dissociated random structure

— is proved (#139). The converse reconstructs a kernel family from an abstract law:

dissociated exchangeable law → measurable functions $f_{r,\pi}$ of independent subset latents

For a tuple with tagged support $A$, its relation value must become a measurable function of

$$(U_B)_{\varnothing \ne B \subseteq A}.$$

The same latent $U_B$ is shared by every relation coordinate using $B$. That sharing is essential:
for a digraph, $X_{ij}$ and $X_{ji}$ both see $U_{{i,j}}$, allowing arbitrary reciprocal-edge
dependence.

Why the converse is hard

It is not enough to condition on the observable structures on proper subsets. In a graphon model,
for example, the vertex latent $U_i$ can contain much more information than the loops or unary
relations observed at $i$.

One expected proof route constructs hidden factor σ-algebras associated with each finite tagged
vertex set (the mixed multi-sorted action is not literally covered by Kallenberg 7.22/7.23, so
this route needs its own bookkeeping):

• $\mathcal F_\varnothing$: global invariant information;
• $\mathcal F_{{i}}$: vertex-level information;
• $\mathcal F_{{i,j}}$: pair-level information;
• and so on.

One then proves the appropriate relative-independence statements and represents each successive
factor using a fresh uniform random variable $U_A$. A measurable randomization or "noise
outsourcing" theorem converts each regular conditional distribution into a measurable function of
the lower-level factors and one fresh uniform.

After that:

1. Exchangeability shows the resulting function depends only on the relation symbol and abstract
   equality pattern, producing $f_{r,\pi}$.
2. The patternLatentIndexEquivCoord machinery converts its abstract block arguments into the
   actual subset latents of a labeled coordinate.
3. Finite-dimensional distributions are shown to agree with L.
4. RelStructure.ext_of_map_restrictFin upgrades this to equality of infinite laws.

Where dissociation enters

In the general AHK representation there is also a global latent $U_\varnothing$:

$$X_c = f_{r,\pi}\bigl(U_\varnothing, (U_B)_{\varnothing \ne B \subseteq \operatorname{supp}(c)}\bigr).$$

Dissociation — or equivalently the R3 extremality/ergodicity conditions (#106) — makes the
invariant factor $\mathcal F_\varnothing$ trivial. More precisely, extremality makes the
conditional component law given $U_\varnothing$ equal to the original law almost surely; one then
fixes a good global-latent value. This is a law-level removal of $U_\varnothing$ — not necessarily
pointwise independence of the original representing function — and it leaves exactly the nonempty
LatentIndex interface built in #137.

For a general exchangeable law, R5 (#108) restores $U_\varnothing$. Conceptually it selects the
dissociated component in the ergodic decomposition. Formalizing that selection measurably is
harder than the dissociated converse.

Sensible implementation campaign

The converse splits into substantial pieces:

1. Randomization, as a small adapter PR rather than a new foundational proof: Mathlib already
   has the theorem — ProbabilityTheory.Kernel.exists_measurable_map_eq_unitInterval
   (Mathlib.Probability.Kernel.Representation) gives a jointly measurable f : X → I → Y with
   volume.map (f x) = κ x for a Markov kernel into a standard Borel space. Expose it, adapt its
   I-valued uniform input to the project's uniform01 : Measure ℝ (via
   unitInterval.measurePreserving_coe and a measurable retraction such as Set.projIcc), and
   establish the standard-Borel instances for the particular countable Boolean bundles the converse
   will randomize.
2. The finite-subset factor σ-algebras and their relative-independence theorem.
3. Recursive realization by $U_A$, inducting on support size.
4. Descent from labeled coordinates to EqualityPattern kernels.
5. Finite-marginal identification and infinite-law extensionality.
6. Graph and digraph specialization tests.

The representing kernel family will not be unique: measure-preserving transformations of the
latent uniforms produce different kernels with the same law. The theorem should therefore assert
existence and equality of induced laws, not uniqueness of RelKernelFamily.

[cameronfreer]

Design checkpoint before converse piece 2: the factor σ-algebras

Piece 1 (randomization) is merged (#140). Before implementing piece 2 — the finite-subset
factor σ-algebras and their relative-independence theorem — the design needs to be settled,
because the naive candidate is wrong and the strict-versus-mod-null boundary matters.

The crucial warning: the factor at $A$ cannot merely be generated by the relation
coordinates whose vertices lie in $A$. That loses hidden vertex information — in a graphon
model the vertex latent $U_i$ carries much more than the loops or unary relations observed at
$i$, and the factor at ${i}$ must capture all of it.

Three distinct objects — do not conflate them:

1. A raw, law-independent fixingAlgebra A: the σ-algebra of events invariant under all
   finitely supported sortwise permutations fixing every tagged vertex of $A$ — the
   $A$-relativized version of the existing RelStructure.invariantAlgebra (whose stabilizer
   is the full finitely supported group at $A = \varnothing$). The SortwiseFinSupp group
   infrastructure (one/mul/inv) relativizes directly. This object mentions no measure.
2. Conditional independence of these algebras under L.law — a statement about one fixed
   exchangeable law, not about the raw algebras alone.
3. A standard-Borel factor realization, only modulo L.law-null sets. Do not require
   $(\Omega, \texttt{fixingAlgebra } A)$ itself to be a StandardBorelSpace — an invariant
   sub-σ-algebra (or its completion) need not admit that literal structure. The useful target
   is a measurable factor map
   $$q_A : \Omega \to Z_A$$
   into a standard Borel $Z_A$, with fixingAlgebra A represented by
   MeasurableSpace.comap qA modulo null sets. Conditional expectations and independence
   are likewise stated modulo L.law; the feat: R4 converse piece 1 (#107) — uniform01 kernel-randomization adapter #140 randomization adapter then applies to the
   regular conditional distributions along these factor maps.

The initial exact (strict, law-free where possible) API:

• $A \subseteq B \Rightarrow$ fixingAlgebra A ≤ fixingAlgebra B (monotonicity: larger fixed
  set = smaller stabilizer = more invariant events);
• transport under relabeling: fixingAlgebra A maps to fixingAlgebra (σ '' A), compatibly
  with the LatentIndex.map / relabelEquiv action;
• fixingAlgebra ∅ = RelStructure.invariantAlgebra — so dissociation/ergodicity (R3, R3: generic dissociation/extremality for relational structures (AHK umbrella #103) #106)
  makes exactly the bottom factor trivial;
• conditional independence of fixingAlgebra A and fixingAlgebra B over
  fixingAlgebra (A ∩ B) under a dissociated law. This last theorem is the real
  mathematical core, and its precise statement should be settled against Kallenberg
  (Probabilistic Symmetries, ch. 7) and Austin's exchangeability notes before
  implementation — noting again that the mixed multi-sorted action is not literally covered
  by Kallenberg 7.22/7.23, so the statement needs its own verification for this setting.

Sequencing: settle the strict-versus-mod-null signatures above first; only then write the
factor realization (object 3), and only after all of it the recursive latent construction
(piece 3, inducting on support size).