LF4 Tranche M slice 2 (option C): Born = Fubini–Study volume ratio on Σ (qubit)

This completes the on-Σ statement of "Born = volume ratio" for the qubit (N = 2), modulo the single explicit analytic hypothesis identified in slice 2: the 0-coordinate of the moment map pushes the genuine Fubini–Study measure to the uniform measure on [0,1].

fs_born_volume_ratio_qubit :
  (Φ₀∗ fubiniStudyMeasure = uniform[0,1]) →
    fubiniStudyMeasure {p | momentMap p 0 ≤ momentMap [ψ] 0} = ‖⟨e₀, ψ⟩‖².

The outcome region is the sublevel set {p | momentMap p 0 ≤ momentMap [ψ] 0} — the rays whose outcome-0 moment value is at most the preparation's. For N = 2 the moment polytope is the segment [0,1], so this sublevel set is the pullback of [0, b₀(ψ)] and its FS measure is its length b₀(ψ) = ‖⟨e₀,ψ⟩‖². The region is geometric (a moment sublevel set), the measure is the genuine fubiniStudyMeasure on the ontic Kähler Σ = ℂℙ¹, and the equality to the Born weight is a theorem — no carving, no busch_effect_gleason.

Honest scope. The hypothesis h_uniform is the N = 2 Duistermaat–Heckman / Dirichlet fact ("|U₀₀|² is Uniform[0,1] for Haar U(2)"), the discharge target of plan B (specs/carve-out-plan.md Tranche M slice 2). Stated as an explicit hypothesis, the theorem stays axiom-clean (the project's load-bearing-hypothesis pattern) and names the precise remaining gap. The sublevel-set form is special to N = 2 (the 1-dimensional polytope); general N uses the barycentric regions of BornVolume.lean with the full Φ∗μ_FS = uniform_Δ pushforward.

Category: 1-Mathlib adjacent; kept in CSD.LF4 for the carve-out programme.

theorem CSD.LF4.momentMap_measurable {N : ℕ} (i : Fin N) : Measurable fun (p : CPN N) => momentMap p i

momentMap · i is measurable. momentMap is defined via the representative rep, but it is scale-invariant, so it descends from the measurable function v ↦ ‖vᵢ‖²/‖v‖² on the nonzero subtype. Routed through the §12 characterisation measurable_iff_measurable_comp_mk'.

theorem CSD.LF4.fs_born_volume_ratio_qubit (p₀ : CPN 2) (ψ : EuclideanSpace ℂ (Fin 2)) (hψ0 : ψ ≠ 0) (hψ : ‖ψ‖ = 1) (h_uniform : MeasureTheory.Measure.map (fun (p : CPN 2) => momentMap p 0) (Matrix.UnitaryGroup.fubiniStudyMeasure p₀) = MeasureTheory.volume.restrict (Set.Icc 0 1)) : (Matrix.UnitaryGroup.fubiniStudyMeasure p₀) {p : CPN 2 | momentMap p 0 ≤ momentMap (Projectivization.mk ℂ ψ hψ0) 0} = ENNReal.ofReal (‖inner ℂ (EuclideanSpace.single 0 1) ψ‖ ^ 2)

Headline (option C): the Born weight is a Fubini–Study volume ratio on ℂℙ¹. For a unit qubit preparation ψ, modulo the N = 2 Duistermaat–Heckman hypothesis (Φ₀∗ fubiniStudyMeasure = uniform[0,1]), the FS measure of the moment sublevel set at [ψ] equals the Born weight ‖⟨e₀, ψ⟩‖².