LF4: Busch-free empirical chain for the qubit Born weight (volume route)

Category: 3-Local (Busch-free empirical chain for the qubit Born weight (volume route)).

This integrates the moment-map / volume derivation of the Born weight into the LF1 empirical chain, giving a frequency-convergence capstone that routes through the Fubini–Study volume rather than through busch_effect_gleason.

The existing LF3 chain capstones land on the Born weight via the operational package and pure_state_born_weights_of_certainty, hence cite busch_effect_gleason. Here, for the qubit, the limiting frequency is identified with the Born weight ‖⟨e₀,ψ⟩‖² via fs_born_volume_ratio_qubit — the genuine Fubini–Study volume of the moment sublevel set on the ontic Kähler Σ = ℂℙ¹. So this capstone cites only the foundational triple plus the explicit h_uniform hypothesis (the N=2 Duistermaat–Heckman fact; the plan-B discharge target — see specs/carve-out-plan.md). No busch_effect_gleason.

This realises the CSD thesis end to end for the qubit: deterministic repeated-trial typicality (LF1) + "Born = Fubini–Study volume ratio" (the moment map) ⟹ empirical frequencies converge almost surely to the Born weight, with the Born value derived from the Kähler volume, not imported via Gleason/Busch.

Honest scope. Conditional on h_uniform (classically true, dischargeable; plan B). The outcome region is the moment sublevel set, special to N=2's 1-dimensional polytope.

theorem CSD.LF4.qubit_born_frequency_convergence (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)) {Ω : Type u_1} [MeasurableSpace Ω] {Pr : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure Pr] (X : ℕ → Ω → CPN 2) (hX : ∀ (n : ℕ), Measurable (X n)) (hlaw : ∀ (n : ℕ), MeasureTheory.Measure.map (X n) Pr = Matrix.UnitaryGroup.fubiniStudyMeasure p₀) (hindep : Pairwise (Function.onFun (fun (f g : Ω → ℝ) => ProbabilityTheory.IndepFun f g Pr) fun (n : ℕ) => (X n ⁻¹' {p : CPN 2 | momentMap p 0 ≤ momentMap (Projectivization.mk ℂ ψ hψ0) 0}).indicator fun (x : Ω) => 1)) : ∀ᵐ (ω : Ω) ∂Pr, Filter.Tendsto (fun (M : ℕ) => (∑ i ∈ Finset.range M, (X i ⁻¹' {p : CPN 2 | momentMap p 0 ≤ momentMap (Projectivization.mk ℂ ψ hψ0) 0}).indicator (fun (x : Ω) => 1) ω) / ↑M) Filter.atTop (nhds (‖inner ℂ (EuclideanSpace.single 0 1) ψ‖ ^ 2))

Busch-free qubit Born frequency convergence. For i.i.d. trials X drawn from the Fubini–Study measure on ℂℙ¹, the empirical frequency of the moment sublevel outcome {p | momentMap p 0 ≤ momentMap [ψ] 0} converges almost surely to the Born weight ‖⟨e₀, ψ⟩‖², provided the N=2 Duistermaat–Heckman hypothesis h_uniform. Cites only the foundational triple + h_uniform; no busch_effect_gleason.