Child of #103; depends on R4 (#107) and R3 (#106). The general (non-dissociated) mixture representation: an arbitrary exchangeable relational law is a mixture of dissociated (ergodic) ones. Two deliverables, split into two sub-issues:
- R5a — law-level ergodic decomposition: every exchangeable law is a barycenter (
Measure.bind) of ergodic exchangeable laws over the invariant σ-algebra. This is the measure-theoretic decomposition, no functional form. Require existence AND uniqueness of the mixing probability measure on the space of ergodic relational laws (the barycenter representation is unique).
- R5b — functional representation with
ξ_∅: the full AHK functional form of a general law, adjoining the global latent ξ_∅ (the empty-tag latent) to the R4 subset-latents; conditioning on ξ_∅ recovers a dissociated law (R4).
Two admissible routes:
- direct AHK — prove R5b directly via the Kallenberg representation with
ξ_∅, then read off R5a;
- mixture-first — prove R5a via the invariant-σ-algebra ergodic decomposition (Mathlib ergodic-theory /
M.law-disintegration), then upgrade to R5b using R4 fiberwise.
Caveat on the fiberwise route. "Apply R4 fiberwise" is not free: it needs a measurably chosen family of representing functions over the fibers (a measurable-selection obligation). The direct Kallenberg theorem (route 1) may be the cleaner path, sidestepping the selection. Whether a #62-style measurable-selection obstruction actually arises depends on the route and target space — do not declare measurable selection mandatory up front, but do budget for it on route 2.
Child of #103; depends on R4 (#107) and R3 (#106). The general (non-dissociated) mixture representation: an arbitrary exchangeable relational law is a mixture of dissociated (ergodic) ones. Two deliverables, split into two sub-issues:
Measure.bind) of ergodic exchangeable laws over the invariant σ-algebra. This is the measure-theoretic decomposition, no functional form. Require existence AND uniqueness of the mixing probability measure on the space of ergodic relational laws (the barycenter representation is unique).ξ_∅: the full AHK functional form of a general law, adjoining the global latentξ_∅(the empty-tag latent) to the R4 subset-latents; conditioning onξ_∅recovers a dissociated law (R4).Two admissible routes:
ξ_∅, then read off R5a;M.law-disintegration), then upgrade to R5b using R4 fiberwise.Caveat on the fiberwise route. "Apply R4 fiberwise" is not free: it needs a measurably chosen family of representing functions over the fibers (a measurable-selection obligation). The direct Kallenberg theorem (route 1) may be the cleaner path, sidestepping the selection. Whether a #62-style measurable-selection obstruction actually arises depends on the route and target space — do not declare measurable selection mandatory up front, but do budget for it on route 2.