LF4 §14: observable correspondence for single-qubit Stern-Gerlach

Category: 3-Local (LF4 §14 discharge — projector-level observable correspondence on the single-qubit N = 2 Kähler instance).

Discharges LF4-todo §14 (observable correspondence) for projector observables on the single-qubit Kähler instance Σ = ℂℙ¹ × T², and lifts the Stern-Gerlach Born predictions from Empirical/CSD/SternGerlach.lean (bridge bundle) to a real LF3-chain frequency-convergence capstone (sg_frequency_convergence), parallel to ofKählerPreparation_singlet_frequency_convergence but at N = 2.

What §14 means for projector observables

For a single-qubit projector observable P = spinProj s a (the s-eigen projector of σ·a) and the |+_z⟩ preparation, the §14 claim is:

⟨zPlus, (toEuclideanLin P) zPlus⟩ = ∫ 1_{sgRegion s a} dμψ
                                 = (μψ (sgRegion s a)).toReal.

Both sides equal sgBorn s a := (1 + s · a_z) / 2. The Hilbert side is the (0,0) entry of P (since zPlus = e_0); the ontic side is the volume of the carved fibre arc.

Generality. This discharges §14 for projector observables on |+z⟩. The general self-adjoint case follows by spectral decomposition A = ∑ λᵢ Pᵢ (linearity of integration in μψ + Hilbert linearity in the Pᵢ); not formalised here.

What sg_frequency_convergence gives

For i.i.d. trials with the posited fibre law sgMuPsi, the empirical frequency of the (s, a) SG outcome converges a.s. to (1 + s · a_z)/2. For a = ẑ: frequencies → 1 (s = +) or 0 (s = −). For a = x̂: frequencies → 1/2 either way. The four SG Born identities (Empirical/QM/SternGerlach.lean's born_zPlus_zPlus etc.) are exactly the corresponding values of sgBorn.

Tier-2 honesty (unchanged from ofKählerPreparation)

sgRegion s a is carved to volume sgBorn s a by construction, so the §14 equation Hilbert = ontic holds because both sides equal sgBorn s a by separate routes (one via spinProj's (0,0) entry, one via the carving). This is the same eq-12-by-construction realisation as the singlet capstone: faithful concrete realisation on a compact Kähler Σ, not a derivation of Born from independent geometry.

Axiom posture

Foundational triple only. No Busch, no invariant_measure_uniqueness. The kBridge constructor for N = 2 is the same axiom-free marginal bridge as for N = 4.

Source

• Stern, Gerlach 1922 (the SG Born identities).
• The §14 observable correspondence framing is new with this corpus.

The single-qubit |+z⟩ state

noncomputable def CSD.LF4.zPlusVec : EuclideanSpace ℂ (Fin 2)

The |+z⟩ state vector in EuclideanSpace ℂ (Fin 2).

Equations

• CSD.LF4.zPlusVec = EuclideanSpace.single 0 1

theorem CSD.LF4.zPlusVec_ofLp_zero : zPlusVec.ofLp 0 = 1

theorem CSD.LF4.zPlusVec_ofLp_one : zPlusVec.ofLp 1 = 0

theorem CSD.LF4.zPlusVec_norm : ‖zPlusVec‖ = 1

theorem CSD.LF4.zPlusVec_ne_zero : zPlusVec ≠ 0

Stern-Gerlach Born value and bounds

noncomputable def CSD.LF4.sgBorn (s : LF3.Sign) (a : LF3.DetectorSetting) : ℝ

Stern-Gerlach Born value. For |+z⟩ preparation, measurement axis a, outcome s ∈ {+, −}: P(s | a, |+z⟩) = (1 + s · a_z) / 2.

Equations

• CSD.LF4.sgBorn s a = (1 + s.val * a.vec.ofLp 2) / 2

theorem CSD.LF4.sgBorn_nonneg (s : LF3.Sign) (a : LF3.DetectorSetting) : 0 ≤ sgBorn s a

theorem CSD.LF4.sgBorn_le_one (s : LF3.Sign) (a : LF3.DetectorSetting) : sgBorn s a ≤ 1

Single-qubit expectation identity (the Hilbert side of §14)

theorem CSD.LF4.zPlus_expectation (M : Matrix (Fin 2) (Fin 2) ℂ) : inner ℂ zPlusVec ((Matrix.toEuclideanLin M) zPlusVec) = M 0 0

Single-qubit expectation formula. The expectation of a 2×2 matrix M on |+z⟩ is just its (0,0) entry, since zPlus = e_0.

theorem CSD.LF4.zPlus_spinProj_expectation (s : LF3.Sign) (a : LF3.DetectorSetting) : inner ℂ zPlusVec ((Matrix.toEuclideanLin (LF3.spinProj s a)) zPlusVec) = ↑(sgBorn s a)

Single-qubit Born identity for the spin projector. For the |+z⟩ preparation, the expectation of spinProj s a equals (1 + s · a_z)/2.

Single-qubit Kähler outcome regions and fibre measure

noncomputable def CSD.LF4.zRay : CPN 2

The projective ray [|+z⟩] ∈ ℂℙ¹.

Equations

• CSD.LF4.zRay = Projectivization.mk ℂ CSD.LF4.zPlusVec CSD.LF4.zPlusVec_ne_zero

noncomputable def CSD.LF4.sgRegion (s : LF3.Sign) (a : LF3.DetectorSetting) : Set (KSigma 2)

The Stern-Gerlach outcome region for sign s and direction a: a fibre arc of measure sgBorn s a (carved by construction).

Equations

• CSD.LF4.sgRegion s a = Set.univ ×ˢ CSD.LF4.fibreArc (CSD.LF4.sgBorn s a) ×ˢ Set.univ

theorem CSD.LF4.sgRegion_measurable (s : LF3.Sign) (a : LF3.DetectorSetting) : MeasurableSet (sgRegion s a)

noncomputable def CSD.LF4.sgMuPsi : MeasureTheory.Measure (KSigma 2)

The single-qubit posited fibre law for |+z⟩: Dirac at the |+z⟩ ray, tensored with the torus volume. Pushes through π = pr₁ to a Dirac at zRay.

Equations

• CSD.LF4.sgMuPsi = (MeasureTheory.Measure.dirac CSD.LF4.zRay).prod MeasureTheory.volume

instance CSD.LF4.instProbSgMuPsi : MeasureTheory.IsProbabilityMeasure sgMuPsi

theorem CSD.LF4.sgMuPsi_push : MeasureTheory.Measure.map Prod.fst sgMuPsi = MeasureTheory.Measure.dirac zRay

theorem CSD.LF4.sgMuPsi_sgRegion (s : LF3.Sign) (a : LF3.DetectorSetting) : sgMuPsi (sgRegion s a) = ENNReal.ofReal (sgBorn s a)

The carving identity: μψ(sgRegion s a) = sgBorn s a.

§14 observable correspondence and SG frequency capstone

theorem CSD.LF4.sg_observable_correspondence (s : LF3.Sign) (a : LF3.DetectorSetting) : inner ℂ zPlusVec ((Matrix.toEuclideanLin (LF3.spinProj s a)) zPlusVec) = ↑(sgMuPsi (sgRegion s a)).toReal

§14 observable correspondence for the SG projectors. For the single-qubit spin projector spinProj s a and the |+z⟩ preparation, the Hilbert expectation equals the ontic measure of the outcome region (as a real number, coerced back to ℂ):

⟨zPlus, (toEuclideanLin (spinProj s a)) zPlus⟩
  = ((μψ (sgRegion s a)).toReal : ℂ).

Both sides equal (sgBorn s a : ℂ): the Hilbert side via the (0,0)-entry of spinProj s a (zPlus_spinProj_expectation), the ontic side via the carving identity (sgMuPsi_sgRegion).

theorem CSD.LF4.sg_frequency_convergence (s : LF3.Sign) (a : LF3.DetectorSetting) {Ω : Type u_1} [MeasurableSpace Ω] {Pr : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure Pr] {X : ℕ → Ω → KSigma 2} (hX : ∀ (n : ℕ), Measurable (X n)) (hlaw : ∀ (n : ℕ), MeasureTheory.Measure.map (X n) Pr = sgMuPsi) (hindep : Pairwise (Function.onFun (fun (f g : Ω → ℝ) => ProbabilityTheory.IndepFun f g Pr) fun (n : ℕ) => (X n ⁻¹' sgRegion s a).indicator fun (x : Ω) => 1)) : ∀ᵐ (ω : Ω) ∂Pr, Filter.Tendsto (fun (M : ℕ) => (∑ i ∈ Finset.range M, (X i ⁻¹' sgRegion s a).indicator (fun (x : Ω) => 1) ω) / ↑M) Filter.atTop (nhds (sgBorn s a))

CSD Stern-Gerlach frequency convergence (LF3-chain lift, §14 discharge applied). For i.i.d. trials drawing microstates from the posited fibre law sgMuPsi (the |+z⟩ preparation on the single-qubit Kähler instance Σ = ℂℙ¹ × T²), the empirical frequency of the SG outcome at sign s and direction a converges almost surely to the QM Born value (1 + s · a_z) / 2.

This is the non-vacuous LF3-chain Stern-Gerlach capstone, parallel to LF4.ofKählerPreparation_singlet_frequency_convergence but at the single-qubit level. Foundational triple only (no Busch, no invariant-measure-uniqueness).

§14.2 single-qubit Pauli observable

Beyond the §14.1 projector case. The Pauli observable σ·a has eigenvalues ±1 and the spectral decomposition σ·a = (+1)·spinProj(+a) + (−1)·spinProj(−a). Its ontic counterpart is the signed indicator 2·1_{R_+(a)} − 1, which equals +1 on the +-outcome region and −1 everywhere else (which is the −-outcome region by measurable partition). The integral against μψ matches the Hilbert expectation ⟨zPlus, σ·a · zPlus⟩ = a_z.

This is the first concrete §14.2 step beyond projectors, demonstrating the spectral-decomposition pattern at single-qubit level. Generalisation to arbitrary bounded self-adjoint via Mathlib's spectral theorem is mechanical on top.

noncomputable def CSD.LF4.pauliDotOntic (a : LF3.DetectorSetting) : KSigma 2 → ℝ

Ontic counterpart of pauliDot a on the |+z⟩ preparation: +1 on the +-outcome region sgRegion + a, −1 elsewhere (the −-outcome region by measurable partition). The signed-indicator decomposition 2·1_{R_+} − 1 is the simplest two-eigenvalue spectral-decomposition form.

Equations

• CSD.LF4.pauliDotOntic a σ = 2 * (CSD.LF4.sgRegion CSD.LF3.Sign.plus a).indicator (fun (x : CSD.LF4.KSigma 2) => 1) σ - 1

theorem CSD.LF4.pauliDotOntic_measurable (a : LF3.DetectorSetting) : Measurable (pauliDotOntic a)

theorem CSD.LF4.pauliDotOntic_integral (a : LF3.DetectorSetting) : ∫ (σ : KSigma 2), pauliDotOntic a σ ∂sgMuPsi = a.vec.ofLp 2

Integral of the Pauli ontic counterpart. ∫ pauliDotOntic a dμψ = a_z, matching ⟨zPlus, pauliDot a zPlus⟩ = a_z (the Hilbert expectation).

theorem CSD.LF4.pauliDot_observable_correspondence (a : LF3.DetectorSetting) : inner ℂ zPlusVec ((Matrix.toEuclideanLin (LF3.pauliDot a)) zPlusVec) = ↑(∫ (σ : KSigma 2), pauliDotOntic a σ ∂sgMuPsi)

§14.2 observable correspondence for pauliDot a (first non-projector case). The Hilbert expectation of σ·a on |+z⟩ equals the μψ-integral of its ontic counterpart. Both sides equal a_z: the Hilbert side via the (0,0) entry of pauliDot a (pauliDot_apply_00), the ontic side via the signed-indicator integration (pauliDotOntic_integral).