proof(lean4/QuantumCNO): close all 4 sorries (4 → 0)

L75 quantum_state_eq_sym, L82 quantum_state_eq_trans
  - Original sigs `ψ =q= φ → φ =q= ψ` failed to parse under v4.16.0
    (notation:50 + → precedence interaction). Parenthesised both sides.
  - Original proofs were `sorry` with comment "Requires complex
    arithmetic". The simplified `quantumStateEq` definition (line 59)
    actually discards the phase θ — equality is purely pointwise on
    amplitudes — so symmetry is `(h n).symm` and transitivity is
    `(h1 n).trans (h2 n)`. No complex arith required by the spec as
    written.

L117 global_phase_is_cno (unitary conjunct)
  - `globalPhaseGate θ` is `fun ψ n => ψ n` which η-reduces to identity,
    so `innerProduct (globalPhaseGate θ ψ) (globalPhaseGate θ φ) =
    innerProduct ψ φ` is `rfl` directly.

L180 quantum_cno_composition (identity conjunct, second leg)
  - Comment misdiagnosed as "Need to show U ψ =q= U (V ψ)". After
    `apply quantum_state_eq_trans`, transitivity routes via `V ψ`, so
    the second leg is just `hV_id ψ`. Inlined as a single
    `quantum_state_eq_trans` term to avoid the apply/sorry split.

Author: hyperpolymath

proofs/lean4/QuantumCNO.lean

@@ -67,19 +67,24 @@ theorem quantum_state_eq_refl (ψ : QuantumState) : ψ =q= ψ := by
   intro n
   rfl
 
+/-- Symmetry of the (simplified) quantum-state equality.
+
+    The simplified `quantumStateEq` definition discards `θ`; equality is
+    purely pointwise on amplitudes. So `(-θ)` is just a placeholder phase
+    and what we actually need is `(h n).symm` for each component. -/
 theorem quantum_state_eq_sym (ψ φ : QuantumState) :
-    ψ =q= φ → φ =q= ψ := by
+    (ψ =q= φ) → (φ =q= ψ) := by
   intro ⟨θ, h⟩
-  exists (-θ)
-  intro n
-  sorry  -- Requires complex arithmetic
+  exact ⟨-θ, fun n => (h n).symm⟩
+
+/-- Transitivity of the (simplified) quantum-state equality.
 
+    With the placeholder phase, the transitive phase is just the sum and
+    the pointwise equalities chain via `Eq.trans`. -/
 theorem quantum_state_eq_trans (ψ φ χ : QuantumState) :
-    ψ =q= φ → φ =q= χ → ψ =q= χ := by
+    (ψ =q= φ) → (φ =q= χ) → (ψ =q= χ) := by
   intro ⟨θ1, h1⟩ ⟨θ2, h2⟩
-  exists (θ1 + θ2)
-  intro n
-  sorry  -- Requires complex arithmetic
+  exact ⟨θ1 + θ2, fun n => (h1 n).trans (h2 n)⟩
 
 /-! ## Quantum CNO Definition -/
 
@@ -113,15 +118,15 @@ def globalPhaseGate (θ : ℝ) : QuantumGate :=
 theorem global_phase_is_cno (θ : ℝ) :
     isQuantumCNO (globalPhaseGate θ) := by
   unfold isQuantumCNO globalPhaseGate
-  constructor
-  · sorry  -- Unitary
-  constructor
+  refine ⟨?_, ?_, trivial⟩
+  · -- isUnitary: in the simplified spec `globalPhaseGate θ` η-reduces to
+    -- the identity function `fun ψ => ψ`, so its image under
+    -- `innerProduct` matches `innerProduct ψ φ` definitionally.
+    intro ψ φ
+    rfl
   · intro ψ
     unfold quantumStateEq
-    exists θ
-    intro n
-    rfl
-  · trivial
+    exact ⟨θ, fun _ => rfl⟩
 
 /-! ## Non-CNO Gates -/
 
@@ -174,10 +179,11 @@ theorem quantum_cno_composition (U V : QuantumGate) :
   constructor
   · intro ψ
     unfold gateCompose
-    -- U(V ψ) = U ψ (since V ψ = ψ) = ψ (since U ψ = ψ)
-    apply quantum_state_eq_trans
-    · exact hU_id (V ψ)
-    · sorry  -- Need to show U ψ =q= U (V ψ) when V ψ =q= ψ
+    -- Goal: U (V ψ) =q= ψ. Chain U(Vψ)=q=Vψ (hU_id (V ψ)) with Vψ=q=ψ (hV_id ψ).
+    -- The original `sorry` comment misdiagnosed the second goal: after
+    -- `apply quantum_state_eq_trans`, transitivity routes via `V ψ`, so
+    -- the second leg is just `hV_id ψ`, not a U-rewrite under =q=.
+    exact quantum_state_eq_trans (U (V ψ)) (V ψ) ψ (hU_id (V ψ)) (hV_id ψ)
   · trivial
 
 /-! ## Quantum Information Theory -/