Bump lean4 to v4.30.0-rc2

.devcontainer/Dockerfile

@@ -14,5 +14,5 @@ RUN apt-get update && \
 USER vscode
 WORKDIR /home/vscode
 
-RUN curl https://elan.lean-lang.org/elan-init.sh -sSf | sh -s -- -y --default-toolchain leanprover/lean4:4.27.0-rc1
+RUN curl https://elan.lean-lang.org/elan-init.sh -sSf | sh -s -- -y --default-toolchain leanprover/lean4:4.30.0-rc2
 ENV PATH="/home/vscode/.elan/bin:${PATH}"

.gitignore

@@ -5,3 +5,6 @@ lefthook-local.yml
 references/
 skill-creator-tests/
 **/__pycache__/
+
+# Ignore until https://github.com/microsoft/vscode-remote-release/issues/11616 is fixed.
+devcontainer-lock.json

QuantumSystem/Algebra/CStarAlgebra/GNS/Construction.lean

@@ -18,7 +18,7 @@ open ComplexConjugate NNReal Topology Filter
 variable {A : Type*} [NonUnitalCStarAlgebra A]
 variable (ω : State ℂ A)
 
-def Nω : CStarAlgebraIdeal A where
+@[reducible] def Nω : CStarAlgebraIdeal A where
   carrier := { x : A | ω (star x * x) = 0 }
   zero_mem' := by
     change ω (star (0 : A) * (0 : A)) = 0
@@ -42,7 +42,7 @@ local notation "Nω" => (Nω ω)
 `⟪[x], [y]⟫ = ω (star x * y)`.  Well-defined because the kernel ideal `Nω` is the null space
 with respect to the positive sesquilinear form coming from the state `ω` (ultimately a
 consequence of the Cauchy–Schwarz inequality for states). -/
-def innerQuotient (xq yq : A ⧸ Nω) : ℂ :=
+noncomputable def innerQuotient (xq yq : A ⧸ Nω) : ℂ :=
   Quotient.liftOn₂' xq yq (fun x y => ω (star x * y))
     (fun x₁ y₁ x₂ y₂ (hx : CStarAlgebraIdeal.leftRel Nω x₁ x₂) (hy : CStarAlgebraIdeal.leftRel Nω y₁ y₂) => by
       rw [CStarAlgebraIdeal.leftRel, QuotientAddGroup.leftRel_apply] at hx hy
@@ -54,7 +54,7 @@ def innerQuotient (xq yq : A ⧸ Nω) : ℂ :=
         _ = ω (star x₂ * y₂) := (State.equiv_right (ω := ω) (x := x₂) (y₁ := y₂) (y₂ := y₁) hy').symm)
 
 /-- The inner product space core structure on the quotient. -/
-instance instInnerProductSpaceCore : InnerProductSpace.Core ℂ (A ⧸ Nω) where
+noncomputable abbrev innerProductSpaceCoreQuot : InnerProductSpace.Core ℂ (A ⧸ Nω) where
   inner := innerQuotient ω
   conj_inner_symm := fun x y => Quotient.inductionOn₂' x y fun a b => by
     simp only [innerQuotient, Quotient.liftOn₂'_mk'']
@@ -81,34 +81,39 @@ instance instInnerProductSpaceCore : InnerProductSpace.Core ℂ (A ⧸ Nω) wher
   definite := fun x hx => Quotient.inductionOn' x (fun a ha => by
     have ha' : ω (star a * a) = 0 := by
       simpa [innerQuotient] using ha
-    exact Quotient.sound' (by
-      simpa [CStarAlgebraIdeal.leftRel, QuotientAddGroup.leftRel_apply] using ha')) hx
+    apply Quotient.sound'
+    rw [CStarAlgebraIdeal.leftRel, QuotientAddGroup.leftRel_apply]
+    simpa using ha') hx
 
--- Pattern adapted from Mathlib 4.25+ Matrix.PosDef
--- First define NormedAddCommGroup from the Core (not an instance yet)
-noncomputable def normedAddCommGroupQuot : NormedAddCommGroup (A ⧸ Nω) :=
-  @InnerProductSpace.Core.toNormedAddCommGroup ℂ _ _ _ _ (instInnerProductSpaceCore (ω := ω))
-
--- Then define InnerProductSpace using ofCore with explicit SeminormedAddCommGroup
-noncomputable def innerProductSpaceQuot : @InnerProductSpace ℂ (A ⧸ Nω) _ (normedAddCommGroupQuot (ω := ω)).toSeminormedAddCommGroup :=
-  letI : InnerProductSpace.Core ℂ (A ⧸ Nω) := instInnerProductSpaceCore (ω := ω)
-  @InnerProductSpace.ofCore ℂ _ _ (normedAddCommGroupQuot (ω := ω)).toAddCommGroup _ inferInstance
-
--- Now make them instances
+-- Pattern from Mathlib's GelfandNaimarkSegal: separate Core abbrev and IPS instances.
 noncomputable instance instNormedAddCommGroupQuot : NormedAddCommGroup (A ⧸ Nω) :=
-  normedAddCommGroupQuot (ω := ω)
+  @InnerProductSpace.Core.toNormedAddCommGroup ℂ (A ⧸ Nω) _ _ _ (innerProductSpaceCoreQuot ω)
+
+/-- The pre-inner product structure derived from the InnerProductSpace.Core. -/
+noncomputable instance instPreInnerProductSpaceCoreQuot : PreInnerProductSpace.Core ℂ (A ⧸ Nω) where
+  inner := innerQuotient ω
+  conj_inner_symm := (innerProductSpaceCoreQuot ω).conj_inner_symm
+  re_inner_nonneg := (innerProductSpaceCoreQuot ω).re_inner_nonneg
+  add_left := (innerProductSpaceCoreQuot ω).add_left
+  smul_left := (innerProductSpaceCoreQuot ω).smul_left
 
 noncomputable instance instInnerProductSpaceQuot : InnerProductSpace ℂ (A ⧸ Nω) :=
-  innerProductSpaceQuot (ω := ω)
+  InnerProductSpace.ofCore (instPreInnerProductSpaceCoreQuot ω)
+
+/-- Inner product on the quotient is the `innerQuotient` function. This holds because the
+`InnerProductSpace` instance on the quotient is built reducibly from the corresponding
+`InnerProductSpace.Core`. -/
+private lemma inner_quotient_eq (x y : A ⧸ Nω) :
+    @inner ℂ (A ⧸ Nω) _ x y = innerQuotient ω x y := rfl
 
 /-- The squared norm of the class `[x]` equals the real part `Re (ω (star x * x))`. -/
 private lemma norm_sq_eq_inner (x : A) :
     @norm (A ⧸ Nω) (instNormedAddCommGroupQuot ω).toNorm (Quotient.mk'' x) ^ 2 = (ω (star x * x)).re := by
   rw [@norm_sq_eq_re_inner ℂ (A ⧸ Nω) _ _]
-  change ((@inner ℂ (A ⧸ Nω) _ (Quotient.mk'' x) (Quotient.mk'' x))).re = (ω (star x * x)).re
-  change (innerQuotient ω (Quotient.mk'' x) (Quotient.mk'' x)).re = (ω (star x * x)).re
+  rw [inner_quotient_eq]
   unfold innerQuotient
   simp only [Quotient.liftOn₂'_mk'']
+  rfl
 
 /-- Inner products with elements of the kernel ideal vanish: if `s ∈ Nω` then
 `ω (star x * s) = 0`. -/
@@ -154,8 +159,7 @@ lemma πω'_norm_sq_le (a : A) (b : A ⧸ Nω) : ‖πω' ω a b‖ ^ 2 ≤ ‖a
   -- Use inner_self = ‖·‖ * ‖·‖ in a pre-Hilbert setting (core inner product structure)
   rw [← inner_self_eq_norm_mul_norm (𝕜 := ℂ) (E := A ⧸ Nω) (Quotient.mk'' (a * b'))]
   rw [← inner_self_eq_norm_mul_norm (𝕜 := ℂ) (E := A ⧸ Nω) (Quotient.mk'' b')]
-  change (innerQuotient ω (Quotient.mk'' (a * b')) (Quotient.mk'' (a * b'))).re ≤
-    ‖a‖ * ‖a‖ * (innerQuotient ω (Quotient.mk'' b') (Quotient.mk'' b')).re
+  rw [inner_quotient_eq, inner_quotient_eq]
   unfold innerQuotient; simp only [Quotient.liftOn₂'_mk'']
   -- Algebraic rearrangement: bring star inside and reassociate to isolate star a * a
   rw [show star (a * b') * (a * b') = star b' * star a * a * b' by rw [star_mul, mul_assoc, mul_assoc, mul_assoc]]
@@ -172,6 +176,7 @@ lemma πω'_norm_sq_le (a : A) (b : A ⧸ Nω) : ‖πω' ω a b‖ ^ 2 ≤ ‖a
   have : ‖a‖ * ‖a‖ * (ω (star b' * b')).re = ‖a‖ * (‖a‖ * (ω (star b' * b')).re) := mul_assoc _ _ _
   have hr_nonneg : (0 : ℝ) ≤ r := r.property
   -- Finish with linear arithmetic: nonneg remainder r gives desired ≤
+  change (ω (star b' * star a * a * b')).re ≤ ‖a‖ * ‖a‖ * (ω (star b' * b')).re
   linarith
 
 /-- Multiplicativity: πω'(ab) = πω'(a) ∘ πω'(b). -/
@@ -184,7 +189,7 @@ lemma πω'_inner (a : A) (b c : A ⧸ Nω) :
   refine Quotient.inductionOn₂' b c fun b' c' => ?_
   unfold πω'
   simp only [Quotient.liftOn'_mk'']
-  change innerQuotient ω (Quotient.mk'' (a * b')) (Quotient.mk'' c') = innerQuotient ω (Quotient.mk'' b') (Quotient.mk'' (star a * c'))
+  rw [inner_quotient_eq, inner_quotient_eq]
   unfold innerQuotient
   simp only [Quotient.liftOn₂'_mk'', star_mul, mul_assoc]
 
@@ -380,7 +385,7 @@ lemma stateOnQuotFun_bound (x : A ⧸ Nω) : ‖stateOnQuotFun ω x‖ ≤ 1 * 
   -- Derive global bound by contradiction if limit were strictly larger
   have : ‖ω a‖ ^ 2 ≤ (ω (star a * a)).re := by
     haveI : (CStarAlgebra.approximateUnit A).NeBot := h_approx.toIsApproximateUnit.neBot
-    by_contra hlt; push_neg at hlt
+    by_contra hlt; push Not at hlt
     set δ : ℝ := (‖ω a‖ ^ 2 - (ω (star a * a)).re) / 2
     have hδ_pos : 0 < δ := half_pos (sub_pos.mpr hlt)
     have h_close := (Metric.tendsto_nhds.mp h_tendsto) δ hδ_pos
@@ -528,11 +533,11 @@ lemma ξω_norm : ‖ξω ω‖ = 1 := by
     suffices 1 ≤ ‖stateOnQuot ω‖ from this.trans h2
     have h_norm : ‖ω‖ = 1 := ω.norm_eq_one
     rw [← h_norm]
-    by_contra h_not; push_neg at h_not
+    by_contra h_not; push Not at h_not
     -- Expand definition of norm via supremum over ratios ‖ω a‖/‖a‖
     rw [State.norm_def] at h_not
     obtain ⟨_, ⟨a, ha, rfl⟩, h_r_large⟩ : ∃ r ∈ {s : ℝ | ∃ a : A, a ≠ 0 ∧ s = ‖ω a‖ / ‖a‖}, ‖stateOnQuot ω‖ < r := by
-      by_contra h_no; push_neg at h_no
+      by_contra h_no; push Not at h_no
       have : sSup {s : ℝ | ∃ a : A, a ≠ 0 ∧ s = ‖ω a‖ / ‖a‖} ≤ ‖stateOnQuot ω‖ := by
         refine csSup_le ?_ h_no
         by_contra h_empty

QuantumSystem/Algebra/CStarAlgebra/GNS/DirectSum.lean

@@ -245,7 +245,7 @@ theorem directSumAlgHom_injective : Function.Injective (directSumAlgHom (A := A)
           simp
         · simp only [dif_neg h, if_neg h]; simp
       rw [h_eq]
-      apply summable_of_finite_support
+      apply summable_of_hasFiniteSupport
       have :
           Function.support (fun ψ' => if ψ' = ψ then ‖ψ.gnsRepresentation.ξ‖ ^ 2 else 0) ⊆ {ψ} := by
         intro ψ' hψ'

QuantumSystem/Algebra/CStarAlgebra/GNS/PureState.lean

@@ -54,7 +54,7 @@ lemma isInvariant_orthogonal (T : GNS.Representation ω) (W : Submodule ℂ T.H)
   refine (W.mem_orthogonal ((T.π a) x)).2 ?_
   intro w hw
   have hw_map : (T.π (star a)) w ∈ W.map (T.π (star a)) :=
-    ⟨w, hw, rfl⟩
+    ⟨w, hw, by rfl⟩
   have hw' : (T.π (star a)) w ∈ W := (hWinv (star a)) hw_map
   have hx0 : ⟪(T.π (star a)) w, x⟫ = 0 := by
     -- `x ∈ Wᗮ` means it is orthogonal to every element of `W`.
@@ -167,7 +167,7 @@ lemma vectorFunctional_isPositive (T : GNS.Representation ω) (v : T.H) :
         rw [RCLike.ofReal_eq_complex_ofReal]
         exact (Complex.ofReal_pow ‖(T.π a) v‖ 2).symm
   -- Convert the RHS into the form expected by `IsPositive` (with an `ℝ≥0` witness).
-  simp [h]
+  rw [h]; rfl
 
 lemma opNorm_vectorFunctional_le (T : GNS.Representation ω) (v : T.H) :
     ‖WeakDual.toStrongDual (T.vectorFunctional v)‖ ≤ ‖v‖ ^ 2 := by
@@ -259,7 +259,7 @@ lemma normalized_vectorFunctional_mem_quasiStateSpace (T : GNS.Representation ω
   · -- Positivity
     have hpos := vectorFunctional_isPositive T v
     let c : ℝ≥0 := ⟨(‖v‖ ^ 2)⁻¹, inv_nonneg.mpr (sq_nonneg _)⟩
-    have : (‖v‖ ^ 2 : ℂ)⁻¹ = (c : ℂ) := by simp [c, Complex.ofReal_inv]
+    have : (‖v‖ ^ 2 : ℂ)⁻¹ = (c : ℂ) := by simp [c]; norm_cast
     rw [this]
     change _ ∈ {φ | IsPositive A φ}
     have h_smul : (c : ℂ) • T.vectorFunctional v = c • T.vectorFunctional v := by
@@ -284,7 +284,7 @@ lemma trichotomy_from_purity {ψ : PureState A}
     ‖v₁‖ ^ 2 = 0 ∨ ‖v₁‖ ^ 2 = 1 := by
   let T := PureState.gnsRepresentation ψ
   by_contra h_contra
-  push_neg at h_contra
+  push Not at h_contra
   have h_in_Icc := norm_sq_in_Icc T v₁ v₂ hξ horth
   have h_pos : 0 < ‖v₁‖ ^ 2 := lt_of_le_of_ne h_in_Icc.1 h_contra.1.symm
   have h_lt_one : ‖v₁‖ ^ 2 < 1 := lt_of_le_of_ne h_in_Icc.2 h_contra.2
@@ -321,12 +321,12 @@ lemma trichotomy_from_purity {ψ : PureState A}
     have h1_sub_t_ne_c : (1 - (t : ℂ)) ≠ 0 := by
       have : ((1 - t : ℝ) : ℂ) ≠ 0 := Complex.ofReal_ne_zero.mpr h1_sub_t_ne
       simpa only [Complex.ofReal_one, Complex.ofReal_sub] using this
-    have ht_smul : (t : ℝ) • φ = (t : ℂ) • φ :=
-      RCLike.real_smul_eq_coe_smul (K := ℂ) (E := WeakDual ℂ A) t φ
+    have ht_smul : (t : ℝ) • φ = (t : ℂ) • φ := by
+      apply ContinuousLinearMap.ext; intro a; rfl
     have h1_smul : (1 - t : ℝ) • χ = (1 - (t : ℂ)) • χ := by
-      -- First use RCLike lemma to get (1 - t) • χ = ↑(1 - t) • χ
-      have step1 : (1 - t : ℝ) • χ = ((1 - t : ℝ) : ℂ) • χ :=
-        RCLike.real_smul_eq_coe_smul (K := ℂ) (E := WeakDual ℂ A) (1 - t) χ
+      -- First show (1 - t) • χ = ↑(1 - t) • χ
+      have step1 : (1 - t : ℝ) • χ = ((1 - t : ℝ) : ℂ) • χ := by
+        apply ContinuousLinearMap.ext; intro a; rfl
       -- Then rewrite ↑(1 - t) as (1 - ↑t)
       rw [step1, Complex.ofReal_sub, Complex.ofReal_one]
     have h_sum_c : ψ.val = (t : ℂ) • φ + (1 - (t : ℂ)) • χ := by
@@ -339,9 +339,12 @@ lemma trichotomy_from_purity {ψ : PureState A}
       have hrhs :
           ((t : ℂ) • φ + (1 - (t : ℂ)) • χ) a =
             (T.vectorFunctional v₁) a + (T.vectorFunctional v₂) a := by
-        rw [ContinuousLinearMap.add_apply, ContinuousLinearMap.smul_apply, ContinuousLinearMap.smul_apply]
+        change (t : ℂ) • φ a + (1 - (t : ℂ)) • χ a = _
         dsimp only [φ, χ]
-        rw [ContinuousLinearMap.smul_apply, ContinuousLinearMap.smul_apply]
+        rw [show ((t : ℂ)⁻¹ • T.vectorFunctional v₁) a
+              = (t : ℂ)⁻¹ • (T.vectorFunctional v₁) a from rfl,
+          show ((1 - (t : ℂ))⁻¹ • T.vectorFunctional v₂) a
+              = (1 - (t : ℂ))⁻¹ • (T.vectorFunctional v₂) a from rfl]
         rw [smul_smul, smul_smul]
         rw [mul_inv_cancel₀ ht_ne_c, mul_inv_cancel₀ h1_sub_t_ne_c]
         rw [one_smul, one_smul]
@@ -367,10 +370,23 @@ lemma trichotomy_from_purity {ψ : PureState A}
   have h_eq : φ = χ := by rw [h_eq2, ← h_eq1]
   -- Contradiction via density
   have h_dense : Dense (Set.range (fun a => (T.π a) T.ξ)) := by
-    change Dense (Set.range (T.piApply T.ξ))
-    rw [← LinearMap.coe_range]
-    rw [← Submodule.span_eq (LinearMap.range (T.piApply T.ξ))]
-    exact T.cyclic
+    have h_cyc := T.cyclic
+    -- View `Set.range (fun a => π a ξ)` via `T.piApply T.ξ` as a `LinearMap.range`,
+    -- then identify it with the cyclic span used by `T.cyclic`.
+    have h1 : (Set.range (fun a => (T.π a) T.ξ))
+        = ((LinearMap.range (T.piApply T.ξ).toLinearMap) : Set T.H) := by
+      rw [LinearMap.coe_range]; rfl
+    have h2 : ((LinearMap.range (T.piApply T.ξ).toLinearMap) : Set T.H)
+        = (Submodule.span ℂ (Set.range (fun a => (T.π a) T.ξ)) : Set T.H) := by
+      rw [h1]
+      congr 1
+      exact (Submodule.span_eq _).symm
+    rw [h1, h2]
+    -- Now reduce `Submodule.span ℂ (Set.range _)` to the set-builder form used by `T.cyclic`.
+    have h3 : (Set.range (fun a => (T.π a) T.ξ)) = {T.π a T.ξ | a : A} := by
+      ext y; simp
+    rw [h3]
+    exact h_cyc
   have hv₁_mem_closure : v₁ ∈ closure (Set.range (fun a => (T.π a) T.ξ)) := by
     rw [h_dense.closure_eq]
     exact Set.mem_univ v₁
@@ -420,7 +436,7 @@ lemma trichotomy_from_purity {ψ : PureState A}
   -- Contradiction
   have h_phi : ‖φ a - 1‖ < 1/2 := by
     dsimp only [φ]
-    rw [ContinuousLinearMap.smul_apply]
+    change ‖(t : ℂ)⁻¹ • (T.vectorFunctional v₁) a - 1‖ < 1/2
     have : (t : ℂ)⁻¹ • T.vectorFunctional v₁ a - 1 = (t : ℂ)⁻¹ * ⟪v₁, (T.π a) v₁ - v₁⟫ := by
       have ht_ne_c : (t : ℂ) ≠ 0 := Complex.ofReal_ne_zero.mpr h_pos.ne'
       rw [vectorFunctional_apply]
@@ -461,7 +477,8 @@ lemma trichotomy_from_purity {ψ : PureState A}
           _ = 1 / 2 := by simp
   have h_chi : ‖χ a‖ < 1/2 := by
     dsimp only [χ]
-    rw [ContinuousLinearMap.smul_apply, vectorFunctional_apply, smul_eq_mul]
+    change ‖(1 - (t : ℂ))⁻¹ • (T.vectorFunctional v₂) a‖ < 1/2
+    rw [vectorFunctional_apply, smul_eq_mul]
     rw [norm_mul, ← Complex.ofReal_one, ← Complex.ofReal_sub, norm_inv, Complex.norm_real, Real.norm_eq_abs, abs_of_pos (by linarith : 0 < 1 - t)]
     calc (1 - t)⁻¹ * ‖⟪v₂, (T.π a) v₂⟫‖
       _ ≤ (1 - t)⁻¹ * (‖v₂‖ * ‖(T.π a) v₂‖) := by

QuantumSystem/Algebra/CStarAlgebra/GNS/Representation.lean

@@ -49,7 +49,7 @@ variable {ω : State ℂ A}
 /-- A submodule `W` of the Hilbert space of a GNS representation is invariant if it is
 stable under the action of `π(a)` for every `a : A`. -/
 def IsInvariant (T : Representation ω) (W : Submodule ℂ T.H) : Prop :=
-  ∀ a : A, W.map (T.π a) ≤ W
+  ∀ a : A, W.map (T.π a).toLinearMap ≤ W
 
 /-- A GNS representation is (topologically) irreducible if the only **closed** invariant
 submodules are `⊥` and `⊤`. -/
@@ -60,11 +60,13 @@ def IsIrreducible (T : Representation ω) : Prop :=
     (W = ⊥ ∨ W = ⊤)
 
 @[simp] lemma isInvariant_bot (T : Representation ω) : T.IsInvariant (⊥ : Submodule ℂ T.H) := by
+  unfold IsInvariant
   intro a w hw
   rcases (show w = 0 from by simpa using hw) with rfl
   simp
 
 @[simp] lemma isInvariant_top (T : Representation ω) : T.IsInvariant (⊤ : Submodule ℂ T.H) := by
+  unfold IsInvariant
   intro a w hw
   simp
 
@@ -115,7 +117,7 @@ private lemma norm_cyclic (T₁ T₂ : Representation ω) (a : A) :
   exact congr_arg RCLike.re (inner_cyclic T₁ T₂ a a)
 
 /-- The canonical correspondence on cyclic orbit vectors: `π₁(a) ξ₁ ↦ π₂(a) ξ₂`. -/
-private def cyclicCorrespondence (_T₁ T₂ : Representation ω) (a : A) : T₂.H :=
+private noncomputable def cyclicCorrespondence (_T₁ T₂ : Representation ω) (a : A) : T₂.H :=
   T₂.π a T₂.ξ
 
 /-- Well-definedness of the cyclic correspondence: equality in the first triplet forces