LF4 §14.2 parametric Robertson: σ·â, σ·b̂ on |0⟩ for arbitrary axes (N=2)

Category: 3-Local (LF4 §14.2 concrete instance — parametric extension of PauliRobertson.lean. Robertson bound for spin-½ Pauli observables σ·â, σ·b̂ along arbitrary unit-vector axes â, b̂, on the spin-up state |0⟩).

The parametric inequality

For unit vectors â, b̂ ∈ ℝ³ (the DetectorSetting constraint) and the spin-up state |0⟩:

• ⟨0 | σ·â | 0⟩ = a_z (third component), real.
• Var(σ·â) = ‖σ·â · 0‖² − a_z² = 1 − a_z² (Pauli unitarity).
• [σ·â, σ·b̂] = 2i · σ·(â × b̂) (standard Pauli algebra).
• ⟨0 | [σ·â, σ·b̂] | 0⟩ = 2i · (â × b̂)_z = 2i · (a_x b_y − a_y b_x).
• ¼ · ‖⟨0 | [σ·â, σ·b̂] | 0⟩‖² = (a_x b_y − a_y b_x)².

The Robertson bound becomes the geometric inequality:

(1 − a_z²)(1 − b_z²) ≥ (a_x b_y − a_y b_x)².

Both sides are explicit polynomials in the components of â and b̂. Equality holds when both axes lie in the xy-plane (a_z = b_z = 0) and are perpendicular (a_x b_y − a_y b_x = ±1), e.g., â = x̂, b̂ = ŷ — recovering PauliRobertson.pauli_xy_robertson_saturation.

Axiom posture

Foundational triple only.

Variance and ontic integral for σ·â on |0⟩

theorem CSD.LF4.pauliDot_zPlus_norm_sq (a : LF3.DetectorSetting) : ‖(Matrix.toEuclideanLin (LF3.pauliDot a)) zPlusVec‖ ^ 2 = 1

The ‖σ·â · |0⟩‖² = 1 (Pauli unitarity computed entry-wise on |0⟩).

theorem CSD.LF4.pauliDot_zPlus_spectralVariance (a : LF3.DetectorSetting) : spectralVariance ⋯ zPlusVec = 1 - a.vec.ofLp 2 ^ 2

Variance of σ·â on |0⟩ is 1 − a_z².

theorem CSD.LF4.pauliDot_zPlus_ontic_integral (a : LF3.DetectorSetting) (p₀ : CPN 2) : ∫ (σ : CPN 2 × KTorus), spectralOnticCentered ⋯ zPlusVec σ ∂(MeasureTheory.Measure.dirac p₀).prod MeasureTheory.volume = 1 - a.vec.ofLp 2 ^ 2

Ontic-side integrated centered observable for σ·â on |0⟩ is 1 − a_z².

Matrix ↔ Module.End commutator bridge

theorem CSD.LF4.toEuclideanLin_mul_apply (A B : Matrix (Fin 2) (Fin 2) ℂ) (v : EuclideanSpace ℂ (Fin 2)) : (Matrix.toEuclideanLin (A * B)) v = (Matrix.toEuclideanLin A) ((Matrix.toEuclideanLin B) v)

Commutator matrix entry (0,0)

theorem CSD.LF4.pauliDot_commutator_matrix_00 (a b : LF3.DetectorSetting) : (LF3.pauliDot a * LF3.pauliDot b - LF3.pauliDot b * LF3.pauliDot a) 0 0 = 2 * Complex.I * ↑(a.vec.ofLp 0 * b.vec.ofLp 1 - a.vec.ofLp 1 * b.vec.ofLp 0)

The (0,0) entry of the matrix commutator [σ·â, σ·b̂] is 2i · (a_x b_y − a_y b_x).

Commutator inner product on |0⟩

theorem CSD.LF4.pauliDot_commutator_inner_zPlus (a b : LF3.DetectorSetting) : inner ℂ zPlusVec ((Matrix.toEuclideanLin (LF3.pauliDot a) * Matrix.toEuclideanLin (LF3.pauliDot b) - Matrix.toEuclideanLin (LF3.pauliDot b) * Matrix.toEuclideanLin (LF3.pauliDot a)) zPlusVec) = 2 * Complex.I * ↑(a.vec.ofLp 0 * b.vec.ofLp 1 - a.vec.ofLp 1 * b.vec.ofLp 0)

Commutator inner squared norm

theorem CSD.LF4.pauliDot_commutator_inner_zPlus_norm_sq (a b : LF3.DetectorSetting) : ‖inner ℂ zPlusVec ((Matrix.toEuclideanLin (LF3.pauliDot a) * Matrix.toEuclideanLin (LF3.pauliDot b) - Matrix.toEuclideanLin (LF3.pauliDot b) * Matrix.toEuclideanLin (LF3.pauliDot a)) zPlusVec)‖ ^ 2 = 4 * (a.vec.ofLp 0 * b.vec.ofLp 1 - a.vec.ofLp 1 * b.vec.ofLp 0) ^ 2

Headline: parametric Robertson on |0⟩

theorem CSD.LF4.pauliDot_robertson_zPlus (a b : LF3.DetectorSetting) (p₀ : CPN 2) : (1 - a.vec.ofLp 2 ^ 2) * (1 - b.vec.ofLp 2 ^ 2) ≥ (a.vec.ofLp 0 * b.vec.ofLp 1 - a.vec.ofLp 1 * b.vec.ofLp 0) ^ 2

Parametric Robertson uncertainty for spin-½ on |0⟩. For any unit-vector measurement axes â, b̂, the product of ontic-side variances of σ·â, σ·b̂ on the spin-up state |0⟩ is bounded below by the squared z-component of the cross product â × b̂:

(1 − a_z²) · (1 − b_z²) ≥ (a_x b_y − a_y b_x)².

A geometric inequality: both sides are explicit polynomial functions of the axis components. Equality holds when both axes lie in the xy-plane and are perpendicular — recovering pauli_xy_robertson_saturation as the special case â = x̂, b̂ = ŷ.

Composes kahler_robertson_ontic_variance (the abstract LF4 ontic- variance Robertson bound) with pauliDot_zPlus_ontic_integral (twice) and pauliDot_commutator_inner_zPlus_norm_sq.