LF4 verification: the general-N joint-Dirichlet law recovers the qubit at N=2

Category: 3-Local (the general-N joint-Dirichlet law recovers the qubit at N=2).

A machine-checked consistency cross-check. The general-N headline fs_moment_joint_dirichlet_N and the qubit fs_moment_pushforward_uniform were proved by independent routes (the qubit via the Fin 4 Gaussian marginal; the general-N via the Gaussian→Dirichlet curry chain). This file derives the qubit statement from the general-N one at M = 1, converting "they agree by hand" into a kernel-checked reduction. If the general-N statement were a faithful generalisation only by accident, this would fail to compile.

The reduction handles the two shape differences the referee flagged:

• ratioN (momentMap p) is the normalised free coordinate on Fin 1 → ℝ; at N = 2 it equals the raw momentMap p 0 because the moments sum to one (momentMap_sum_eq_one), composed with the (Fin 1 → ℝ) ≃ᵐ ℝ evaluation iso (MeasurableEquiv.funUnique, measure-preserving);
• openSimplexFree on Fin 1 → ℝ is the funUnique-preimage of Ioo 0 1, which differs from the qubit's Icc 0 1 by the volume-null endpoint set (Ioo_ae_eq_Icc).

theorem CSD.LF4.fs_moment_pushforward_uniform_of_joint_dirichlet (p₀ : CPN 2) : MeasureTheory.Measure.map (fun (p : CPN 2) => momentMap p 0) (Matrix.UnitaryGroup.fubiniStudyMeasure p₀) = MeasureTheory.volume.restrict (Set.Icc 0 1)

N=2 consistency: the qubit moment pushforward is the M = 1 case of the joint Dirichlet law. Re-derives fs_moment_pushforward_uniform from fs_moment_joint_dirichlet_N (M := 1). Foundational-triple-only (inherits the general-N theorem's axiom posture).