feat: relatively independent joinings over a common factor (#107)

[cameronfreer]

Generic transfer infrastructure for the R4 rankwise recursion, pitched one level above the uniform construction it was drafted as. Signature-free throughout; #107 remains open.

Branched from master, independent of #158.

Graphon/ForMathlib/RelativeFactorCoupling.lean — upstream candidate

Mathlib-only imports, nothing about relational structures.

• map_condDistrib_id — fibre concentration: pushing condDistrib id q μ forward through q is the deterministic identity kernel, a.e. for the law of the factor. This is the whole content of "conditioning on q pins down q", and everything else rests on it. It plausibly belongs beside condDistrib_comp and condDistrib_self.
• relativeFactorCoupling μ ν q r = (condDistrib id q μ ×ₖ condDistrib id r ν) ∘ₘ μ.map q — the relatively independent joining of μ and ν over a common factor: both sides disintegrated over Z, fibres multiplied independently. The independent product μ.prod ν does not identify the factors, and an arbitrary coupling that did could still let each side see more of the other.
• the two marginals, μ and ν (the second under ν.map r = μ.map q);
• comp_fst_ae_eq_comp_snd_relativeFactorCoupling — the common-factor identity q ∘ Prod.fst =ᵐ r ∘ Prod.snd, proved from the two fibre-concentration statements, one on each side. Equality of the two factor marginals would not suffice: it says nothing about the joint law.
• condIndepFun_fst_snd_relativeFactorCoupling — the two coordinates are conditionally independent given the common factor.

Conditioning

The conditioning σ-algebra is MeasurableSpace.comap (q ∘ Prod.fst) inferInstance, generated by a variable on the coupling space itself, not by the Z-valued disintegration variable that ∘ₘ integrates out. Only the former is available to downstream consumers, who see the coupling and not its construction. Conditional independence of the second coordinate from any coarser measurable function of the first is then a corollary by composition, and the common-factor identity transfers the statement to r ∘ Prod.snd when that side is more convenient.

No σ-algebra equality σ(q ∘ fst) = σ(snd) is asserted or supplied. The coupling gives only the inclusion modulo the law: the second coordinate may carry strictly more than the shared factor, exactly as U carries more than 1_{U < p}. What the conditional independence excludes is that the surplus says anything about the first coordinate beyond what the factor already determines.

The structural identity behind the proof is map_factorProd_relativeFactorCoupling: the joint law of the factor and the two coordinates is (Kernel.id ×ₖ (κ ×ₖ η)) ∘ₘ μ.map q, i.e. reading the factor off the first coordinate reconstitutes the outer integration. The two conditional distributions are then identified with the two disintegration kernels, and Mathlib's condIndepFun_iff_map_prod_eq_prod_condDistrib_prod_condDistrib closes it.

Graphon/UniformFactorCoupling.lean

exists_relativeFactorCoupling_uniform01 — the uniform specialization, bundling a measurable coding map with all five properties of the resulting coupling. The only uniform-specific input is Measure.exists_measurable_map_eq_uniform01 (#140), which supplies f : ℝ → Z matching the two factor laws; everything after that is the generic joining. There is no separate uniformFactorCoupling definition — the wrapper specializes the generic construction directly, so there is one object and one API.

This runs in the direction Graphon.KernelRandomization does not: that module manufactures a variable with a prescribed law out of a uniform, whereas here a uniform is manufactured alongside an already-given variable. Being reusable at every rank, it is the narrow transfer step the recursion needs in place of porting an external de Finetti package.

Gates

• lake build — 0 errors.
• scripts/check_census_and_axioms.py — census and axiom audit OK; the ten new declarations use only propext, Classical.choice, Quot.sound.
• Audit list updated in both scripts/axiom_audit.lean and the AUDITED_DECLS literal: 229 → 239, measured directly on base and head (base is master after feat: rank-one mutual conditional independence (#107) #158).
• Zero sorry/admit.