refactor(Exchangeability): rename conditional IID mixture representation

[kim-em]

What changed

Renames the roadmap's ConditionallyIID representation predicate to IsIIDMixture, with the named-directing-measure relation becoming IsIIDMixtureWith. Updates the suggested Lean target, theorem milestones, public API list, and prose consistently.

Why

The predicate states an unconditional finite-dimensional mixture identity. It does not formalize conditional independence relative to a sigma-algebra or random element, so ConditionallyIID gave the API a stronger and materially different standard probabilistic meaning than its definition supplied.

The roadmap now explicitly distinguishes an i.i.d. mixture representation from genuine conditional i.i.d.-ness, which would require conditional laws or almost-sure conditional-expectation identities.

Impact

Once this roadmap change lands, TauCeti can rename the existing mixture-representation API without contradicting the human-owned specification. No mathematical target is removed or weakened.

Validation

• lake build
• git diff --check

[cameronfreer]

This correctly identifies a mismatch between what TauCeti has proved (about mixtures) and how it has labeled them ("conditionally IID", etc.). But in the process of changing the naming, it eliminates the conditional independence route entirely (which is proving something stronger than the mixture, and which is needed for later results about the directing random measure ν that care about it as a random variable rather than just about its law). More details below.

---

🤖 detailed review/update from Fable 5 with review by GPT 5.6

The diagnosis here is correct: the landed predicate is an unconditional mixture identity — blockLaw μ X k = μ.bind (fun ω => (ν ω)^{⊗m}) — and ConditionallyIID gave it a stronger standard meaning than the definition supplied. The decisive way to see the gap: the relation constrains only the marginal law of each block, never the joint law of (ν, X). So if X is exchangeable with a nondegenerate mixing law and canonical directing measure ν̃, any independent copy ν of ν̃ (on a rich enough space) also witnesses the mixture identity, while P[X ∈ · ∣ ν] is just the unconditional law — X is not conditionally i.i.d. given that ν.

I've pushed a commit that keeps the diagnosis but completes the fix in both directions:

1. Naming: MixedIID / MixedIIDWith instead of IsIIDMixture. This is Kallenberg's exact terminology for the unconditional identity, it reads adjective-style like the neighboring Exchangeable / Contractable / ConditionallyIID, and it avoids IsIIDMixture's suggestion that the predicate applies to the mixing distribution rather than the process. The fixed-witness relation MixedIIDWith μ X ν is now actually pinned (the README used the …With name but Suggested.lean inlined it), with the existential wrapper over it. A ν witnessing only the mixture identity is a mixing representative; directing measure is reserved for the conditional witness.

2. The genuine conditional notion is reinstated — and remains the summit. ConditionallyIIDWith μ X ν is pinned as a joint-law disintegration — Law(ν, block) = ∫ δ_{ν(ω)} ⊗ (ν(ω))^{⊗m} dμ(ω), i.e. conditionally on ν the block is i.i.d. ν (Kallenberg 2005, §1.1 eq. (2); Thm 1.1 there is the equivalence with exchangeability) — stated with the same bind/pi toolkit, no conditional expectations needed. Crucially, the headline returns to contractable ↔ exchangeable ↔ conditionally i.i.d., deFinetti and the Ryll–Nardzewski equivalence conclude ConditionallyIID (the rename-only version left them at the mixture identity, which omits the stronger witness-level conditional conclusion — under the standard-Borel infinite-sequence hypotheses the existential properties are ultimately equivalent; the strictness is at fixed ν), the hard route theorem conditionallyIID_of_contractable is pinned explicitly (Contractable μ X → ConditionallyIID μ X) with conditionallyIID_of_exchangeable alongside, and the mixture forms (mixedIID_of_contractable, deFinetti_mixture) are retained as integrated-out corollaries.

3. The conditional target is connected to the proof routes, not just named. The fixed-witness bridge ConditionallyIIDWith μ X ν → MixedIIDWith μ X ν and its existential corollary mixedIID_of_conditionallyIID are pinned (both with process measurability, so projecting Measure.map identities isn't needlessly delicate), and Layer 1 gains the conditional common ending conditionallyIID_of_jointRectangles — the joint-rectangle criterion (measurable sets in the ν coordinate times block rectangles, upgraded by the same π-system argument) that each route calls to reach the summit — beside the mixture ending mixedIID_of_mixingRepresentative.

4. iidMixture_ae_unique was a false target as renamed. By the independent-copy construction, no witness-level a.e.-equality theorem may conclude ν = ν' from the mixture relation alone; what is unique there is the mixing law μ.map ν (mixedIID_mixingLaw_unique, which does quantify over mixture witnesses). Witness-level a.e. uniqueness is the conditional-side milestone conditionallyIID_ae_unique, quantifying over witnesses of ConditionallyIIDWith.

One sequencing note, now recorded in the README: TauCeti's landed API uses the name ConditionallyIID for the mixture shape, so the code rename this PR enables (to MixedIID / MixedIIDWith) must land before the conditional predicate is implemented under that name. (Also worth coordinating with the still-open as-landed sync in #69, which documents the landed names and touches the same README regions.)

lake build green on the new head. The new definitions have real bodies; the newly added bridge and common-ending proof targets are intentionally stated with sorry (alongside the file's pre-existing sorry targets).

Directed by Cameron Freer, written by Fable 5 high, reviewed by GPT 5.6 Sol xhigh.

[cameronfreer]

@kim-em the PR description/title are now stale, if we accept my proposed fix/extension. Should I change that myself?

---

🤖 suggested changes by GPT 5.6:

The description is stale. It still says IsIIDMixture / IsIIDMixtureWith and describes genuine conditional i.i.d. as something not formalized.

Update it to reflect:

• MixedIIDWith / MixedIID
• genuine ConditionallyIIDWith / ConditionallyIID
• conditional i.i.d. retained as the summit
• joint-rectangle common ending and fixed-witness bridge
• witness uniqueness versus mixing-law uniqueness

I’d also retitle it to something like:

refactor(Exchangeability): separate mixed IID from conditional IID