feat: I(1), the rank-one transfer step (#107)

[cameronfreer]

The base of the rank recursion: the relative joining of #159 instantiated at q = lowerFactorMap 1, with relabeling compatibility and the transfer clause kept explicit. #107 remains open.

Rank one is invariant, not merely equivariant

lowerFactorMap_one_relabel is what makes this step easy, and it is worth stating why. LowerIndex 1 consists of the indices anchored at a set of cardinality < 1, i.e. at ∅, and a basis event anchored at ∅ is measurable for fixingAlgebra ∅ = invariantAlgebra. So it is literally fixed by every finitely supported sortwise relabeling — not fixed modulo the law. Hence

lowerFactorMap 1 ∘ RelStructure.relabel σ.1 = lowerFactorMap 1

as functions, and the equivariance square of Graphon.RelLowerFactor degenerates at rank one: no transport of the factor space, and the conditioning factor of the coupling does not move with σ.

That yields map_prodMap_relabel_rankOneCoupling — every finitely supported sortwise relabeling of the structure coordinate preserves the coupling, because it acts inside the fibres of the disintegration and so never disturbs the outer integration.

This is exactly what fails at higher rank. There the factor map is only equivariant, and the corresponding statement will have to move the factor space by lowerFactorSpaceEquiv on the other side. The module header records this rather than leaving the rank-one convenience looking general.

I(1)

exists_rankOneUniformCoupling bundles six clauses: f measurable; the coupling is a probability measure; structure marginal is M.law; latent marginal is uniform01; the latent resolves the factor, lowerFactorMap 1 X = f ξ a.s.; and the structure and latent are conditionally independent given that factor.

The last clause is the one that cannot be dropped, and the reason is the one you gave: the marginals and the resolution identity together still permit a latent that encodes arbitrary further information about whatever rank one leaves unresolved. It is stated in its strongest form — over the whole structure coordinate — so any particular unresolved reading follows by measurable composition. condIndepFun_comp_fst_snd_rankOne records that transfer explicitly rather than leaving it implicit in the strong clause.

No σ-algebra equality between latent and factor is claimed. The latent may carry strictly more than lowerFactorMap 1 reads; conditional independence is precisely the statement that the surplus is irrelevant to the structure.

Two additions to the generic API

Both are driven by I(1) rather than added speculatively, per the #160 rule:

• map_prodMap_relativeFactorCoupling — if T preserves μ and q ∘ T = q, then Prod.map T id preserves the joining. Proved through uniqueness of conditional distributions: condDistrib T q μ =ᵐ condDistrib id q μ because q ∘ T = q and T is measure preserving, so T leaves each fibre invariant.
• condIndepFun_comp_fst_snd_relativeFactorCoupling — the transfer clause in general form; one line from Mathlib's CondIndepFun.comp, but named because it is the property downstream consumers actually need to cite.

Both remain Provisional in #160 — one consumer each so far. The later rank transition is the second consumer that would harden them.

Gates

• lake build — 0 errors.
• scripts/check_census_and_axioms.py — census and axiom audit OK; the seven new declarations use only propext, Classical.choice, Quot.sound.
• Audit list updated in both scripts: 239 → 246, measured directly on base and head.
• Zero sorry/admit.