D4: the directed correspondence — D4a existence (raw), D4b unique quotient equivalence (after D5)

[cameronfreer]

Sub-issue of the directed umbrella (#84); split per review — DJ Theorem 9.1 gives existence of a random raw digraphon, but its distribution is not unique before quotienting by weak isomorphism:

D4a — existence/surjectivity using raw digraphons (after D1–D3, #85–#87): every infinite exchangeable digraph law is the law of a sampled random raw digraphon (mixture over raw digraphons; no uniqueness claim). The Prokhorov/cylinder-extensionality/collision architecture reuses.

D5 (#89) — directed determination, weak isomorphism, quotient topology and analytics — the prerequisite for uniqueness.

D4b — the unique quotient-level equivalence (after D5):

ProbabilityMeasure (DigraphonSpace) ≃ InfiniteExchangeableDigraphLaw

with extremality (dissociated/Dirac), empirical directed convergence, and fixed-digraphon almost-sure convergence.

Sequencing guard: do not promise uniqueness (D4b) using a quotient that #89 has not constructed.

[cameronfreer]

Roadmap correction (2026-07-16 review): this issue as written suggests Prokhorov extraction on raw digraphons, but raw digraphons carry no compact topology at this stage, so that route is not available. Raw existence before D5 needs a direct AHK/Kallenberg representation — which is naturally the generic R4/R5 machinery — or else it should wait for D5's quotient space.

Revised sequencing (post-#87, which is now closing via #129):

1. Public without-replacement density triangle: t, t_inj, t_ind (DJ §2) #94 — the t/t_inj/t_ind directed interlude (two compact PRs).
2. Generic R3 (R3: generic dissociation/extremality for relational structures (AHK umbrella #103) #106): R3a sortwise block restrictions + exact finite-event factorization; R3b generic restriction independence, vertex-tail and invariant σ-algebras; R3c dissociated ↔ restriction-independent ↔ tail-trivial ↔ ergodic ↔ extreme, with graph and digraph specializations as regression tests.
3. R4/R5 — the generic functional AHK and mixture theorem; D4a then becomes a directed specialization of that machinery, and this issue's statement should be revised accordingly before D4a work begins.