LF4 §14.2 Robertson saturation: Pauli σ_x, σ_y on |0⟩ (N=2) #
Category: 3-Local (LF4 §14.2 concrete instance — first witness of the Kähler Robertson bound, demonstrating saturation on the canonical two-non-commuting-Paulis-and-a-spin-z-eigenstate example).
The classical textbook case. For Pauli observables σ_x, σ_y acting
on the spin-up state |0⟩ = (1, 0):
⟨0|σ_x|0⟩ = 0,⟨0|σ_y|0⟩ = 0(off-diagonal expectations vanish on diagonal state).Var(σ_x) = ‖σ_x |0⟩‖² − 0 = 1,Var(σ_y) = 1(each Pauli is unitary and squares to I).[σ_x, σ_y] = 2i·σ_z, and⟨0|σ_z|0⟩ = +1, so⟨0,[σ_x,σ_y]0⟩ = 2i.- Robertson:
1 · 1 ≥ ¼ · |2i|² = ¼ · 4 = 1. Saturated.
Via UncertaintyKahler.kahler_robertson_ontic_variance, the Robertson
bound is realised at the ontic level:
(∫ σ, spectralOnticCentered σ_x σ ∂μψ) · (∫ σ, spectralOnticCentered σ_y σ ∂μψ) ≥ ¼ · ‖⟨0, [σ_x, σ_y] 0⟩‖².
This module computes both sides explicitly and proves the LHS = RHS = 1
saturation theorem pauli_xy_robertson_saturation.
Module contents #
- Definitions:
pauliX,pauliYas rawMatrix (Fin 2) (Fin 2) ℂ. - Hermiticity:
pauliX_isHermitian,pauliY_isHermitian. - Action on |0⟩, |1⟩:
pauliX_apply_zPlusVec,pauliX_apply_zMinusVec,pauliY_apply_zPlusVec,pauliY_apply_zMinusVec. - Expectations:
pauliX_zPlus_re_expectation = 0, same for Y. - Norm-squareds:
pauliX_zPlus_norm_sq = 1, same for Y. - Variances:
pauliX_zPlus_spectralVariance = 1, same for Y. - Ontic integrals:
pauliX_zPlus_ontic_integral = 1, same for Y. - Commutator inner:
commutator_inner_zPlus = 2 * Complex.I. - Commutator norm-sq:
commutator_inner_zPlus_norm_sq = 4. - HEADLINE
pauli_xy_robertson_saturation:(LHS) = (1/4) * (RHS) = 1.
Axiom posture #
Foundational triple only.
Pauli matrices and the spin-down state #
Hermiticity #
Entry-level facts #
Pauli action on |0⟩ and |1⟩ #
Expectations on |0⟩ #
Norm-squareds on |0⟩ #
Spectral variances = 1 #
Ontic integrals = 1 #
Commutator inner product = 2i, norm² = 4 #
[σ_x, σ_y]·|0⟩ = (σ_x σ_y − σ_y σ_x)·|0⟩. Compute by stepping through
each composition: σ_x σ_y · |0⟩ = σ_x · (i·|1⟩) = i·|0⟩, and σ_y σ_x · |0⟩ = σ_y · |1⟩ = -i·|0⟩. Subtraction gives 2i·|0⟩.
Headline: saturation #
Robertson saturation for Pauli σ_x, σ_y on the spin-up state |0⟩.
On the Kähler instance KSigma 2 with preparation (Dirac p₀) × vol_T²,
the ontic-side product of integrated centered indicator-sums for σ_x
and σ_y on the spin-up state |0⟩ equals exactly the Robertson lower
bound ¼ · |⟨0, [σ_x, σ_y] · 0⟩|², both equal to 1. The state |0⟩
saturates Robertson — it is a minimum-uncertainty state for the pair
(σ_x, σ_y). Combines with kahler_robertson_ontic_variance (which
gives ≥) to give equality.