Empirical/CSD: Bell singlet joint probabilities as derived Kähler-volume frequencies

Category: 3-Local (CSD-ontic layer; genuine volume derivation, not a transport tag, and not conditional on the undischarged PureSingletPreparation bundle).

The two-qubit (N = 4) surfacing of the general-N Born-from-Kähler-volume capstone LF4.born_frequency_convergence_N_uncond (the hpos-free form, since the 2026-06-11 migration) for the Bell singlet. Where Empirical/CSD/Bell.lean's bell_singlet_frequency_convergence* are conditional on the undischarged PureSingletPreparation bundle (LF4-todo §2/§3/§7) and where LF4/SingletObservables.lean works with sector regions carved to volume P_st (Tier-2), this file lands the singlet's four joint-outcome probabilities as genuine Fubini–Study volumes on the ontic Σ = ℂℙ³, derived via the Duistermaat–Heckman theorem, carving-free and Gleason-free, and unconditional.

Construction

For detectors at relative angle θ (so a · b = cos θ), the singlet's four joint spin amplitudes in the product measurement eigenbasis {u_z^s ⊗ u_θ^t} are, in closed form,

⟨u_z^+ ⊗ u_θ^+, singlet⟩ = sin(θ/2)/√2     ⟨u_z^+ ⊗ u_θ^-, singlet⟩ =  cos(θ/2)/√2
⟨u_z^- ⊗ u_θ^+, singlet⟩ = -cos(θ/2)/√2    ⟨u_z^- ⊗ u_θ^-, singlet⟩ =  sin(θ/2)/√2

bellSingletVec θ is the vector of these amplitudes on Fin 4 ↔ (s,t). Its four computational-basis Born weights are the singlet joint probabilities

P_{++} = P_{--} = sin²(θ/2)/2 = (1 − cos θ)/4
P_{+-} = P_{-+} = cos²(θ/2)/2 = (1 + cos θ)/4,

and ∑ st·P_st = −cos θ recovers the singlet correlation ⟨σ_a σ_b⟩ = −a·b (bell_singlet_volume_correlation).

What is and is not claimed

Derived (Lean-checked, carving-free, Gleason-free, unconditional). The four Born weights are the genuine Fubini–Study volumes of the barycentric moment regions on ℂℙ³ (born_frequency_convergence_N_uncond via fs_born_volume_ratio_N_uncond), and i.i.d. Fubini–Study trials have outcome frequencies converging a.s. to them — at every relative angle θ, the aligned / anti-aligned boundary values θ = 0, π included (hpos-free since the 2026-06-11 migration onto LF4/BornRegionUncond.lean; the vanishing-amplitude outcomes' cells are FS-null). No busch_effect_gleason, no carving, no PureSingletPreparation bundle.

Not claimed. (i) The closed-form amplitudes above are the physics input (the known singlet inner products, defined directly — cf. LF3's cAmp); identifying bellSingletVec θ with the abstract singlet measured at relative angle θ is the LF4-todo §3 amplitude identity, here supplied by construction rather than derived from an abstract singlet object. (ii) The moment-region → physical-detector-outcome labelling is LF4-todo §14. The genuine, derived content is volume = Born number.

Experimental verification

• Bell 1964: Physics 1, 195; Aspect, Grangier, Roger 1982: Phys. Rev. Lett. 49, 91; loophole-free: Hensen 2015, Giustina 2015, Shalm 2015.

Reusable amplitude helpers

theorem CSD.Empirical.CSDBridge.BellVolume.normSq_inner_single (ψ : EuclideanSpace ℂ (Fin 4)) (i : Fin 4) : ‖inner ℂ (EuclideanSpace.single i 1) ψ‖ ^ 2 = ‖ψ.ofLp i‖ ^ 2

‖⟨eᵢ, ψ⟩‖² = ‖ψᵢ‖² on ℂℙ³ (the fixed-outcome Born amplitude is the i-th coordinate squared norm).

theorem CSD.Empirical.CSDBridge.BellVolume.normSq_ofReal_div_sqrt2 (r : ℝ) : ‖↑(r / √2)‖ ^ 2 = r ^ 2 / 2

‖↑(r/√2)‖² = r²/2.

The singlet amplitude vector on ℂℙ³

noncomputable def CSD.Empirical.CSDBridge.BellVolume.bellSingletVec (θ : ℝ) : EuclideanSpace ℂ (Fin 4)

The singlet's four joint amplitudes in the (z, θ) product measurement eigenbasis, as a vector on Fin 4 ↔ (s,t).

Equations

• One or more equations did not get rendered due to their size.

theorem CSD.Empirical.CSDBridge.BellVolume.bellSingletVec_ofLp_zero (θ : ℝ) : (bellSingletVec θ).ofLp 0 = ↑(Real.sin (θ / 2) / √2)

theorem CSD.Empirical.CSDBridge.BellVolume.bellSingletVec_ofLp_one (θ : ℝ) : (bellSingletVec θ).ofLp 1 = ↑(Real.cos (θ / 2) / √2)

theorem CSD.Empirical.CSDBridge.BellVolume.bellSingletVec_ofLp_two (θ : ℝ) : (bellSingletVec θ).ofLp 2 = ↑(-Real.cos (θ / 2) / √2)

theorem CSD.Empirical.CSDBridge.BellVolume.bellSingletVec_ofLp_three (θ : ℝ) : (bellSingletVec θ).ofLp 3 = ↑(Real.sin (θ / 2) / √2)

The four Born weights (component form)

theorem CSD.Empirical.CSDBridge.BellVolume.born_value_zero (θ : ℝ) : ‖inner ℂ (EuclideanSpace.single 0 1) (bellSingletVec θ)‖ ^ 2 = Real.sin (θ / 2) ^ 2 / 2

P_{++} Born weight: sin²(θ/2)/2.

theorem CSD.Empirical.CSDBridge.BellVolume.born_value_one (θ : ℝ) : ‖inner ℂ (EuclideanSpace.single 1 1) (bellSingletVec θ)‖ ^ 2 = Real.cos (θ / 2) ^ 2 / 2

P_{+-} Born weight: cos²(θ/2)/2.

theorem CSD.Empirical.CSDBridge.BellVolume.born_value_two (θ : ℝ) : ‖inner ℂ (EuclideanSpace.single 2 1) (bellSingletVec θ)‖ ^ 2 = Real.cos (θ / 2) ^ 2 / 2

P_{-+} Born weight: cos²(θ/2)/2.

theorem CSD.Empirical.CSDBridge.BellVolume.born_value_three (θ : ℝ) : ‖inner ℂ (EuclideanSpace.single 3 1) (bellSingletVec θ)‖ ^ 2 = Real.sin (θ / 2) ^ 2 / 2

P_{--} Born weight: sin²(θ/2)/2.

The P_st = (1 ∓ cos θ)/4 closed forms (recognisable singlet kernel)

theorem CSD.Empirical.CSDBridge.BellVolume.sin_half_sq (θ : ℝ) : Real.sin (θ / 2) ^ 2 = (1 - Real.cos θ) / 2

theorem CSD.Empirical.CSDBridge.BellVolume.cos_half_sq (θ : ℝ) : Real.cos (θ / 2) ^ 2 = (1 + Real.cos θ) / 2

theorem CSD.Empirical.CSDBridge.BellVolume.born_value_pst_minus (θ : ℝ) : ‖inner ℂ (EuclideanSpace.single 0 1) (bellSingletVec θ)‖ ^ 2 = (1 - Real.cos θ) / 4

P_{++} = P_{--} = (1 − cos θ)/4.

theorem CSD.Empirical.CSDBridge.BellVolume.born_value_pst_plus (θ : ℝ) : ‖inner ℂ (EuclideanSpace.single 1 1) (bellSingletVec θ)‖ ^ 2 = (1 + Real.cos θ) / 4

P_{+-} = P_{-+} = (1 + cos θ)/4.

Norm, non-vanishing, genericity

theorem CSD.Empirical.CSDBridge.BellVolume.bellSingletVec_norm (θ : ℝ) : ‖bellSingletVec θ‖ = 1

theorem CSD.Empirical.CSDBridge.BellVolume.bellSingletVec_ne_zero (θ : ℝ) : bellSingletVec θ ≠ 0

theorem CSD.Empirical.CSDBridge.BellVolume.bellSingletVec_hpos (θ : ℝ) (hθ : 0 < θ ∧ θ < Real.pi) (j : Fin 4) : 0 < ‖inner ℂ (EuclideanSpace.single j 1) (bellSingletVec θ)‖ ^ 2

Genericity: for θ ∈ (0, π) all four Born weights are strictly positive (sin(θ/2), cos(θ/2) > 0), so the conditional born_frequency_convergence_N applies. No longer consumed by the capstone (it routes through the hpos-free born_frequency_convergence_N_uncond); retained as the interior-point fact.

The Bell singlet volume-frequency capstone

theorem CSD.Empirical.CSDBridge.BellVolume.bell_singlet_born_frequency_volume (θ : ℝ) (p₀ : LF4.CPN 4) {Ω : Type u_1} [MeasurableSpace Ω] {Pr : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure Pr] (X : ℕ → Ω → LF4.CPN 4) (hX : ∀ (n : ℕ), Measurable (X n)) (hlaw : ∀ (n : ℕ), MeasureTheory.Measure.map (X n) Pr = Matrix.UnitaryGroup.fubiniStudyMeasure p₀) (hindep : ∀ (i : Fin 4), Pairwise (Function.onFun (fun (f g : Ω → ℝ) => ProbabilityTheory.IndepFun f g Pr) fun (n : ℕ) => (X n ⁻¹' LF4.bornRegion (bellSingletVec θ) ⋯ i).indicator fun (x : Ω) => 1)) : ∀ᵐ (ω : Ω) ∂Pr, ∀ (i : Fin 4), Filter.Tendsto (fun (m : ℕ) => (∑ k ∈ Finset.range m, (X k ⁻¹' LF4.bornRegion (bellSingletVec θ) ⋯ i).indicator (fun (x : Ω) => 1) ω) / ↑m) Filter.atTop (nhds (‖inner ℂ (EuclideanSpace.single i 1) (bellSingletVec θ)‖ ^ 2))

CSD Bell singlet joint frequencies as derived Kähler-volume convergence. For detectors at any relative angle θ and i.i.d. trials drawing microstates from the Fubini–Study typicality measure on the ontic Σ = ℂℙ³, the empirical frequencies of the four barycentric Born outcome regions converge, on a single almost-sure event, to the singlet joint Born weights ‖⟨eᵢ, bellSingletVec θ⟩‖² (equal to (1 ∓ cos θ)/4, see born_value_pst_minus/plus).

Carving-free, Gleason-free, unconditional — no busch_effect_gleason, no carved sector regions, no PureSingletPreparation bundle, and (since the 2026-06-11 hpos migration) no angle restriction: the aligned / anti-aligned boundary values θ = 0, π, where two of the four amplitudes vanish, are covered — their cells are FS-null and their frequencies converge to 0. The genuine upgrade over Empirical/CSD/Bell.lean's bundle-conditional capstones and over LF4/SingletObservables.lean's carved sector identities. The amplitude values are the physics input; the volume = Born number step is derived.

theorem CSD.Empirical.CSDBridge.BellVolume.bell_singlet_volume_correlation (θ : ℝ) : ‖inner ℂ (EuclideanSpace.single 0 1) (bellSingletVec θ)‖ ^ 2 - ‖inner ℂ (EuclideanSpace.single 1 1) (bellSingletVec θ)‖ ^ 2 - ‖inner ℂ (EuclideanSpace.single 2 1) (bellSingletVec θ)‖ ^ 2 + ‖inner ℂ (EuclideanSpace.single 3 1) (bellSingletVec θ)‖ ^ 2 = -Real.cos θ

Recovered singlet correlation. The signed sum of the four volume-derived Born weights is −cos θ = −a·b, the singlet two-point correlation ⟨σ_a ⊗ σ_b⟩. Ties the volume capstone to the Bell/CHSH content.