proof(S4): Session 6 — commutator algebra + Robertson commutator form (Rung 4b)

§12a–§12d: phr_commutator definition, phr_commutator_expect_zero (SelfAdj ⟹ ⟨ψ,[A,B]ψ⟩=0),
phr_commutator_anticomm, phr_variance_nonneg, robertson_commutator (¼·⟨ψ,[A,B]ψ⟩²≤Var·Var).

Rung 4 complete: both robertson_real (Rung 4a) and robertson_commutator (Rung 4b) Qed-closed.
90 Qed, 0 Admitted. Rung 5 (ComplexPreHilbert + anti-Hermitian commutator) deferred.

Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>

Author: hyperpolymath

proofs/canonical-proof-suite/S4_heisenberg_ndim.v

@@ -1454,3 +1454,144 @@ Proof.
   (* phr_cauchy_schwarz gives (ip u v)^2 <= norm2 u * norm2 v. *)
   lra.
 Qed.
+
+(* ====================================================================
+   §12  Rung 4b — Commutator algebra and Robertson commutator form.
+   Session 6 deliverables.
+
+   For SYMMETRIC (self-adjoint) operators A, B in a real pre-Hilbert
+   space, the commutator [A,B] = A∘B − B∘A has zero expectation in
+   any state ψ:
+
+       ⟨ψ, [A,B]ψ⟩  =  ⟨Aψ, Bψ⟩ − ⟨Aψ, Bψ⟩  =  0.
+
+   This follows from the symmetric adjoint swap:
+     · ⟨ψ, A(Bψ)⟩ = ⟨Aψ, Bψ⟩   (SelfAdj A, x=ψ, y=Bψ, reversed)
+     · ⟨ψ, B(Aψ)⟩ = ⟨B(Aψ),ψ⟩  (phr_ip_sym)
+                   = ⟨Aψ, Bψ⟩   (SelfAdj B, x=Aψ, y=ψ)
+
+   Consequence (robertson_commutator):
+       ¼ · ⟨ψ,[A,B]ψ⟩² ≤ Var_ψ(A) · Var_ψ(B).
+   In a REAL pre-Hilbert space this is trivially 0 ≤ Var·Var.
+   The structure mirrors the complex Robertson (Rung 5) where
+   the RHS need not vanish.
+   ==================================================================== *)
+
+(* ── §12a  Commutator ─────────────────────────────────────────────── *)
+
+(** [A,B] x = A(Bx) − B(Ax). *)
+Definition phr_commutator (H : PreHilbertR) (A B : PHREndo H) (x : H) : H :=
+  phr_add H (A (B x)) (phr_neg H (B (A x))).
+
+(* ── §12b  Expectation of commutator for symmetric operators ─────── *)
+
+(** For self-adjoint A and B, ⟨ψ, [A,B]ψ⟩ = 0. *)
+Lemma phr_commutator_expect_zero :
+  forall (H : PreHilbertR) (A B : PHREndo H) (psi : H),
+    SelfAdj H A ->
+    SelfAdj H B ->
+    phr_ip H psi (phr_commutator H A B psi) = 0.
+Proof.
+  intros H A B psi HA HB.
+  unfold phr_commutator.
+  rewrite phr_ip_linear_r, phr_ip_neg_r.
+  (* ⟨ψ, A(Bψ)⟩ = ⟨Aψ, Bψ⟩  via SelfAdj A (x=ψ, y=Bψ). *)
+  assert (Hstep1 : phr_ip H psi (A (B psi)) = phr_ip H (A psi) (B psi)).
+  { exact (HA psi (B psi)). }
+  (* ⟨ψ, B(Aψ)⟩ = ⟨B(Aψ),ψ⟩ = ⟨Aψ,Bψ⟩  via ip_sym then SelfAdj B (x=Aψ, y=ψ). *)
+  assert (Hstep2 : phr_ip H psi (B (A psi)) = phr_ip H (A psi) (B psi)).
+  { rewrite (phr_ip_sym H psi (B (A psi))).
+    exact (eq_sym (HB (A psi) psi)). }
+  rewrite Hstep1, Hstep2. ring.
+Qed.
+
+(** Anti-commutativity of commutator expectation (holds without symmetry). *)
+Lemma phr_commutator_anticomm :
+  forall (H : PreHilbertR) (A B : PHREndo H) (psi : H),
+    phr_ip H psi (phr_commutator H B A psi)
+      = - phr_ip H psi (phr_commutator H A B psi).
+Proof.
+  intros H A B psi.
+  unfold phr_commutator.
+  rewrite !phr_ip_linear_r, !phr_ip_neg_r.
+  ring.
+Qed.
+
+(* ── §12c  Variance non-negativity (unit + self-adjoint) ─────────── *)
+
+(** Var_ψ(A) ≥ 0 when A is self-adjoint and ψ is a unit vector.
+    Follows from Var_ψ(A) = ‖u_A‖² ≥ 0 (phr_centered_norm2). *)
+Lemma phr_variance_nonneg :
+  forall (H : PreHilbertR) (A : PHREndo H) (psi : H),
+    SelfAdj H A ->
+    phr_unit H psi ->
+    0 <= phr_variance H A psi.
+Proof.
+  intros H A psi HA Hunit.
+  rewrite <- (phr_centered_norm2 H A psi HA Hunit).
+  apply phr_norm2_nonneg.
+Qed.
+
+(* ── §12d  Robertson commutator form ─────────────────────────────── *)
+
+(** Robertson uncertainty, commutator form (real pre-Hilbert).
+
+    For self-adjoint A, B and unit ψ:
+        ¼ · ⟨ψ,[A,B]ψ⟩² ≤ Var_ψ(A) · Var_ψ(B).
+
+    In a real pre-Hilbert space the LHS is always 0
+    (phr_commutator_expect_zero), so the proof reduces to
+    0 ≤ Var(A)·Var(B), which follows from variance non-negativity.
+
+    The complex analogue (Rung 5) replaces the zero with the
+    imaginary part of ⟨ψ,[A,B]ψ⟩ over a ComplexPreHilbert record. *)
+Theorem robertson_commutator :
+  forall (H : PreHilbertR) (A B : PHREndo H) (psi : H),
+    SelfAdj H A ->
+    SelfAdj H B ->
+    phr_unit H psi ->
+    (1/4) * (phr_ip H psi (phr_commutator H A B psi))^2
+      <= phr_variance H A psi * phr_variance H B psi.
+Proof.
+  intros H A B psi HA HB Hunit.
+  rewrite (phr_commutator_expect_zero H A B psi HA HB).
+  (* Goal: (1/4) * 0^2 <= Var(A) * Var(B). *)
+  assert (HvA : 0 <= phr_variance H A psi) by
+    (apply phr_variance_nonneg; assumption).
+  assert (HvB : 0 <= phr_variance H B psi) by
+    (apply phr_variance_nonneg; assumption).
+  assert (Hmul : 0 <= phr_variance H A psi * phr_variance H B psi)
+    by (apply Rmult_le_pos; assumption).
+  simpl. lra.
+Qed.
+
+(* ====================================================================
+   Session 6 status note
+   ====================================================================
+
+   STATUS: robertson_real (Rung 4a, covariance form) + robertson_commutator
+   (Rung 4b, commutator form) both Qed-closed.  Zero banned constructs.
+
+   WHAT IS PROVED (Rung 4 complete)
+
+   Rung 4a — Robertson covariance (Theorem robertson_real):
+       For self-adjoint A, B and unit ψ ∈ H (real pre-Hilbert):
+           Cov_ψ(A,B)² ≤ Var_ψ(A) · Var_ψ(B).
+       Direct from phr_cauchy_schwarz on the centered vectors.
+
+   Rung 4b — Robertson commutator (Theorem robertson_commutator):
+       For self-adjoint A, B and unit ψ ∈ H (real pre-Hilbert):
+           ¼ · ⟨ψ,[A,B]ψ⟩² ≤ Var_ψ(A) · Var_ψ(B).
+       The LHS is 0 in the real case; the inequality is non-trivial
+       in the complex case (Rung 5).
+
+   WHAT IS NOT PROVED
+
+   Rung 5 (deferred):
+     · ComplexPreHilbert record with Hermitian (self-adjoint for ℂ)
+       operators.
+     · Complex Robertson: ¼|⟨ψ,[A,B]ψ⟩|² ≤ Var_ψ(A)·Var_ψ(B) with
+       non-trivial LHS (commutator of position+momentum = iℏ·I).
+     · Requires sesquilinear ip and anti-Hermitian commutator structure.
+       Estimated ~800 LOC beyond this file.
+   ==================================================================== *)