Polish

.github/workflows/blueprint.yml

@@ -16,16 +16,14 @@ permissions:
   contents: read          # Read access to repository contents
   pages: write            # Write access to GitHub Pages
   id-token: write         # Write access to ID tokens
-  issues: write           # Write access to issues
-  pull-requests: write    # Write access to pull requests
 
 jobs:
   build_project:
     runs-on: ubuntu-latest
     name: Build project
     steps:
       - name: Cleanup to free disk space
-        uses: jlumbroso/free-disk-space@main
+        uses: jlumbroso/free-disk-space@3f13feab2962a87273d379ebc36ea159527e6cc9 # v1.3.2
         with:
           tool-cache: false
           android: true

.github/workflows/lean_action_ci.yml

@@ -18,8 +18,8 @@ jobs:
     runs-on: ubuntu-latest
 
     steps:
-      - uses: actions/checkout@v5
-      - uses: leanprover/lean-action@v1
+      - uses: actions/checkout@v6
+      - uses: leanprover/lean-action@434f25c2f80ded67bba02502ad3a86f25db50709 # 2025-07-02
         with:
           build: true
           lint: true

Physicslib4/AQFT/HaagKastler/Net.lean

@@ -338,11 +338,15 @@ noncomputable def trivialQuasilocalAlgebra :
       ⟨trivialBasisSet, isAlexandrovBasisSet_trivialBasisSet, x, rfl⟩)
   ι_inclusion := fun _ _ _ _ _ _ => rfl
 
+/-- The trivial local net satisfies Axiom 3 (local commutativity), since `ℂ` is
+commutative. -/
 theorem trivialLocalNet_localCommutativity :
     LocalCommutativity trivialLocalNet trivialLocalNetIsotony := by
   intro B₁ B₂ B hB₁ hB₂ hB _ h₁ h₂ a b
   exact @mul_comm ℂ _ _ _
 
+/-- The trivial local net satisfies Axiom 5 (Lorentz covariance), realized by the
+identity automorphism of `ℂ` at every basis set. -/
 theorem trivialLocalNet_lorentzCovariance :
     LorentzCovariance trivialLocalNet trivialLocalNetIsotony := by
   refine ⟨fun _ _ => StarAlgEquiv.refl ℂ ℂ, ?_, ?_, ?_⟩

Physicslib4/AQFT/HaagKastler/QuasilocalIntertwiner.lean

@@ -360,6 +360,7 @@ algebra. -/
 noncomputable def extendHom (L : InhomogeneousLorentzGroup) : Q.carrier →⋆ₐ[ℂ] Q.carrier :=
   (exists_intertwiner_extend N Q L).choose
 
+/-- The extended intertwiner `Φ_L` is continuous. -/
 theorem extendHom_continuous (L : InhomogeneousLorentzGroup) : Continuous (extendHom N Q L) :=
   (exists_intertwiner_extend N Q L).choose_spec.1
 
@@ -441,6 +442,7 @@ noncomputable def trivialQuasilocalLift (L : InhomogeneousLorentzGroup) :
     trivialHaagKastlerNet.QuasilocalLift trivialQuasilocalAlgebra L :=
   quasilocalLift trivialHaagKastlerNet trivialQuasilocalAlgebra L
 
+/-- The quasilocal lift exists unconditionally for the trivial net. -/
 theorem nonempty_trivialQuasilocalLift (L : InhomogeneousLorentzGroup) :
     Nonempty (trivialHaagKastlerNet.QuasilocalLift trivialQuasilocalAlgebra L) :=
   ⟨trivialQuasilocalLift L⟩

Physicslib4/AQFT/HaagKastler/QuasilocalKMS.lean

@@ -93,10 +93,11 @@ fixing `Ω`, the one-parameter unitary group `t ↦ U t` has positive energy
 ground-state (`β → ∞`, spectrum-condition) counterpart of `IsKMSStateForFlow`: the
 stationary state whose flow generator (the Hamiltonian, for a timelike flow) is
 positive. -/
-def IsGroundStateForFlow (flow : ℝ → InhomogeneousLorentzGroup)
+def IsGroundStateForFlow.{u} (N : HaagKastlerNet.{u})
+    (flow : ℝ → InhomogeneousLorentzGroup)
     (ω : Physicslib4.GNS.State N.quasilocal.carrier) : Prop :=
   (∀ (t : ℝ) (a : N.quasilocal.carrier), (ω (N.flowAut flow t a) : ℂ) = ω a) ∧
-    ∃ (K : Type) (_ : NormedAddCommGroup K) (_ : InnerProductSpace ℂ K)
+    ∃ (K : Type u) (_ : NormedAddCommGroup K) (_ : InnerProductSpace ℂ K)
       (_ : CompleteSpace K) (π : N.quasilocal.carrier →⋆ₐ[ℂ] (K →L[ℂ] K)) (Ω : K)
       (U : ℝ → (K ≃ₗᵢ[ℂ] K)),
         (∀ a : N.quasilocal.carrier, (ω a : ℂ) = ⟪Ω, π a Ω⟫_ℂ) ∧
@@ -116,11 +117,11 @@ open scoped InnerProductSpace in
 /-- The implementing unitary group of a covariance-flow ground state is strongly
 continuous: strong continuity is a field of the positive-energy hypothesis
 (`AQFT.IsPositiveEnergy.strongContinuous`). -/
-theorem IsGroundStateForFlow.exists_strongContinuous_unitary
-    (flow : ℝ → InhomogeneousLorentzGroup)
+theorem IsGroundStateForFlow.exists_strongContinuous_unitary.{u}
+    (N : HaagKastlerNet.{u}) (flow : ℝ → InhomogeneousLorentzGroup)
     {ω : Physicslib4.GNS.State N.quasilocal.carrier}
     (h : N.IsGroundStateForFlow flow ω) :
-    ∃ (K : Type) (_ : NormedAddCommGroup K) (_ : InnerProductSpace ℂ K)
+    ∃ (K : Type u) (_ : NormedAddCommGroup K) (_ : InnerProductSpace ℂ K)
       (_ : CompleteSpace K) (π : N.quasilocal.carrier →⋆ₐ[ℂ] (K →L[ℂ] K)) (Ω : K)
       (U : ℝ → (K ≃ₗᵢ[ℂ] K)),
         (∀ a : N.quasilocal.carrier, (ω a : ℂ) = ⟪Ω, π a Ω⟫_ℂ) ∧

Physicslib4/AQFT/HaagKastler/VacuumState.lean

@@ -122,11 +122,11 @@ def IsFutureTimelikeTranslation (γ : ℝ → InhomogeneousLorentzGroup) : Prop
 This packages the two *necessary* vacuum conditions — invariance and the spectrum
 condition. The predicate `ftl` is a parameter; `IsVacuumStateConcrete` fixes it to
 `IsFutureTimelikeTranslation`. -/
-def HaagKastlerNet.IsVacuumState (N : HaagKastlerNet)
+def HaagKastlerNet.IsVacuumState (N : HaagKastlerNet.{u})
     (ftl : (ℝ → InhomogeneousLorentzGroup) → Prop)
     (ω : Physicslib4.GNS.State N.quasilocal.carrier) : Prop :=
   N.IsInvariantState ω ∧
-    ∃ (K : Type) (_ : NormedAddCommGroup K) (_ : InnerProductSpace ℂ K)
+    ∃ (K : Type u) (_ : NormedAddCommGroup K) (_ : InnerProductSpace ℂ K)
       (_ : CompleteSpace K) (π : N.quasilocal.carrier →⋆ₐ[ℂ] (K →L[ℂ] K)) (Ω : K)
       (U : InhomogeneousLorentzGroup → (K ≃ₗᵢ[ℂ] K)),
         (∀ a : N.quasilocal.carrier, (ω a : ℂ) = ⟪Ω, π a Ω⟫_ℂ) ∧

Physicslib4/AQFT/HaagKastlerCurved/Concrete.lean

@@ -38,7 +38,8 @@ The pieces of the abstract interface are read off the concrete spacetime:
 * `Isom` is the oriented identity component
   `Spacetime.Isometry.orientedIdentityComponent` (the topological
   `connectedComponentOfOne` intersected with future-orientation preservation),
-  matching the blueprint's "isometries connected to the identity" in Axiom 5;
+  which is the blueprint's group of "isometries connected to the identity" in
+  Axiom 5 (see the implementation note on `toAbstractIdentityComponent`);
 * `isBasisSet_smul` is `Spacetime.LorentzianSpacetime.isBasisSet_smul`: these
   isometries carry Alexandrov diamonds to Alexandrov diamonds.
 -/
@@ -56,6 +57,12 @@ component** (identity-component isometries that also preserve the future
 orientation), as in Axiom 5. For these isometries basis-set preservation is a
 theorem (`Spacetime.LorentzianSpacetime.isBasisSet_smul`), which supplies the
 interface field `isBasisSet_smul`.
+
+Implementation note: the oriented identity component is the group of isometries
+connected to the identity named in the blueprint. That an isometry connected to
+the identity preserves the future orientation needs a Myers–Steenrod-type rigidity
+theorem that Mathlib does not provide, so orientation preservation is included in
+the definition of the group rather than proved.
 -/
 noncomputable def toAbstractIdentityComponent (L : LorentzianSpacetime) :
     AQFT.HaagKastlerCurved.LorentzianSpacetime where

Physicslib4/AQFT/KMS.lean

@@ -36,7 +36,8 @@ This is the analytic form of the KMS condition (Bratteli-Robinson): at inverse
 temperature `β > 0`, `ω` is KMS iff for all `a, b` there is `F` continuous on the
 strip `{0 ≤ Im z ≤ β}`, holomorphic in the interior, with `F(t) = ω(a α_t b)`
 and `F(t + iβ) = ω(α_t b · a)`. KMS states are automatically `α`-invariant
-(`IsKMSState.invariant`, unconditionally for `β > 0` by `IsKMSState.invariant_of_pos`).
+(`IsKMSState.invariant`, given a `StripLiouville β` hypothesis; `IsKMSState.invariant_of_pos`
+discharges that extra hypothesis automatically whenever `β > 0`).
 -/
 
 namespace Physicslib4

Physicslib4/AQFT/PositiveEnergy.lean

@@ -69,7 +69,7 @@ one-parameter unitary group — `exp(i t P) = exp(i t Q)` for all `t` — they a
 Differentiating at `t = 0` gives `i P = i Q`, hence `P = Q`. The unbounded form is
 `generator_eq_of_eq_expUnitary`.
 
-Blueprint reference: `lmm:exp-generator-unique`. -/
+Blueprint reference: the bounded special case of `lmm:exp-generator-unique`. -/
 theorem exp_generator_unique {P Q : H →L[ℂ] H}
     (h : ∀ (t : ℝ) (x : H),
       NormedSpace.exp (((t : ℂ) * Complex.I) • P) x

Physicslib4/GNS/Amplification.lean

@@ -44,6 +44,9 @@ theorem summandProj_isScalar_of_isIrreducible (hirr : IsIrreducible (directSum 
     summandProj (H := H) j ∈ scalarOperators (lp H 2) :=
   isIrreducible_iff_centralizer.mp hirr ▸ summandProj_mem_commutant π j
 
+-- `DecidableEq ι` is bound by the ambient `variable` but only used irrelevantly, through
+-- `lp.single`/instance resolution, not by name in this proof; the `unusedDecidableInType`
+-- linter flags it when the full project is built (though not in isolation).
 set_option linter.unusedDecidableInType false in
 /-- A direct sum with two summands carrying nonzero vectors is **reducible**: the
 projection onto one summand is a non-scalar element of the commutant. -/

Physicslib4/GNS/Basic.lean

@@ -34,9 +34,11 @@ here. The positivity condition is stated using the canonical
 partial order on `ℂ` from Mathlib: `0 ≤ z` iff `z.re ≥ 0` and `z.im = 0`.
 
 The blueprint statement of `def:cyclic-vector` only requires `A` to be an
-algebra; here we keep the assumptions general enough to be reusable but
-require the operator-algebra side `H →L[ℂ] H` to make sense, so `H` is a
-complex Hilbert space.
+algebra, but `IsCyclicVector` is declared under this file's ambient
+`variable (A : Type*) [CStarAlgebra A]`, so in Lean `A` is a unital C*-algebra
+(matching every call site in the project). The generality kept here is on the
+`H` side: `H` is required only to be a complex Hilbert space, not fixed to the
+GNS space of a particular state.
 -/
 
 namespace Physicslib4

Physicslib4/GNS/PureStateExists.lean

@@ -71,6 +71,7 @@ theorem isClosed_complex_nonneg : IsClosed {z : ℂ | (0 : ℂ) ≤ z} := by
   exact (isClosed_Ici.preimage Complex.continuous_re).inter
     (isClosed_singleton.preimage Complex.continuous_im)
 
+/-- The state set is weak-* closed. -/
 theorem isClosed_weakStateSet : IsClosed (weakStateSet : Set (WeakDual ℂ A)) := by
   have h1 : IsClosed {φ : WeakDual ℂ A | ∀ a : A, (0 : ℂ) ≤ φ (star a * a)} := by
     rw [Set.ofPred_forall]
@@ -80,8 +81,15 @@ theorem isClosed_weakStateSet : IsClosed (weakStateSet : Set (WeakDual ℂ A)) :
     isClosed_singleton.preimage (WeakDual.eval_continuous 1)
   exact h1.inter h2
 
-theorem isCompact_weakStateSet [Nontrivial A] :
+/-- **Banach–Alaoglu for states.** The state set is weak-* compact. -/
+theorem isCompact_weakStateSet :
     IsCompact (weakStateSet : Set (WeakDual ℂ A)) := by
+  rcases subsingleton_or_nontrivial A with hA | hA
+  · convert isCompact_empty
+    refine Set.eq_empty_of_forall_notMem fun φ hφ => ?_
+    have h := hφ.2
+    rw [Subsingleton.elim (1 : A) 0, map_zero] at h
+    exact zero_ne_one h
   refine (WeakDual.isCompact_closedBall (0 : StrongDual ℂ A) 1).of_isClosed_subset
     isClosed_weakStateSet ?_
   intro φ hφ

Physicslib4/Spacetime/CausalComplement.lean

@@ -180,6 +180,8 @@ noncomputable def causalClosure : ClosureOperator (Set M.Carrier) :=
 def IsCausallyComplete (B : Set M.Carrier) : Prop :=
   M.spacelikeComplement (M.spacelikeComplement B) = B
 
+/-- A region is causally complete iff it is a closed element of the `causalClosure`
+closure operator. -/
 theorem isCausallyComplete_iff_isClosed {B : Set M.Carrier} :
     M.IsCausallyComplete B ↔ M.causalClosure.IsClosed B := by
   rw [ClosureOperator.isClosed_iff]
@@ -331,6 +333,8 @@ private theorem coe_iInf {ι : Sort*} (B : ι → M.CausallyCompleteRegion) :
   rw [Set.iInf_eq_iInter] at h'
   exact h'
 
+/-- The causal complement is **antitone**: a larger causally complete region has a
+smaller (or equal) causal complement. -/
 theorem causalComplement_antitone : Antitone M.causalComplement := by
   intro B₁ B₂ h
   rw [← Subtype.coe_le_coe]

Physicslib4/Spacetime/CrossMetricIsometry.lean

@@ -562,6 +562,9 @@ theorem pullback_alexandrovBasis_image (M : Spacetime) (ψ : Diffeo M M)
     (M.pullbackTimeOrientation ψ t) t
     (pullback_preservesFutureOrientationTwoSided M ψ t) hB
 
+-- Needed for the same reason as the `respectTransparency` options in `Pullback.lean` (see the
+-- comment on `bilinearPrecomp` there): `TangentSpace M.model x` is only semireducibly, not
+-- reducibly, defeq to `SpacetimeModel`.
 set_option backward.isDefEq.respectTransparency false in
 /-- **`ψ⁻¹` carries Alexandrov basis sets to pullback Alexandrov basis sets**
 (`lmm:pullback-alexandrov-homeomorphism`, backward matching hypothesis).

Physicslib4/Spacetime/IsometryCausality.lean

@@ -199,10 +199,10 @@ noncomputable def futureOrientationPreserving (M : Spacetime) (t : M.TimeOrienta
   Iff.rfl
 
 /-- The **oriented identity component**: the identity-component isometries that
-also preserve the future orientation. This folds orientation-preservation into
-the identity-component group of Axiom 5, sidestepping the statement that every
-identity-component isometry preserves orientation, which the C⁰ topology used
-here does not give. -/
+also preserve the future orientation. This is the identity-component group of
+Axiom 5: every identity-component isometry preserves the future orientation, but
+the proof needs a Myers–Steenrod-type rigidity theorem that Mathlib does not
+provide, so orientation preservation is part of the definition instead. -/
 noncomputable def orientedIdentityComponent (M : Spacetime) (t : M.TimeOrientation) :
     Subgroup (Isometry M) :=
   Isometry.identityComponent M ⊓ futureOrientationPreserving M t

Physicslib4/Spacetime/LorentzCauchySchwarz.lean

@@ -13,16 +13,19 @@ import Mathlib.LinearAlgebra.BilinearForm.Basic
 This file formalises the blueprint declaration `lmm:reverse-cauchy-schwarz`
 (Chapter 10, `sections/sec10/spacetime`).
 
-For a symmetric Lorentzian bilinear form `g` (signature `diag(-1,1,1,1)`) and two
-timelike vectors `v, w` (i.e. `g v v < 0`, `g w w < 0`) the *reverse* Cauchy-Schwarz
-inequality holds:
+For a symmetric Lorentzian bilinear form `g` (signature `diag(-1,1,1,1)`) and a
+timelike vector `w` (i.e. `g w w < 0`) the *reverse* Cauchy-Schwarz inequality
+holds for every `v`:
 ```
 g v v * g w w ≤ (g v w) ^ 2.
 ```
 
-The abstract statement `reverse_cauchy_schwarz_of_lorentzianAt` depends only on the
-pointwise `LorentzianAt` condition, so it transfers verbatim to the metric `g|_p` of
-any spacetime; `Spacetime.reverse_cauchy_schwarz` is that specialisation.
+The abstract statement `reverse_cauchy_schwarz_of_lorentzianAt` only needs `w` to
+be timelike, which is stronger than the blueprint's `lmm:reverse-cauchy-schwarz`
+(stated symmetrically, with both `v` and `w` timelike); the specialisation
+`Spacetime.reverse_cauchy_schwarz` keeps the blueprint's symmetric hypotheses to
+match its statement. It depends only on the pointwise `LorentzianAt` condition,
+so it transfers verbatim to the metric `g|_p` of any spacetime.
 
 ## Proof strategy
 
@@ -41,13 +44,16 @@ namespace Physicslib4
 
 open scoped BigOperators
 
-/-- **Reverse Cauchy-Schwarz inequality** for two timelike vectors of a symmetric
-Lorentzian bilinear form on a real four-dimensional vector space. -/
+/-- **Reverse Cauchy-Schwarz inequality** for a timelike vector `w` of a symmetric
+Lorentzian bilinear form on a real four-dimensional vector space, and an arbitrary
+vector `v`. Only `w` needs to be timelike: this is stronger than the blueprint's
+`lmm:reverse-cauchy-schwarz`, which states the symmetric hypothesis `v, w` both
+timelike. -/
 theorem reverse_cauchy_schwarz_of_lorentzianAt
     {V : Type*} [AddCommGroup V] [Module ℝ V]
     {B : LinearMap.BilinForm ℝ V} (_hsymm : ∀ v w, B v w = B w v)
     (hL : LorentzianAt (fun v w => B v w))
-    {v w : V} (_hv : B v v < 0) (hw : B w w < 0) :
+    {v w : V} (hw : B w w < 0) :
     B v v * B w w ≤ (B v w) ^ 2 := by
   obtain ⟨b, hb⟩ := hL
   -- Beta-reduced form of the Gram-matrix hypothesis, usable directly by `rw`.
@@ -95,10 +101,13 @@ theorem reverse_cauchy_schwarz_of_lorentzianAt
 namespace Spacetime
 
 /-- **Reverse Cauchy-Schwarz inequality** for the metric of a spacetime: two timelike
-tangent vectors at a point satisfy `g v v * g w w ≤ (g v w) ^ 2`. -/
+tangent vectors at a point satisfy `g v v * g w w ≤ (g v w) ^ 2`. The hypothesis on `v`
+is kept (unused in the proof) to match the blueprint's symmetric statement of
+`lmm:reverse-cauchy-schwarz`; see `reverse_cauchy_schwarz_of_lorentzianAt` for the
+sharper form that only needs `w` timelike. -/
 theorem reverse_cauchy_schwarz (M : Spacetime) (x : M.Carrier)
     {v w : TangentSpace M.model x}
-    (hv : M.IsTimelike v) (hw : M.IsTimelike w) :
+    (_hv : M.IsTimelike v) (hw : M.IsTimelike w) :
     M.val x v v * M.val x w w ≤ (M.val x v w) ^ 2 := by
   let B : LinearMap.BilinForm ℝ (TangentSpace M.model x) :=
     LinearMap.mk₂ ℝ (fun a c => M.val x a c)
@@ -109,9 +118,8 @@ theorem reverse_cauchy_schwarz (M : Spacetime) (x : M.Carrier)
     intro a c; rw [hBapp, hBapp]; exact M.symm x a c
   have hL : LorentzianAt (fun a c => B a c) := by
     simpa only [hBapp] using M.lorentzian x
-  have hv' : B v v < 0 := by rw [hBapp]; exact hv
   have hw' : B w w < 0 := by rw [hBapp]; exact hw
-  have h := reverse_cauchy_schwarz_of_lorentzianAt (B := B) hsymm hL hv' hw'
+  have h := reverse_cauchy_schwarz_of_lorentzianAt (B := B) (v := v) hsymm hL hw'
   simpa only [hBapp] using h
 
 end Spacetime

Physicslib4/Spacetime/LorentzCone.lean

@@ -70,7 +70,7 @@ theorem reverse_triangle_of_lorentzianAt
   have hc : (0 : ℝ) ≤ -(B v w) := by linarith
   -- Reverse Cauchy-Schwarz, rephrased for the nonnegative quantities.
   have hcs : B v v * B w w ≤ (B v w) ^ 2 :=
-    reverse_cauchy_schwarz_of_lorentzianAt hsymm hL hv hw
+    reverse_cauchy_schwarz_of_lorentzianAt hsymm hL hw
   have hab : (-(B v v)) * (-(B w w)) ≤ (-(B v w)) ^ 2 := by nlinarith [hcs]
   -- Hence `√a · √b ≤ c`.
   have hprod : Real.sqrt (-(B v v)) * Real.sqrt (-(B w w)) ≤ -(B v w) := by

Physicslib4/Spacetime/LorentzOrthogonal.lean

@@ -54,7 +54,7 @@ theorem nonneg_of_orthogonal_timelike
     {t u : V} (ht : B t t < 0) (h : B t u = 0) : 0 ≤ B u u := by
   by_contra hcon
   have hneg : B u u < 0 := not_le.mp hcon
-  have hcs := reverse_cauchy_schwarz_of_lorentzianAt hsymm hL ht hneg
+  have hcs := reverse_cauchy_schwarz_of_lorentzianAt (v := t) hsymm hL hneg
   rw [h] at hcs
   nlinarith [mul_pos_of_neg_of_neg ht hneg]
 
@@ -216,8 +216,8 @@ theorem bilin_neg_of_inner_t_neg
     ring
   rw [evp, ewp, evw] at hcs
   exact sign_algebra ht hv hw htv htw
-    (reverse_cauchy_schwarz_of_lorentzianAt hsymm hL ht hv)
-    (reverse_cauchy_schwarz_of_lorentzianAt hsymm hL ht hw) hcs
+    (reverse_cauchy_schwarz_of_lorentzianAt (v := t) hsymm hL hv)
+    (reverse_cauchy_schwarz_of_lorentzianAt (v := t) hsymm hL hw) hcs
 
 namespace Spacetime