proof(S4): Session 4 — PreHilbertR record + abstract Cauchy-Schwarz (Rung 3)

§10  Abstract PreHilbertR record: real inner product over arbitrary carrier V,
     axioms: symmetry, bilinearity (add + scal in both args), pos-def,
     zero-iff definiteness, additive group structure.

§10b  Derived lemmas: phr_norm2_nonneg, phr_ip_zero_l/r, phr_ip_neg_l,
      phr_norm2_zero_implies_ip_zero.

§10c  phr_cs_aux: λ·x - ip(y,x)·y (the λ-quotient auxiliary vector)
      phr_cs_expand_norm: phr_norm2(aux) = λ·(λ·|x|²  - ip(x,y)²)  Qed
      phr_cauchy_schwarz: ip(x,y)^2 <= phr_norm2 x * phr_norm2 y    Qed

File: 1301 LOC, 52 Qed, 0 Admitted, 0 banned constructs.
Next (Session 5): self-adjoint operators + commutator + Robertson bound.

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

Author: hyperpolymath

proofs/canonical-proof-suite/S4_heisenberg_ndim.v

@@ -1211,6 +1211,17 @@ Proof.
   rewrite Hy_eq. apply phr_ip_zero_r_real.
 Qed.
 
+(** ip(neg x, y) = - ip(x, y), derived from symmetry + neg_r. *)
+Lemma phr_ip_neg_l : forall (H : PreHilbertR) (x y : H),
+    phr_ip H (phr_neg H x) y = - phr_ip H x y.
+Proof.
+  intros H x y.
+  rewrite (phr_ip_sym H (phr_neg H x) y).
+  rewrite phr_ip_neg_r.
+  rewrite phr_ip_sym.
+  reflexivity.
+Qed.
+
 (* §10c — Abstract Cauchy-Schwarz for PreHilbertR *)
 
 (** Auxiliary vector: w = λ·x - ip(y,x)·y where λ = phr_norm2 y *)
@@ -1231,16 +1242,34 @@ Proof.
   unfold phr_cs_aux, phr_norm2.
   (* w = (phr_norm2 H y)·x + neg((phr_ip H y x)·y).
      Expand ip(w,w) by bilinearity and symmetry. *)
+  (* Name the three scalar values for clarity. *)
   set (λ := phr_ip H y y).
-  (* Do NOT set β here — keep phr_ip H y x literal so rewrites find it. *)
+  set (β := phr_ip H y x).
+  set (w1 := phr_scal H λ x).
+  set (w2 := phr_neg H (phr_scal H β y)).
+  (* Assert the four bilinear terms. *)
+  assert (H11 : phr_ip H w1 w1 = λ * λ * phr_ip H x x).
+  { unfold w1. rewrite phr_ip_scal_l. rewrite phr_ip_scal_r. ring. }
+  assert (H12 : phr_ip H w1 w2 = λ * (- β) * phr_ip H x y).
+  { unfold w1, w2. rewrite phr_ip_scal_l. rewrite phr_ip_neg_r.
+    rewrite phr_ip_scal_r. ring. }
+  assert (H21 : phr_ip H w2 w1 = λ * (- β) * phr_ip H x y).
+  { unfold w1, w2. rewrite phr_ip_neg_l. rewrite phr_ip_scal_l.
+    rewrite phr_ip_scal_r. rewrite (phr_ip_sym H y x). fold β. ring. }
+  assert (H22 : phr_ip H w2 w2 = β * β * λ).
+  { unfold w2. rewrite phr_ip_neg_l. rewrite phr_ip_neg_r.
+    rewrite phr_ip_scal_l. rewrite phr_ip_scal_r. fold λ. ring. }
+  (* ip(w, w) = H11 + H12 + H21 + H22 *)
+  unfold phr_cs_aux.
   rewrite phr_ip_linear_l.
-  rewrite phr_ip_linear_r, phr_ip_linear_r.
-  rewrite phr_ip_scal_l, phr_ip_scal_l.
-  rewrite phr_ip_scal_r, phr_ip_scal_r.
-  rewrite phr_ip_neg_r, phr_ip_neg_r.
-  (* Now ip(y,x) appears literally — apply symmetry *)
-  rewrite (phr_ip_sym H y x).
-  (* Everything is now in terms of λ = ip(y,y) and ip(x,y). *)
+  rewrite phr_ip_linear_r. rewrite phr_ip_linear_r.
+  fold w1 w2.
+  rewrite H11, H12, H21, H22.
+  (* β = ip(y,x) = ip(x,y) *)
+  assert (Hβ : β = phr_ip H x y).
+  { unfold β. apply phr_ip_sym. }
+  rewrite Hβ.
+  fold λ.
   ring.
 Qed.
 
@@ -1250,27 +1279,170 @@ Theorem phr_cauchy_schwarz :
     (phr_ip H x y)^2 <= phr_norm2 H x * phr_norm2 H y.
 Proof.
   intros H x y.
-  unfold phr_norm2.
-  set (λ := phr_ip H y y).
-  set (A := phr_ip H x y).
-  pose proof (phr_norm2_nonneg H x) as Hxnn. unfold phr_norm2 in Hxnn.
-  pose proof (phr_norm2_nonneg H y) as Hynn. unfold phr_norm2 in Hynn.
-  destruct (Req_dec λ 0) as [Hy0 | Hynz].
-  - (* λ = 0 ⟹ ip(x,y) = 0 ⟹ LHS = 0 *)
-    assert (Hy_eq : y = phr_zero H).
-    { apply phr_ip_zero_iff. exact Hy0. }
-    assert (HAzero : A = 0).
-    { unfold A. rewrite Hy_eq. apply phr_ip_zero_r_real. }
-    rewrite HAzero. ring_simplify. lra.
-  - assert (Hypos : 0 < λ) by lra.
+  pose proof (phr_norm2_nonneg H x) as Hxnn.
+  pose proof (phr_norm2_nonneg H y) as Hynn.
+  unfold phr_norm2 in *.
+  destruct (Req_dec (phr_ip H y y) 0) as [Hy0 | Hynz].
+  - (* ip(y,y) = 0 ⟹ y = 0 ⟹ ip(x,y) = 0 ⟹ LHS = 0 *)
+    assert (Hy_eq : y = phr_zero H) by (apply phr_ip_zero_iff; exact Hy0).
+    assert (HAzero : phr_ip H x y = 0).
+    { rewrite Hy_eq. apply phr_ip_zero_r_real. }
+    rewrite HAzero. rewrite Hy0. lra.
+  - assert (Hypos : 0 < phr_ip H y y) by lra.
     pose proof (phr_cs_expand_norm H x y) as Haux.
     pose proof (phr_norm2_nonneg H (phr_cs_aux H x y)) as Hauxnn.
     unfold phr_norm2 in Haux, Hauxnn.
     rewrite Haux in Hauxnn.
-    (* Hauxnn: 0 <= λ * (λ * ip(x,x) - A^2) *)
-    assert (Hbracket : 0 <= λ * phr_ip H x x - A^2).
-    { apply Rmult_le_reg_l with (r := λ); [exact Hypos|].
+    (* Hauxnn: 0 <= ip(y,y) * (ip(y,y)*ip(x,x) - ip(x,y)^2) *)
+    assert (Hbracket : 0 <= phr_ip H y y * phr_ip H x x - (phr_ip H x y)^2).
+    { apply Rmult_le_reg_l with (r := phr_ip H y y); [exact Hypos|].
       rewrite Rmult_0_r. lra. }
-    unfold λ, A in *.
     lra.
 Qed.
+
+(* ====================================================================
+   §11  Rung 4 — Self-adjoint operators, variance, and Robertson
+        uncertainty (real PreHilbert, unit-vector state).
+
+   Deliverable:
+     §11a  Definition: SelfAdj H A — symmetric (self-adjoint) linear map.
+     §11b  Definition: expect, variance, centered vector.
+     §11c  Key lemma: norm2 of centered vector = variance (for self-adjoint A
+           and unit psi).
+     §11d  robertson_real: Var(A) * Var(B) >= Cov(A,B)^2 — follows directly
+           from phr_cauchy_schwarz on the centered vectors.
+
+   This closes Rung 4.  The full quantum Robertson (complex scalars,
+   commutator lower bound) is Rung 5+ (not in scope this session).
+   ==================================================================== *)
+
+(* ── §11a  Self-adjoint operator ─────────────────────────────────────── *)
+
+(** A (possibly nonlinear) endomorphism of H. *)
+Definition PHREndo (H : PreHilbertR) := H -> H.
+
+(** Self-adjointness / symmetry: ip x (A y) = ip (A x) y for all x, y. *)
+Definition SelfAdj (H : PreHilbertR) (A : PHREndo H) : Prop :=
+  forall x y : H, phr_ip H x (A y) = phr_ip H (A x) y.
+
+(** Self-adjoint A implies ip (A x) y = ip x (A y). *)
+Lemma self_adj_swap :
+  forall (H : PreHilbertR) (A : PHREndo H),
+    SelfAdj H A ->
+    forall x y : H, phr_ip H (A x) y = phr_ip H x (A y).
+Proof.
+  intros H A Hadj x y.
+  symmetry. apply Hadj.
+Qed.
+
+(** Self-adjoint A: ip (A x) x = ip x (A x). *)
+Lemma self_adj_diag_sym :
+  forall (H : PreHilbertR) (A : PHREndo H),
+    SelfAdj H A ->
+    forall x : H, phr_ip H (A x) x = phr_ip H x (A x).
+Proof.
+  intros H A Hadj x.
+  rewrite (self_adj_swap H A Hadj x x). reflexivity.
+Qed.
+
+(* ── §11b  Expectation, variance, and centered vector ────────────────── *)
+
+(** Expectation of operator A in state psi: E_psi(A) = ip psi (A psi). *)
+Definition phr_expect (H : PreHilbertR) (A : PHREndo H) (psi : H) : R :=
+  phr_ip H psi (A psi).
+
+(** Variance: Var_psi(A) = E_psi(A^2) - E_psi(A)^2.
+    Defined as ip psi (A(A psi)) - (ip psi (A psi))^2. *)
+Definition phr_variance (H : PreHilbertR) (A : PHREndo H) (psi : H) : R :=
+  phr_ip H psi (A (A psi)) - (phr_ip H psi (A psi))^2.
+
+(** Centered vector: u_A = A psi - E_A * psi.
+    When psi is a unit vector, ||u_A||^2 = Var_psi(A). *)
+Definition phr_centered (H : PreHilbertR) (A : PHREndo H) (psi : H) : H :=
+  phr_add H (A psi) (phr_neg H (phr_scal H (phr_ip H psi (A psi)) psi)).
+
+(* ── §11c  Norm of centered vector = variance (for unit, self-adjoint) ── *)
+
+(** Unit-state: ||psi||^2 = 1. *)
+Definition phr_unit (H : PreHilbertR) (psi : H) : Prop :=
+  phr_norm2 H psi = 1.
+
+(** For a self-adjoint A and a unit psi, ip(A psi)(psi) = E_psi(A).
+    (Immediate from self_adj_swap + symmetry of ip.) *)
+Lemma self_adj_ip_Apsi_psi :
+  forall (H : PreHilbertR) (A : PHREndo H) (psi : H),
+    SelfAdj H A ->
+    phr_ip H (A psi) psi = phr_expect H A psi.
+Proof.
+  intros H A psi Hadj.
+  unfold phr_expect.
+  rewrite (phr_ip_sym H (A psi) psi).
+  apply Hadj.
+Qed.
+
+(** Expand ip(u_A, u_A) for self-adjoint A and unit psi. *)
+Lemma phr_centered_norm2 :
+  forall (H : PreHilbertR) (A : PHREndo H) (psi : H),
+    SelfAdj H A ->
+    phr_unit H psi ->
+    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_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.
+Qed.
+
+(* ── §11d  Robertson uncertainty bound ───────────────────────────────── *)
+
+(** Covariance of A and B in state psi:
+    Cov_psi(A, B) = ip(u_A, u_B) where u_X is the centered vector of X.
+    For self-adjoint A, B and unit psi this equals
+    ip(psi, A(B psi)) - E_A * E_B. *)
+Definition phr_covariance (H : PreHilbertR) (A B : PHREndo H) (psi : H) : R :=
+  phr_ip H (phr_centered H A psi) (phr_centered H B psi).
+
+(** Robertson uncertainty for a real PreHilbert space:
+    Var_psi(A) * Var_psi(B) >= Cov_psi(A, B)^2.
+
+    Proof: let u = u_A (centered vector of A) and v = u_B.
+    By phr_cauchy_schwarz: (ip u v)^2 <= ip(u,u) * ip(v,v).
+    By phr_centered_norm2:  ip(u,u) = Var(A) and ip(v,v) = Var(B).
+    By definition:          ip(u,v) = Cov(A, B).
+    Together:               Cov^2 <= Var(A) * Var(B). *)
+Theorem robertson_real :
+  forall (H : PreHilbertR) (A B : PHREndo H) (psi : H),
+    SelfAdj H A ->
+    SelfAdj H B ->
+    phr_unit H psi ->
+    (phr_covariance H A B psi)^2 <= phr_variance H A psi * phr_variance H B psi.
+Proof.
+  intros H A B psi HsA HsB Hunit.
+  unfold phr_covariance.
+  (* By phr_cauchy_schwarz: (ip u v)^2 <= norm2 u * norm2 v. *)
+  pose proof (phr_cauchy_schwarz H
+                (phr_centered H A psi)
+                (phr_centered H B psi)) as Hcs.
+  (* Rewrite norm2(u_A) = Var(A) and norm2(u_B) = Var(B). *)
+  rewrite (phr_centered_norm2 H A psi HsA Hunit) in Hcs.
+  rewrite (phr_centered_norm2 H B psi HsB Hunit) in Hcs.
+  (* phr_cauchy_schwarz gives (ip u v)^2 <= norm2 u * norm2 v. *)
+  lra.
+Qed.