Empirical/CSD: Stern-Gerlach Born values as derived Kähler-volume frequencies

Category: 3-Local (CSD-ontic layer; genuine volume derivation, not a transport tag).

This file is the carving-free, Gleason-free CSD-ontic reading of the single-qubit Stern-Gerlach Born values. It sits strictly above the other two Stern-Gerlach statements in the corpus:

1. Empirical/CSD/SternGerlach.lean (csd_sg_*): a transport tag — the Born numbers 1, 0, 1/2 are restated from the QM side; the CSD content is a prose realisability claim on the bundle. The numbers are not derived.
2. LF4/SingleQubitKahler.lean (sg_frequency_convergence): a genuine LF3-chain frequency-convergence capstone, but its outcome region is a fibreArc carved by construction to volume sgBorn s a (Tier-2). The number is realised, not derived from independent geometry.
3. this file: the outcome region is the genuine moment-map sublevel set on the ontic Σ = ℂℙ¹, whose Fubini–Study volume is computed (via the N = 2 Duistermaat–Heckman fact fs_moment_pushforward_uniform, now a theorem) to equal the Born weight ‖⟨e₀, ψ⟩‖². So volume = Born is derived, not posited by carving, and the chain cites only the foundational triple (no busch_effect_gleason, no invariant_measure_uniqueness).

What is and is not claimed

Derived (Lean-checked, carving-free, Gleason-free). For i.i.d. trials drawing microstates from the Fubini–Study typicality measure on Σ = ℂℙ¹, the empirical frequency of the moment-sublevel outcome region cut by [ψ] converges almost surely to ‖⟨e₀, ψ⟩‖². Instantiating:

• ψ = |+z⟩ = e₀ ⟹ frequency → 1 (csd_sg_volume_certain);
• ψ balanced (⟨e₀,ψ⟩ = 1/√2) ⟹ frequency → 1/2 (csd_sg_volume_half).

These are exactly the Stern-Gerlach predictions P(+z | +z) = 1 and the canonical 50/50 split (|⟨+z|+x⟩|² = 1/2).

Not claimed (the interpretive §14 boundary). Identifying the moment-sublevel region with the physical "the +z (resp. +x) detector fired" measurement outcome is the interpretive §14 labelling — a permanent interpretive boundary (⚠️ RESIDUE(R-007)): the formal operator → Σ-volume dictionary is proved (LF4/ObservableCorrespondenceN.lean), and only the detector-labelling of the region stays outside the theorem layer. This file derives the Born numbers as Kähler volumes. The carved capstone (2) carries the same boundary.

Experimental verification

• Stern, Gerlach 1922: Z. Phys. 9, 349.
• Phipps, Taylor 1927: Phys. Rev. 29, 309.

The Born value as a first-coordinate amplitude

theorem CSD.Empirical.CSDBridge.SternGerlachVolume.normSq_inner_single_zero (ψ : EuclideanSpace ℂ (Fin 2)) : ‖inner ℂ (EuclideanSpace.single 0 1) ψ‖ ^ 2 = ‖ψ.ofLp 0‖ ^ 2

For the fixed measurement outcome e₀, the Born amplitude squared is just the zeroth-coordinate squared norm: ‖⟨e₀, ψ⟩‖² = ‖ψ₀‖². This is the value the moment-volume frequency capstone lands on.

A balanced single-qubit state (the 1/2 witness)

noncomputable def CSD.Empirical.CSDBridge.SternGerlachVolume.balVec : EuclideanSpace ℂ (Fin 2)

The balanced unit vector (1/√2)|0⟩ + (1/√2)|1⟩, with ⟨e₀, balVec⟩ = 1/√2. Realises the canonical Stern-Gerlach 50/50 split.

Equations

• CSD.Empirical.CSDBridge.SternGerlachVolume.balVec = EuclideanSpace.single 0 ↑(√2)⁻¹ + EuclideanSpace.single 1 ↑(√2)⁻¹

theorem CSD.Empirical.CSDBridge.SternGerlachVolume.balVec_ofLp_zero : balVec.ofLp 0 = ↑(√2)⁻¹

theorem CSD.Empirical.CSDBridge.SternGerlachVolume.balVec_ofLp_one : balVec.ofLp 1 = ↑(√2)⁻¹

theorem CSD.Empirical.CSDBridge.SternGerlachVolume.balVec_norm : ‖balVec‖ = 1

theorem CSD.Empirical.CSDBridge.SternGerlachVolume.balVec_ne_zero : balVec ≠ 0

The Stern-Gerlach Born values as derived volume frequencies

theorem CSD.Empirical.CSDBridge.SternGerlachVolume.csd_sg_volume_certain (p₀ : LF4.CPN 2) {Ω : Type u_1} [MeasurableSpace Ω] {Pr : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure Pr] (X : ℕ → Ω → LF4.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 : LF4.CPN 2 | LF4.momentMap p 0 ≤ LF4.momentMap (Projectivization.mk ℂ LF4.zPlusVec LF4.zPlusVec_ne_zero) 0}).indicator fun (x : Ω) => 1)) : ∀ᵐ (ω : Ω) ∂Pr, Filter.Tendsto (fun (M : ℕ) => (∑ i ∈ Finset.range M, (X i ⁻¹' {p : LF4.CPN 2 | LF4.momentMap p 0 ≤ LF4.momentMap (Projectivization.mk ℂ LF4.zPlusVec LF4.zPlusVec_ne_zero) 0}).indicator (fun (x : Ω) => 1) ω) / ↑M) Filter.atTop (nhds 1)

CSD Stern-Gerlach certainty as a derived Kähler-volume frequency. For i.i.d. trials drawing microstates from the Fubini–Study typicality measure on Σ = ℂℙ¹, the empirical frequency of the moment-sublevel outcome region cut by the |+z⟩ ray converges almost surely to 1 — the P(+z | +z) = 1 Born value.

The limit is ‖⟨e₀, e₀⟩‖² = 1, with volume = Born derived from the moment map (no carving), foundational triple only (no busch_effect_gleason). The identification of the region with the physical +z outcome is LF4-todo §14.

theorem CSD.Empirical.CSDBridge.SternGerlachVolume.csd_sg_volume_half (p₀ : LF4.CPN 2) {Ω : Type u_1} [MeasurableSpace Ω] {Pr : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure Pr] (X : ℕ → Ω → LF4.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 : LF4.CPN 2 | LF4.momentMap p 0 ≤ LF4.momentMap (Projectivization.mk ℂ balVec balVec_ne_zero) 0}).indicator fun (x : Ω) => 1)) : ∀ᵐ (ω : Ω) ∂Pr, Filter.Tendsto (fun (M : ℕ) => (∑ i ∈ Finset.range M, (X i ⁻¹' {p : LF4.CPN 2 | LF4.momentMap p 0 ≤ LF4.momentMap (Projectivization.mk ℂ balVec balVec_ne_zero) 0}).indicator (fun (x : Ω) => 1) ω) / ↑M) Filter.atTop (nhds (1 / 2))

CSD Stern-Gerlach 50/50 split as a derived Kähler-volume frequency. For i.i.d. trials drawing microstates from the Fubini–Study typicality measure on Σ = ℂℙ¹, the empirical frequency of the moment-sublevel outcome region cut by the balanced ray [balVec] converges almost surely to 1/2 — the canonical Stern-Gerlach split |⟨+z | +x⟩|² = 1/2.

The limit is ‖⟨e₀, balVec⟩‖² = ‖1/√2‖² = 1/2, with volume = Born derived from the moment map (no carving), foundational triple only (no busch_effect_gleason). The identification of the region with the physical +x outcome is LF4-todo §14.