Numerous AQFT additions

Physicslib4.lean

@@ -37,17 +37,22 @@ import Physicslib4.Analysis.HorizontalLineRemovable
 import Physicslib4.Analysis.StripPeriodicExtension
 import Physicslib4.Analysis.StrongContinuity
 import Physicslib4.Basic
+import Physicslib4.GNS.Amplification
 import Physicslib4.GNS.Basic
 import Physicslib4.GNS.CauchySchwarz
 import Physicslib4.GNS.Construction
+import Physicslib4.GNS.DirectSum
 import Physicslib4.GNS.ExtremeState
 import Physicslib4.GNS.Irreducibility
 import Physicslib4.GNS.NullSpace
 import Physicslib4.GNS.PureStateExists
 import Physicslib4.GNS.RadonNikodym
 import Physicslib4.GNS.Separating
+import Physicslib4.GNS.Superselection
+import Physicslib4.GNS.UnitaryEquiv
 import Physicslib4.GNS.UnitaryRepresentation
 import Physicslib4.Operators.Conjugation
+import Physicslib4.Operators.LpDiagonal
 import Physicslib4.Spacetime.Basic
 import Physicslib4.Spacetime.CausalStructure
 import Physicslib4.Spacetime.Causality

Physicslib4/AQFT/HaagKastler/QuasilocalIntertwiner.lean

@@ -602,6 +602,49 @@ theorem IsInvariantState.exists_gns_unitary_strongContinuous
   Physicslib4.GNS.exists_gns_unitary_of_invariant_strongContinuous C.action ω hω
     C.action_mul_apply C.action_one_apply hwc
 
+open scoped InnerProductSpace in
+/-- **Bundled GNS unitary representation of an invariant state.** The bundled form
+of `IsInvariantState.exists_gns_unitary`: the implementing unitaries are returned
+as a genuine unitary representation `U : InhomogeneousLorentzGroup →* (H ≃ₗᵢ[ℂ] H)`
+(a bundled group homomorphism), rather than a bare family with separate group-law
+clauses. It feeds the covariance group homomorphism `C.actionHom` into the bundled
+analytic core `GNS.exists_gns_unitaryRep_of_invariant`. -/
+theorem IsInvariantState.exists_gns_unitaryRep (C : CovariantQuasilocalAlgebra)
+    {ω : Physicslib4.GNS.State C.quasilocal.carrier} (hω : C.IsInvariantState ω) :
+    ∃ (H : Type) (_ : NormedAddCommGroup H) (_ : InnerProductSpace ℂ H)
+      (_ : CompleteSpace H) (π : C.quasilocal.carrier →⋆ₐ[ℂ] (H →L[ℂ] H)) (Ω : H)
+      (U : InhomogeneousLorentzGroup →* (H ≃ₗᵢ[ℂ] H)),
+        (∀ a : C.quasilocal.carrier, (ω a : ℂ) = ⟪Ω, π a Ω⟫_ℂ) ∧
+        (∀ (L : InhomogeneousLorentzGroup) (a : C.quasilocal.carrier),
+          U L (π a Ω) = π (C.action L a) Ω) ∧
+        (∀ L : InhomogeneousLorentzGroup, U L Ω = Ω) ∧
+        (∀ (L : InhomogeneousLorentzGroup) (a : C.quasilocal.carrier) (x : H),
+          U L (π a ((U L).symm x)) = π (C.action L a) x) ∧
+        Physicslib4.GNS.IsCyclicVector π Ω :=
+  Physicslib4.GNS.exists_gns_unitaryRep_of_invariant C.actionHom ω hω
+
+open scoped InnerProductSpace in
+/-- **Bundled strongly continuous GNS unitary representation of an invariant state.**
+The bundled form of `IsInvariantState.exists_gns_unitary_strongContinuous`: the
+strongly continuous implementing unitaries are returned as a bundled group
+homomorphism `U : InhomogeneousLorentzGroup →* (H ≃ₗᵢ[ℂ] H)`. -/
+theorem IsInvariantState.exists_gns_unitaryRep_strongContinuous
+    (C : CovariantQuasilocalAlgebra)
+    {ω : Physicslib4.GNS.State C.quasilocal.carrier} (hω : C.IsInvariantState ω)
+    (hwc : ∀ a b : C.quasilocal.carrier,
+      Continuous fun L : InhomogeneousLorentzGroup => (ω (star a * C.action L b) : ℂ)) :
+    ∃ (H : Type) (_ : NormedAddCommGroup H) (_ : InnerProductSpace ℂ H)
+      (_ : CompleteSpace H) (π : C.quasilocal.carrier →⋆ₐ[ℂ] (H →L[ℂ] H)) (Ω : H)
+      (U : InhomogeneousLorentzGroup →* (H ≃ₗᵢ[ℂ] H)),
+        (∀ a : C.quasilocal.carrier, (ω a : ℂ) = ⟪Ω, π a Ω⟫_ℂ) ∧
+        (∀ (L : InhomogeneousLorentzGroup) (a : C.quasilocal.carrier),
+          U L (π a Ω) = π (C.action L a) Ω) ∧
+        (∀ L : InhomogeneousLorentzGroup, U L Ω = Ω) ∧
+        (∀ ψ : H, Continuous fun L : InhomogeneousLorentzGroup => U L ψ) ∧
+        (∀ (L : InhomogeneousLorentzGroup) (a : C.quasilocal.carrier) (x : H),
+          U L (π a ((U L).symm x)) = π (C.action L a) x) :=
+  Physicslib4.GNS.exists_gns_unitaryRep_of_invariant_strongContinuous C.actionHom ω hω hwc
+
 open scoped InnerProductSpace in
 /-- **Irreducible covariant representation of a pure invariant state (Minkowski).**
 A state `ω` on the quasilocal algebra that is both invariant under the covariance

Physicslib4/AQFT/HaagKastlerCurved/IdentityComponent.lean

@@ -69,6 +69,31 @@ can be rewritten to the concrete subgroup. -/
       = ↥(Spacetime.Isometry.orientedIdentityComponent L.toSpacetime
           L.timeOrientation) := rfl
 
+/-- The abstract isometry group of the `toAbstract` bridge inherits the
+topological-group topology of the concrete isometry group. This discharges the
+`[TopologicalSpace M.Isom]` hypothesis of the curved covariance/KMS results
+(e.g. the strongly continuous stabilizer GNS unitary) automatically for a net
+over a concrete Lorentzian spacetime — no explicit topology argument is needed. -/
+noncomputable instance instTopologicalSpaceToAbstractIsom (L : LorentzianSpacetime) :
+    TopologicalSpace (L.toAbstract).Isom :=
+  inferInstanceAs (TopologicalSpace (Isometry L.toSpacetime))
+
+/-- The abstract isometry group of the `toAbstractIdentityComponent` bridge
+inherits the subspace topology of the oriented identity-component subgroup,
+discharging `[TopologicalSpace M.Isom]` automatically over a concrete spacetime. -/
+noncomputable instance instTopologicalSpaceToAbstractIdentityComponentIsom
+    (L : LorentzianSpacetime) :
+    TopologicalSpace (L.toAbstractIdentityComponent).Isom :=
+  inferInstanceAs (TopologicalSpace
+    ↥(Spacetime.Isometry.orientedIdentityComponent L.toSpacetime L.timeOrientation))
+
+/-- Confirmation that the `[TopologicalSpace M.Isom]` requirement of the curved
+results is met by both bridges over a concrete spacetime. -/
+example (L : LorentzianSpacetime) : True := by
+  have _ : TopologicalSpace (L.toAbstract).Isom := inferInstance
+  have _ : TopologicalSpace (L.toAbstractIdentityComponent).Isom := inferInstance
+  trivial
+
 open scoped Pointwise in
 /-- **Axiom 5 basis-set preservation, stated over the abstract bridge.** Every
 isometry `φ` of the abstract spacetime carries Alexandrov-basis sets to basis

Physicslib4/AQFT/HaagKastlerCurved/Purity.lean

@@ -6,6 +6,7 @@ Authors: Lean Community
 import Physicslib4.AQFT.HaagKastlerCurved.Net
 import Physicslib4.GNS.RadonNikodym
 import Physicslib4.GNS.ExtremeState
+import Physicslib4.GNS.Superselection
 
 /-!
 # Purity of states on curved local algebras
@@ -90,6 +91,19 @@ theorem exists_gns_generates_all_of_isPure {B : Set M.Carrier} {ω : State (N.al
         gnsVonNeumann π = Set.univ :=
   GNS.exists_gns_generates_all_of_isPure hpure
 
+/-- **The irreducible dichotomy for curved local algebras.** Two irreducible
+representations of a curved local algebra `𝔘(B)` are either disjoint or unitarily
+equivalent. The abstract `GNS.areDisjoint_or_unitaryEquiv_of_isIrreducible` at the
+C*-algebra `𝔘(B)`. -/
+theorem areDisjoint_or_unitaryEquiv_of_isIrreducible {B : Set M.Carrier}
+    {H₁ H₂ : Type*}
+    [NormedAddCommGroup H₁] [InnerProductSpace ℂ H₁] [CompleteSpace H₁]
+    [NormedAddCommGroup H₂] [InnerProductSpace ℂ H₂] [CompleteSpace H₂]
+    {π₁ : N.algebra B →⋆ₐ[ℂ] (H₁ →L[ℂ] H₁)} {π₂ : N.algebra B →⋆ₐ[ℂ] (H₂ →L[ℂ] H₂)}
+    (h1 : GNS.IsIrreducible π₁) (h2 : GNS.IsIrreducible π₂) :
+    GNS.AreDisjoint π₁ π₂ ∨ GNS.UnitaryEquiv π₁ π₂ :=
+  GNS.areDisjoint_or_unitaryEquiv_of_isIrreducible h1 h2
+
 end HaagKastlerNet
 end HaagKastlerCurved
 end AQFT

Physicslib4/AQFT/HaagKastlerCurved/StabilizerAction.lean

@@ -199,6 +199,51 @@ theorem exists_gns_unitary_stabilizer_strongContinuous [TopologicalSpace M.Isom]
     ω hinv (fun g g' a => N.stabAutHom_mul B g g' a)
     (fun a => N.stabAutHom_one B a) hwc
 
+/-- **Bundled GNS unitary representation of the stabilizer.** The bundled form of
+`exists_gns_unitary_stabilizer`: the implementing unitaries are returned as a
+genuine unitary representation `U : ↥Stab(B) →* (H ≃ₗᵢ[ℂ] H)`, feeding the
+stabilizer group homomorphism `stabAutMonoidHom` into the bundled analytic core
+`GNS.exists_gns_unitaryRep_of_invariant`. -/
+theorem exists_gns_unitaryRep_stabilizer (B : Set M.Carrier)
+    (ω : State (N.algebra B))
+    (hinv : ∀ (g : ↥(MulAction.stabilizer M.Isom B)) (a : N.algebra B),
+        ω (N.stabAutHom B g a) = ω a) :
+    ∃ (H : Type) (_ : NormedAddCommGroup H) (_ : InnerProductSpace ℂ H)
+      (_ : CompleteSpace H) (π : N.algebra B →⋆ₐ[ℂ] (H →L[ℂ] H)) (Ω : H)
+      (U : ↥(MulAction.stabilizer M.Isom B) →* (H ≃ₗᵢ[ℂ] H)),
+        (∀ a : N.algebra B, (ω a : ℂ) = ⟪Ω, π a Ω⟫_ℂ) ∧
+        (∀ (g : ↥(MulAction.stabilizer M.Isom B)) (a : N.algebra B),
+          U g (π a Ω) = π (N.stabAutHom B g a) Ω) ∧
+        (∀ g : ↥(MulAction.stabilizer M.Isom B), U g Ω = Ω) ∧
+        (∀ (g : ↥(MulAction.stabilizer M.Isom B)) (a : N.algebra B) (x : H),
+          U g (π a ((U g).symm x)) = π (N.stabAutHom B g a) x) ∧
+        IsCyclicVector π Ω :=
+  Physicslib4.GNS.exists_gns_unitaryRep_of_invariant (N.stabAutMonoidHom B) ω hinv
+
+/-- **Bundled strongly continuous GNS unitary representation of the stabilizer.**
+The bundled form of `exists_gns_unitary_stabilizer_strongContinuous`: the strongly
+continuous implementing unitaries are returned as a bundled group homomorphism
+`U : ↥Stab(B) →* (H ≃ₗᵢ[ℂ] H)`. -/
+theorem exists_gns_unitaryRep_stabilizer_strongContinuous [TopologicalSpace M.Isom]
+    (B : Set M.Carrier) (ω : State (N.algebra B))
+    (hinv : ∀ (g : ↥(MulAction.stabilizer M.Isom B)) (a : N.algebra B),
+        ω (N.stabAutHom B g a) = ω a)
+    (hwc : ∀ a b : N.algebra B,
+        Continuous fun g : ↥(MulAction.stabilizer M.Isom B) =>
+          (ω (star a * N.stabAutHom B g b) : ℂ)) :
+    ∃ (H : Type) (_ : NormedAddCommGroup H) (_ : InnerProductSpace ℂ H)
+      (_ : CompleteSpace H) (π : N.algebra B →⋆ₐ[ℂ] (H →L[ℂ] H)) (Ω : H)
+      (U : ↥(MulAction.stabilizer M.Isom B) →* (H ≃ₗᵢ[ℂ] H)),
+        (∀ a : N.algebra B, (ω a : ℂ) = ⟪Ω, π a Ω⟫_ℂ) ∧
+        (∀ (g : ↥(MulAction.stabilizer M.Isom B)) (a : N.algebra B),
+          U g (π a Ω) = π (N.stabAutHom B g a) Ω) ∧
+        (∀ g : ↥(MulAction.stabilizer M.Isom B), U g Ω = Ω) ∧
+        (∀ ψ : H, Continuous fun g : ↥(MulAction.stabilizer M.Isom B) => U g ψ) ∧
+        (∀ (g : ↥(MulAction.stabilizer M.Isom B)) (a : N.algebra B) (x : H),
+          U g (π a ((U g).symm x)) = π (N.stabAutHom B g a) x) :=
+  Physicslib4.GNS.exists_gns_unitaryRep_of_invariant_strongContinuous
+    (N.stabAutMonoidHom B) ω hinv hwc
+
 /-- **Irreducible covariant representation of a pure invariant state (curved
 spacetime).** A state `ω` on a local algebra `𝔘(B)` that is invariant under the
 stabilizer action and pure yields a GNS representation that is simultaneously

Physicslib4/GNS/Amplification.lean

@@ -0,0 +1,104 @@
+/-
+Copyright (c) 2026 Lean Community. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Lean Community
+-/
+import Physicslib4.GNS.DirectSum
+
+/-!
+# Amplification and reducibility of direct sums
+
+Two consequences of the direct-sum construction (`Physicslib4.GNS.DirectSum`):
+
+* **Reducibility.** The summand projections lie in the commutant, so if the
+  direct-sum representation is irreducible they must be scalars
+  (`summandProj_isScalar_of_isIrreducible`); consequently a direct sum with two
+  summands carrying nonzero vectors is reducible (`not_isIrreducible_directSum`).
+* **Amplification.** The `ι`-fold amplification `ι · π := ⊕_{ι} π` of a single
+  representation, in which `π` embeds as each summand (`amplification_intertwines_single`).
+
+## The quasi-equivalence `π ~ ι · π`
+
+The quasi-equivalence of a representation with its amplification (`QuasiEquiv π (ι · π)`)
+is **not** proved here. It requires a `*`-isomorphism of the generated von Neumann
+algebras `π(A)'' ≃⋆ₐ (ι·π)(A)''`. The natural map is `T ↦ lpDiag (fun _ ↦ T)`
+(the diagonal), which is an injective `*`-homomorphism carrying `π a ↦ (ι·π) a`;
+but *surjectivity* onto `(ι·π)(A)''` is exactly the amplification commutant theorem
+`(π ⊗ 1)' = π' ⊗ B(K)` (equivalently `(π ⊗ 1)'' = π'' ⊗ ℂ1`), a genuine von Neumann
+algebra result that Mathlib does not currently provide. It is recorded as deferred.
+-/
+
+namespace Physicslib4
+namespace GNS
+
+variable {A : Type*} [CStarAlgebra A]
+variable {ι : Type*} [DecidableEq ι] {H : ι → Type*}
+    [∀ i, NormedAddCommGroup (H i)] [∀ i, InnerProductSpace ℂ (H i)] [∀ i, CompleteSpace (H i)]
+variable (π : ∀ i, A →⋆ₐ[ℂ] (H i →L[ℂ] H i))
+
+/-! ### Reducibility -/
+
+/-- If the direct-sum representation is irreducible, each summand projection is a
+scalar operator (irreducibility means the commutant is trivial). -/
+theorem summandProj_isScalar_of_isIrreducible (hirr : IsIrreducible (directSum π)) (j : ι) :
+    summandProj (H := H) j ∈ scalarOperators (lp H 2) :=
+  isIrreducible_iff_centralizer.mp hirr ▸ summandProj_mem_commutant π j
+
+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. -/
+theorem not_isIrreducible_directSum {j k : ι} (hjk : j ≠ k)
+    {v : H j} (hv : v ≠ 0) {w : H k} (hw : w ≠ 0) :
+    ¬ IsIrreducible (directSum π) := by
+  intro hirr
+  obtain ⟨c, hc⟩ := summandProj_isScalar_of_isIrreducible π hirr j
+  have hjv : lp.single 2 j v ≠ 0 := by
+    rw [← norm_ne_zero_iff, lp.norm_single (by norm_num)]
+    exact norm_ne_zero_iff.mpr hv
+  have hkw : lp.single 2 k w ≠ 0 := by
+    rw [← norm_ne_zero_iff, lp.norm_single (by norm_num)]
+    exact norm_ne_zero_iff.mpr hw
+  have e1 := DFunLike.congr_fun hc (lp.single 2 j v)
+  have e2 := DFunLike.congr_fun hc (lp.single 2 k w)
+  simp only [summandProj_apply, ContinuousLinearMap.smul_apply, ContinuousLinearMap.one_apply,
+    lp.single_apply_self] at e1
+  simp only [summandProj_apply, lp.single_apply_ne 2 k w hjk, lp.single_zero,
+    ContinuousLinearMap.smul_apply, ContinuousLinearMap.one_apply] at e2
+  have hc1 : c = 1 := by
+    have h0 : (1 - c) • lp.single 2 j v = 0 := by rw [sub_smul, one_smul, ← e1, sub_self]
+    rcases smul_eq_zero.mp h0 with h | h
+    · exact (sub_eq_zero.mp h).symm
+    · exact absurd h hjv
+  have hc0 : c = 0 := by
+    rcases smul_eq_zero.mp e2.symm with h | h
+    · exact h
+    · exact absurd h hkw
+  rw [hc1] at hc0
+  exact one_ne_zero hc0
+
+end GNS
+
+/-! ### Amplification -/
+
+namespace GNS
+
+variable {A : Type*} [CStarAlgebra A]
+variable {H₀ : Type*} [NormedAddCommGroup H₀] [InnerProductSpace ℂ H₀] [CompleteSpace H₀]
+variable {ι : Type*} [DecidableEq ι]
+variable (π : A →⋆ₐ[ℂ] (H₀ →L[ℂ] H₀))
+
+/-- The `ι`-fold **amplification** `ι · π := ⊕_{i : ι} π` of a representation, on the
+ℓ²-direct sum of `ι` copies of `H₀`. -/
+noncomputable def amplification :
+    A →⋆ₐ[ℂ] (lp (fun _ : ι => H₀) 2 →L[ℂ] lp (fun _ : ι => H₀) 2) :=
+  directSum (fun _ : ι => π)
+
+/-- In the amplification, `π` embeds as each summand: the isometric inclusion of the
+`j`-th copy `H₀ ↪ ℓ²(ι, H₀)` intertwines `π` with `ι · π`. -/
+theorem amplification_intertwines_single (j : ι) :
+    Intertwines π (amplification (ι := ι) π)
+      (lp.singleContinuousLinearMap ℂ (fun _ : ι => H₀) 2 j) :=
+  intertwines_single (fun _ : ι => π) j
+
+end GNS
+end Physicslib4