proof(S4): Session 7 — ComplexPreHilbert + robertson_complex (Rung 5)

§14a–§14d: ComplexPreHilbert record (re+im decomposition, complex CS axiom),
CPHHerm definition, cph_im_self_zero, cph_herm_expect_imag_zero,
cph_commutator_re_zero, cph_im_commutator, cph_im_centered_centered,
cph_centered_re_variance, cph_cs_im, robertson_complex.

Theorem robertson_complex (Rung 5):
  For Hermitian A, B and unit ψ in a complex pre-Hilbert space:
    ¼·|⟨ψ,[A,B]ψ⟩|² ≤ Var_ψ(A)·Var_ψ(B).
Re = 0 (anti-Hermitian commutator), Im = 2·im(u,v), im(u,v)² ≤ Var·Var (CS).
This is the operator-algebra Heisenberg bound in abstract Robertson form.

98 Qed, 0 Admitted. The full headline target of this WIP file is reached.

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

Author: hyperpolymath

proofs/canonical-proof-suite/S4_heisenberg_ndim.v

@@ -1585,13 +1585,260 @@ Qed.
        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.
+   WHAT IS NOT PROVED (within this session stack)
+
+   Rung 5 is proved in §14 (Session 7) below.
+   ==================================================================== *)
+
+(* ====================================================================
+   §14  Rung 5 — Complex Robertson bound (Session 7).
+
+   We introduce ComplexPreHilbert, a record whose inner product decomposes
+   into a real part (cph_re : H → H → R, symmetric, positive definite,
+   bilinear) and an imaginary part (cph_im : H → H → R, anti-symmetric,
+   bilinear).  Complex Cauchy-Schwarz:
+
+       cph_re(x,y)² + cph_im(x,y)² ≤ cph_re(x,x) · cph_re(y,y)
+
+   is taken as a record axiom (cph_cs).  It is derivable via the complex
+   structure J : H → H with J² = −I, re(x,Jy) = −im(x,y), ‖Jy‖ = ‖y‖,
+   but the derivation adds ~60 LOC irrelevant to the Robertson bound.
+
+   Hermitian (self-adjoint for ℂ) operator condition:
+       CPHHerm H A  ≡  ∀x y, re(x,Ay) = re(Ax,y)  ∧  im(x,Ay) = im(Ax,y)
+
+   Proof skeleton:
+
+     1. Re⟨ψ,[A,B]ψ⟩ = 0            (commutator anti-Hermitian → real part = 0)
+     2. Im⟨ψ,[A,B]ψ⟩ = 2·im(Aψ,Bψ) (Hermitian A,B + im anti-symmetry)
+     3. im(u,v) = im(Aψ,Bψ)         (Hermitian expectations are real → cross
+                                      terms im(Aψ,ψ), im(ψ,Bψ), im(ψ,ψ) = 0)
+     4. im(u,v)² ≤ Var(A)·Var(B)    (complex CS projected to imaginary part)
+     5. ¼·|⟨ψ,[A,B]ψ⟩|² ≤ Var(A)·Var(B) (combine 1–4)
+
+   The RHS of the modulus |⟨ψ,[A,B]ψ⟩|² = Re²+Im² reduces to Im²
+   because Re = 0 (step 1).  Im = 2·im(u,v) (steps 2–3), so
+   ¼·Im² = im(u,v)² ≤ Var(A)·Var(B) (step 4).
    ==================================================================== *)
+
+(* ── §14a  ComplexPreHilbert record ───────────────────────────────── *)
+
+Record ComplexPreHilbert : Type := mkCPH {
+  cph_carrier  :> Type;
+  cph_add  : cph_carrier -> cph_carrier -> cph_carrier;
+  cph_scal : R -> cph_carrier -> cph_carrier;
+  cph_neg  : cph_carrier -> cph_carrier;
+  cph_zero : cph_carrier;
+  cph_re   : cph_carrier -> cph_carrier -> R;
+  cph_im   : cph_carrier -> cph_carrier -> R;
+  (* additive group *)
+  cph_add_comm   : forall x y, cph_add x y = cph_add y x;
+  cph_add_assoc  : forall x y z, cph_add (cph_add x y) z = cph_add x (cph_add y z);
+  cph_add_zero_l : forall x, cph_add cph_zero x = x;
+  cph_add_neg_l  : forall x, cph_add (cph_neg x) x = cph_zero;
+  cph_scal_add   : forall a x y,
+    cph_scal a (cph_add x y) = cph_add (cph_scal a x) (cph_scal a y);
+  (* re: symmetric bilinear, positive definite *)
+  cph_re_sym    : forall x y, cph_re x y = cph_re y x;
+  cph_re_lin_r  : forall x y z, cph_re x (cph_add y z) = cph_re x y + cph_re x z;
+  cph_re_lin_l  : forall x y z, cph_re (cph_add x y) z = cph_re x z + cph_re y z;
+  cph_re_scal_r : forall x y a, cph_re x (cph_scal a y) = a * cph_re x y;
+  cph_re_scal_l : forall x y a, cph_re (cph_scal a x) y = a * cph_re x y;
+  cph_re_neg_r  : forall x y, cph_re x (cph_neg y) = - cph_re x y;
+  cph_re_neg_l  : forall x y, cph_re (cph_neg x) y = - cph_re x y;
+  cph_re_nonneg : forall x, 0 <= cph_re x x;
+  cph_re_zero   : forall x, cph_re x x = 0 <-> x = cph_zero;
+  (* im: anti-symmetric bilinear *)
+  cph_im_anti   : forall x y, cph_im x y = - cph_im y x;
+  cph_im_lin_r  : forall x y z, cph_im x (cph_add y z) = cph_im x y + cph_im x z;
+  cph_im_lin_l  : forall x y z, cph_im (cph_add x y) z = cph_im x z + cph_im y z;
+  cph_im_scal_r : forall x y a, cph_im x (cph_scal a y) = a * cph_im x y;
+  cph_im_scal_l : forall x y a, cph_im (cph_scal a x) y = a * cph_im x y;
+  cph_im_neg_r  : forall x y, cph_im x (cph_neg y) = - cph_im x y;
+  cph_im_neg_l  : forall x y, cph_im (cph_neg x) y = - cph_im x y;
+  (* complex Cauchy-Schwarz: re(x,y)² + im(x,y)² ≤ re(x,x) · re(y,y).
+     Derivable via complex structure J (J²=-I, re(x,Jy)=-im(x,y),
+     ‖Jy‖=‖y‖); taken as axiom to avoid ~60 LOC of structural boilerplate. *)
+  cph_cs : forall x y, cph_re x y ^ 2 + cph_im x y ^ 2 <= cph_re x x * cph_re y y;
+}.
+
+(* ── §14b  Hermitian operators and predicates ─────────────────────── *)
+
+(** A is Hermitian iff ⟨x,Ay⟩ = ⟨Ax,y⟩ in both re and im components. *)
+Definition CPHHerm (H : ComplexPreHilbert) (A : H -> H) : Prop :=
+  forall x y : H,
+    cph_re H x (A y) = cph_re H (A x) y /\
+    cph_im H x (A y) = cph_im H (A x) y.
+
+Definition cph_unit (H : ComplexPreHilbert) (psi : H) : Prop :=
+  cph_re H psi psi = 1.
+
+Definition cph_expect (H : ComplexPreHilbert) (A : H -> H) (psi : H) : R :=
+  cph_re H psi (A psi).
+
+Definition cph_variance (H : ComplexPreHilbert) (A : H -> H) (psi : H) : R :=
+  cph_re H psi (A (A psi)) - (cph_re H psi (A psi)) ^ 2.
+
+Definition cph_centered (H : ComplexPreHilbert) (A : H -> H) (psi : H) : H :=
+  cph_add H (A psi) (cph_neg H (cph_scal H (cph_expect H A psi) psi)).
+
+Definition cph_commutator (H : ComplexPreHilbert) (A B : H -> H) (x : H) : H :=
+  cph_add H (A (B x)) (cph_neg H (B (A x))).
+
+(* ── §14c  Derived lemmas ─────────────────────────────────────────── *)
+
+Lemma cph_im_self_zero (H : ComplexPreHilbert) (x : H) : cph_im H x x = 0.
+Proof.
+  pose proof (cph_im_anti H x x) as Hanti. lra.
+Qed.
+
+(** Hermitian operators have purely real expectations: Im⟨ψ,Aψ⟩ = 0. *)
+Lemma cph_herm_expect_imag_zero (H : ComplexPreHilbert) (A : H -> H) (psi : H) :
+    CPHHerm H A -> cph_im H psi (A psi) = 0.
+Proof.
+  intros HA.
+  destruct (HA psi psi) as [_ Him].
+  pose proof (cph_im_anti H (A psi) psi) as Hanti.
+  lra.
+Qed.
+
+(** For Hermitian A, B: Re⟨ψ,[A,B]ψ⟩ = 0. *)
+Lemma cph_commutator_re_zero (H : ComplexPreHilbert) (A B : H -> H) (psi : H) :
+    CPHHerm H A -> CPHHerm H B ->
+    cph_re H psi (cph_commutator H A B psi) = 0.
+Proof.
+  intros HA HB.
+  unfold cph_commutator.
+  rewrite cph_re_lin_r, cph_re_neg_r.
+  destruct (HA psi (B psi)) as [HAre _].
+  destruct (HB psi (A psi)) as [HBre _].
+  rewrite HAre, HBre, (cph_re_sym H (A psi) (B psi)).
+  lra.
+Qed.
+
+(** For Hermitian A, B: Im⟨ψ,[A,B]ψ⟩ = 2·Im⟨Aψ,Bψ⟩. *)
+Lemma cph_im_commutator (H : ComplexPreHilbert) (A B : H -> H) (psi : H) :
+    CPHHerm H A -> CPHHerm H B ->
+    cph_im H psi (cph_commutator H A B psi) =
+      2 * cph_im H (A psi) (B psi).
+Proof.
+  intros HA HB.
+  unfold cph_commutator.
+  rewrite cph_im_lin_r, cph_im_neg_r.
+  destruct (HA psi (B psi)) as [_ HAim].
+  destruct (HB psi (A psi)) as [_ HBim].
+  pose proof (cph_im_anti H (B psi) (A psi)) as Hanti.
+  lra.
+Qed.
+
+(** Im of centered vectors equals Im⟨Aψ,Bψ⟩ — all cross-terms vanish
+    because Hermitian expectations are real (Im⟨ψ,Aψ⟩ = 0). *)
+Lemma cph_im_centered_centered (H : ComplexPreHilbert) (A B : H -> H) (psi : H) :
+    CPHHerm H A -> CPHHerm H B ->
+    cph_im H (cph_centered H A psi) (cph_centered H B psi) =
+      cph_im H (A psi) (B psi).
+Proof.
+  intros HA HB.
+  unfold cph_centered, cph_expect.
+  set (EA := cph_re H psi (A psi)).
+  set (EB := cph_re H psi (B psi)).
+  assert (Hbil :
+    cph_im H (cph_add H (A psi) (cph_neg H (cph_scal H EA psi)))
+             (cph_add H (B psi) (cph_neg H (cph_scal H EB psi)))
+    = cph_im H (A psi) (B psi)
+      - EB * cph_im H (A psi) psi
+      - EA * cph_im H psi (B psi)
+      + EA * EB * cph_im H psi psi).
+  { rewrite cph_im_lin_l.
+    rewrite cph_im_lin_r; rewrite cph_im_lin_r.
+    rewrite cph_im_neg_r; rewrite cph_im_neg_r.
+    rewrite cph_im_scal_r; rewrite cph_im_scal_r.
+    rewrite cph_im_neg_l; rewrite cph_im_neg_l.
+    rewrite cph_im_scal_l; rewrite cph_im_scal_l.
+    ring. }
+  rewrite Hbil.
+  pose proof (cph_herm_expect_imag_zero H A psi HA) as HimA.
+  pose proof (cph_herm_expect_imag_zero H B psi HB) as HimB.
+  pose proof (cph_im_self_zero H psi) as Himp.
+  assert (HimApsi : cph_im H (A psi) psi = 0).
+  { rewrite cph_im_anti. lra. }
+  rewrite HimApsi, HimB, Himp. ring.
+Qed.
+
+(** Re(u,u) = Var_ψ(A) for centered u = Aψ − ⟨A⟩·ψ, Hermitian A, unit ψ. *)
+Lemma cph_centered_re_variance (H : ComplexPreHilbert) (A : H -> H) (psi : H) :
+    CPHHerm H A -> cph_unit H psi ->
+    cph_re H (cph_centered H A psi) (cph_centered H A psi) =
+      cph_variance H A psi.
+Proof.
+  intros HA Hunit.
+  unfold cph_centered, cph_expect, cph_variance.
+  unfold cph_unit in Hunit.
+  set (E := cph_re H psi (A psi)).
+  assert (Hbil :
+    cph_re H (cph_add H (A psi) (cph_neg H (cph_scal H E psi)))
+             (cph_add H (A psi) (cph_neg H (cph_scal H E psi)))
+    = cph_re H (A psi) (A psi)
+      - E * cph_re H (A psi) psi
+      - E * cph_re H psi (A psi)
+      + E * E * cph_re H psi psi).
+  { rewrite cph_re_lin_l.
+    rewrite cph_re_lin_r; rewrite cph_re_lin_r.
+    rewrite cph_re_neg_r; rewrite cph_re_neg_r.
+    rewrite cph_re_scal_r; rewrite cph_re_scal_r.
+    rewrite cph_re_neg_l; rewrite cph_re_neg_l.
+    rewrite cph_re_scal_l; rewrite cph_re_scal_l.
+    ring. }
+  rewrite Hbil.
+  assert (HAA : cph_re H (A psi) (A psi) = cph_re H psi (A (A psi))).
+  { symmetry. destruct (HA psi (A psi)) as [Hre _]. exact Hre. }
+  assert (HAp : cph_re H (A psi) psi = E).
+  { unfold E. apply cph_re_sym. }
+  assert (Hpp : cph_re H psi psi = 1). { exact Hunit. }
+  rewrite HAA, HAp, Hpp. unfold E. ring.
+Qed.
+
+(** Im² ≤ Re(x,x)·Re(y,y): imaginary CS, from cph_cs by discarding Re². *)
+Lemma cph_cs_im (H : ComplexPreHilbert) (x y : H) :
+    cph_im H x y ^ 2 <= cph_re H x x * cph_re H y y.
+Proof.
+  pose proof (cph_cs H x y) as Hcs.
+  nra.
+Qed.
+
+(* ── §14d  Complex Robertson bound ───────────────────────────────── *)
+
+(** For Hermitian A, B and unit ψ in a complex pre-Hilbert space:
+        ¼ · |⟨ψ,[A,B]ψ⟩|² ≤ Var_ψ(A) · Var_ψ(B),
+    where |⟨ψ,[A,B]ψ⟩|² = Re⟨ψ,[A,B]ψ⟩² + Im⟨ψ,[A,B]ψ⟩².
+
+    The real case (§12d, Theorem robertson_commutator) is trivial because
+    Re⟨ψ,[A,B]ψ⟩ = 0 AND Im⟨ψ,[A,B]ψ⟩ = 0 (commutator vanishes).
+    The complex case is non-trivial: Re = 0 but Im need not vanish.
+
+    This is the full Heisenberg bound in its Robertson form, matching the
+    headline statement in the file header (abstractly, without spectral
+    theorem or operator domain considerations). *)
+Theorem robertson_complex :
+  forall (H : ComplexPreHilbert) (A B : H -> H) (psi : H),
+    CPHHerm H A -> CPHHerm H B -> cph_unit H psi ->
+    (1/4) * (cph_re H psi (cph_commutator H A B psi) ^ 2
+             + cph_im H psi (cph_commutator H A B psi) ^ 2)
+    <= cph_variance H A psi * cph_variance H B psi.
+Proof.
+  intros H A B psi HA HB Hunit.
+  (* Step 1: Re⟨ψ,[A,B]ψ⟩ = 0. *)
+  pose proof (cph_commutator_re_zero H A B psi HA HB) as Hre0.
+  (* Step 2: Im⟨ψ,[A,B]ψ⟩ = 2·im(Aψ,Bψ). *)
+  pose proof (cph_im_commutator H A B psi HA HB) as Him2.
+  (* Step 3: im(u,v) = im(Aψ,Bψ). *)
+  pose proof (cph_im_centered_centered H A B psi HA HB) as Himuv.
+  (* Step 4: im(u,v)² ≤ Var(A)·Var(B) via complex CS. *)
+  pose proof (cph_cs_im H (cph_centered H A psi) (cph_centered H B psi)) as Hcs.
+  rewrite (cph_centered_re_variance H A psi HA Hunit) in Hcs.
+  rewrite (cph_centered_re_variance H B psi HB Hunit) in Hcs.
+  rewrite Himuv in Hcs.
+  (* Combine: ¼·(0² + (2·im(Aψ,Bψ))²) = im(Aψ,Bψ)² ≤ Var(A)·Var(B). *)
+  rewrite Hre0, Him2.
+  nra.
+Qed.