LF4 general-N Slice E (headline): the joint Dirichlet moment pushforward

Category: 3-Local (the joint Dirichlet moment pushforward).

The general-N analogue of fs_moment_pushforward_uniform (which handled the qubit scalar marginal N = 2). The free-coordinate moment map ratioN ∘ momentMap pushes the genuine Fubini–Study measure on ℂℙ^M forward to M! times the uniform measure on the open simplex — the Dirichlet(1,…,1) law,

(ratioN ∘ momentMap)∗ μ_FS = M! · vol|_{openSimplexFree}.

This is the joint Duistermaat–Heckman fact for general N = M+1, the object the qubit marginal could not give (the single-coordinate marginal is Beta(1, N-1), not the Born weight, for N ≥ 3; only the joint simplex law feeds born_eq_volume_ratio).

The proof is the general-N assembly: gaussianCPN_eq_fubiniStudy (Slice B) realises μ_FS as a projectivised Gaussian; map_pi_eq_stdGaussian exposes the ℝ^{N×2} standard Gaussian as gaussianReal^{⊗(N×2)}; blockSqNormCurry_map_pi (Slice E bridge) lands on Exp(1/2)^{⊗N}; and ratioSqNorm_map_expHalf_pi (Slice D) is the Gamma→Dirichlet crux. The a.e.-off-{0} pointwise identity ratioN (momentMap [coordsN(toLp y)]) = ratioN (blockSqNorm (curry y)) glues the geometric and coordinate routes.

theorem CSD.LF4.pi_gaussianReal_prod_singleton_zero {M : ℕ} : (MeasureTheory.Measure.pi fun (x : Fin (M + 1) × Fin 2) => ProbabilityTheory.gaussianReal 0 1) {0} = 0

The standard Gaussian on ℝ^{(M+1)×2} has no atom at the origin.

theorem CSD.LF4.fs_moment_joint_dirichlet_N {M : ℕ} (p₀ : CPN (M + 1)) : MeasureTheory.Measure.map (fun (p : CPN (M + 1)) => ratioN fun (i : Fin (M + 1)) => momentMap p i) (Matrix.UnitaryGroup.fubiniStudyMeasure p₀) = ↑M.factorial • MeasureTheory.volume.restrict openSimplexFree

Slice E headline: the joint Dirichlet moment pushforward (general N). The free-coordinate moment map ratioN ∘ momentMap pushes the Fubini–Study measure on ℂℙ^M to M! times uniform measure on the open simplex (the Dirichlet(1,…,1) law). The qubit fs_moment_pushforward_uniform is the M = 1 shadow (its scalar marginal). Foundational-triple-only; no busch_effect_gleason.