feat: rank-one mutual conditional independence (#107)

[cameronfreer]

Statement A of the rank-one checkpoint, proved entirely from the merged two-set theorem. No de Finetti representation, no mixing measure, no identification of a mixing measure with an invariant conditional distribution, and nothing ported from the exchangeability package.

theorem iCondIndepFun_exactMap_singleton [Fintype S.Srt] [Countable S.Rel] :
    iCondIndepFun RelStructure.invariantAlgebra RelStructure.invariantAlgebra_le
      (fun v : Σ s : S.Srt, Vinfinite S s => B.exactMap {v})
      (M.law : Measure (RelStructure S (Vinfinite S)))

This is the conditional-independence half of the multi-sorted de Finetti statement; sort-orbit equality of the conditional kernels is the other half and is deliberately absent here. Mutual, not pairwise, and stated over the whole vertex index — iCondIndepFun already quantifies over finite subfamilies, so finite families are a corollary. Arbitrary exchangeable law: no IsDissociated, no NoNullary. Mathlib's iCondIndepFun takes dependent codomains, so v ↦ exactMap {v} with its varying ExactSpace {v} is a valid target as it stands.

The peel

Via iCondIndepFun_iff_condExp_inter_preimage_eq_mul, then Finset.induction_on:

• peel a vertex v;
• the accumulated events bundle into one fixingAlgebra s-event, since each is fixingAlgebra {i}-measurable and fixingAlgebra is monotone;
• {v} ∩ s = ∅ because v ∉ s, so condIndep_fixingAlgebra {v} s conditions on fixingAlgebra ∅ = invariantAlgebra — the same algebra at every stage;
• multiply by the induction hypothesis.

Why this does not generalize

The third step is what fails above rank one: for supports of rank n > 1 the peeled support need not be disjoint from the accumulated union, and where it is not, that stage conditions on a larger algebra — and conditional independence is not preserved under enlarging the conditioning. A positive-rank intersection is not inevitable for every family, but it is possible, which is enough to break the induction. That is the collider/intersection obstruction recorded on #107 — avoided here, not solved. The module docstring says so explicitly, so the argument is not mistaken for a route to the general case.

Also adds measurable_exactMap_fixingAlgebra — exactMap A is measurable for fixingAlgebra A, not merely for the ambient algebra — which is what lets the accumulated events be bundled. It lives in Graphon/RelFactorLaws.lean beside exactMap, as general factor API: rankwise work should not import the rank-one theorem to obtain it.

Deliberately not in this PR: kernel equality within each sort orbit (provable separately from exchangeability and conditional-distribution uniqueness), and everything about I(1), the uniform-factor coupling, and transfer.

Gates: lake build clean (3363 jobs), zero sorries, axiom audit 227 → 229 (two commits on the branch), documentation drift checks pass.

#107 remains open.