proof(S4): Session 5 — Robertson uncertainty (Rung 4, real PreHilbert)

§11  Self-adjoint operators + Robertson bound on PreHilbertR:

  SelfAdj H A         := forall x y, ip x (A y) = ip (A x) y
  phr_expect          := ip psi (A psi)
  phr_variance        := ip psi (A(A psi)) - ip(psi, A psi)^2
  phr_centered H A    := A psi - E_A * psi
  phr_unit            := norm2 psi = 1

  self_adj_swap         Qed — ip(A x) y = ip x (A y)
  self_adj_diag_sym     Qed — ip(A x) x = ip x (A x)
  self_adj_ip_Apsi_psi  Qed — ip(A psi) psi = E_psi(A)
  phr_centered_norm2    Qed — norm2(centered A psi) = Var(A) for unit psi + SA A
  robertson_real        Qed — Cov(A,B)^2 <= Var(A) * Var(B)  (Robertson)

Robertson via phr_cauchy_schwarz on the centered vectors.
Note: real-ip Robertson degenerates (Cov real ⟹ no commutator lower bound).
Complex-scalars Rung 5 is a future session.

File: 1456 LOC, 57 Qed, 0 Admitted, 0 banned constructs.

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

Author: hyperpolymath

proofs/canonical-proof-suite/S4_heisenberg_ndim.v

@@ -1376,8 +1376,7 @@ Lemma self_adj_ip_Apsi_psi :
 Proof.
   intros H A psi Hadj.
   unfold phr_expect.
-  rewrite (phr_ip_sym H (A psi) psi).
-  apply Hadj.
+  apply phr_ip_sym.
 Qed.
 
 (** Expand ip(u_A, u_A) for self-adjoint A and unit psi. *)
@@ -1388,26 +1387,35 @@ Lemma phr_centered_norm2 :
     phr_norm2 H (phr_centered H A psi) = phr_variance H A psi.
 Proof.
   intros H A psi Hadj Hunit.
-  unfold phr_centered, phr_variance, phr_expect, phr_norm2.
-  set (E := phr_ip H psi (A psi)).
-  set (u := phr_add H (A psi) (phr_neg H (phr_scal H E psi))).
-  (* Expand ip(u, u) = ip(Apsi, Apsi) - 2*E*ip(psi, Apsi) + E^2*ip(psi,psi). *)
-  unfold u.
-  rewrite phr_ip_linear_l.
-  rewrite phr_ip_linear_r, phr_ip_linear_r.
-  rewrite phr_ip_neg_r, phr_ip_neg_r.
-  rewrite phr_ip_scal_r, phr_ip_scal_r.
-  (* phr_unit psi: phr_ip H psi psi = 1. *)
+  unfold phr_centered, phr_variance, phr_norm2.
   unfold phr_unit, phr_norm2 in Hunit.
-  (* ip(Apsi, Apsi) = ip(psi, A(Apsi)) by self-adjointness. *)
-  rewrite (Hadj (A psi) psi).
-  (* ip(Apsi, psi) = ip(psi, Apsi) by symmetry and self-adj. *)
-  rewrite (phr_ip_sym H (A psi) psi).
-  rewrite (Hadj psi psi).
-  fold E.
-  (* Now we have:
-     ip(psi, A(Apsi)) - E * ip(psi, Apsi) - (E * ip(psi, Apsi) - E * E * ip(psi,psi)) *)
-  lra.
+  set (E := phr_ip H psi (A psi)).
+  (* Establish key scalar equalities. *)
+  assert (HAA : phr_ip H (A psi) (A psi) = phr_ip H psi (A (A psi))).
+  { symmetry. apply Hadj. }
+  assert (HAp : phr_ip H (A psi) psi = E).
+  { unfold E. symmetry. apply Hadj. }
+  assert (Hpp : phr_ip H psi psi = 1).
+  { exact Hunit. }
+  (* Now bilinearly expand ip(Apsi - E*psi, Apsi - E*psi). *)
+  assert (Hbil :
+    phr_ip H
+      (phr_add H (A psi) (phr_neg H (phr_scal H E psi)))
+      (phr_add H (A psi) (phr_neg H (phr_scal H E psi)))
+    = phr_ip H (A psi) (A psi)
+      - E * phr_ip H (A psi) psi
+      - E * phr_ip H psi (A psi)
+      + E * E * phr_ip H psi psi).
+  { rewrite phr_ip_linear_l.
+    rewrite phr_ip_linear_r; rewrite phr_ip_linear_r.
+    rewrite phr_ip_neg_r; rewrite phr_ip_neg_r.
+    rewrite phr_ip_scal_r; rewrite phr_ip_scal_r.
+    rewrite phr_ip_neg_l; rewrite phr_ip_neg_l.
+    rewrite phr_ip_scal_l; rewrite phr_ip_scal_l.
+    ring. }
+  rewrite Hbil.
+  rewrite HAA, HAp, Hpp.
+  unfold E. ring.
 Qed.
 
 (* ── §11d  Robertson uncertainty bound ───────────────────────────────── *)