diff --git a/CHANGELOG.md b/CHANGELOG.md index 54df7f7..c4dd5a3 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -8,6 +8,13 @@ file is where its history lives. The first release, 1.0, is in preparation. +- The blueprint has a section on the Reeh–Schlieder theorem (§10.9): a main theorem with no additivity + hypothesis, and corollaries under cyclicity for the translation-generated algebras, the von Neumann + form of weak additivity, and weak additivity. All of it is formalized and proved in Lean + (`Physicslib4/AQFT/HaagKastler/ReehSchlieder/`, with the analytic lemmas in + `Physicslib4/AQFT/PositiveEnergyHolomorphic.lean` and `Physicslib4/Analysis/EdgeVanishing.lean`), + and the reference manual has a chapter on it. + - The website has About, Roadmap and Get Involved pages, and the header on every page links to them. - The Jekyll home page is retired: the Verso website is served at the root, with redirects from the diff --git a/Physicslib4.lean b/Physicslib4.lean index fb4324c..aeea6f2 100644 --- a/Physicslib4.lean +++ b/Physicslib4.lean @@ -17,6 +17,10 @@ import Physicslib4.AQFT.HaagKastler.QuasilocalExistence import Physicslib4.AQFT.HaagKastler.QuasilocalIntertwiner import Physicslib4.AQFT.HaagKastler.QuasilocalKMS import Physicslib4.AQFT.HaagKastler.QuasilocalObservable +import Physicslib4.AQFT.HaagKastler.ReehSchlieder.Additivity +import Physicslib4.AQFT.HaagKastler.ReehSchlieder.Correlations +import Physicslib4.AQFT.HaagKastler.ReehSchlieder.CyclicSubspace +import Physicslib4.AQFT.HaagKastler.ReehSchlieder.Translations import Physicslib4.AQFT.HaagKastler.StrongDensity import Physicslib4.AQFT.HaagKastler.VacuumState import Physicslib4.AQFT.HaagKastlerCurved.Concrete @@ -38,8 +42,10 @@ import Physicslib4.AQFT.HaagKastlerCurved.StabilizerAction import Physicslib4.AQFT.HaagKastlerCurved.StabilizerKMS import Physicslib4.AQFT.KMS import Physicslib4.AQFT.PositiveEnergy +import Physicslib4.AQFT.PositiveEnergyHolomorphic import Physicslib4.Analysis.CStarCompletion import Physicslib4.Analysis.CStarDenseExtend +import Physicslib4.Analysis.EdgeVanishing import Physicslib4.Analysis.HorizontalLineRemovable import Physicslib4.Analysis.StripPeriodicExtension import Physicslib4.Analysis.StrongContinuity diff --git a/Physicslib4/AQFT/HaagKastler/ReehSchlieder/Additivity.lean b/Physicslib4/AQFT/HaagKastler/ReehSchlieder/Additivity.lean new file mode 100644 index 0000000..a0c8195 --- /dev/null +++ b/Physicslib4/AQFT/HaagKastler/ReehSchlieder/Additivity.lean @@ -0,0 +1,324 @@ +/- +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.AQFT.HaagKastler.ReehSchlieder.Correlations +import Physicslib4.AQFT.HaagKastler.LocalVonNeumann +import Physicslib4.Operators.DensityTheorem + +/-! +# Weak additivity and the Reeh–Schlieder theorem + +For a diamond `B`, the translation-generated algebra `𝔄_B` is the norm closure of the +`*`-subalgebra of the quasilocal algebra `𝔘` generated by the translates +`ι_{B + x}(𝔘(B + x))`, `x ∈ ℝ⁴`, where `B + x = translationSub x • B`. The net is weakly additive +when `𝔄_B = 𝔘` for every nonempty diamond `B`. + +The covariant setting is that of `Correlations.lean`: a `*`-representation `π` of `𝔘` on `H`, a +vector `Ω`, unitaries `U(x)` indexed by `ℝ⁴` with `U(x)π(a)Ω = π(β_x a)Ω`, and positive energy of +every future-timelike translation subgroup `t ↦ U(t n)`. A vector `Ω` is cyclic for a set `S` of +operators when `{T Ω | T ∈ S}` is dense; for the local algebra this is +`Dense ((fun T => T Ω) '' N.localOperators π hB)`, and for `π(𝔄_B)` it is +`Dense (Set.range fun a : N.translationGeneratedAlgebra hB => π a Ω)`. The commutant is +`Set.centralizer` in `H →L[ℂ] H`, as in `LocalVonNeumann.lean`. + +* `HaagKastlerNet.translationGeneratedAlgebra` — the algebra `𝔄_B`. +* `HaagKastlerNet.IsWeaklyAdditive` — weak additivity. +* `HaagKastlerNet.IsWeaklyAdditiveVonNeumann` — weak additivity in the von Neumann sense. +* `reeh_schlieder` — `π(𝔄_{B₁})Ω` lies in the closure of `π(𝔘(B))Ω`. +* `reeh_schlieder_cyclic`, `reeh_schlieder_cyclic_of_vonNeumann`, + `reeh_schlieder_cyclic_of_weaklyAdditive`, `reeh_schlieder_cyclic_of_vacuum`, + `reeh_schlieder_separating` — the corollaries. +-/ + +namespace Physicslib4 +namespace AQFT +namespace HaagKastler + +open scoped InnerProductSpace Pointwise +open Spacetime + +variable {H : Type*} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] + +/-- The translation-generated algebra `𝔄_B` of a diamond `B`: the C*-subalgebra of the +quasilocal algebra generated by the translates `ι_{B + x}(𝔘(B + x))`, `x ∈ ℝ⁴`, that is, the norm +closure of the `*`-subalgebra they generate. Here `B + x = translationSub x • B`. + +Blueprint: def:translation-generated-algebra -/ +noncomputable def HaagKastlerNet.translationGeneratedAlgebra (N : HaagKastlerNet) + {B : Set StandardMinkowskiSpacetime.Carrier} (hB : IsAlexandrovBasisSet B) : + StarSubalgebra ℂ N.quasilocal.carrier := + StarSubalgebra.topologicalClosure <| StarAlgebra.adjoin ℂ <| + ⋃ x : StandardMinkowskiSpacetime.Carrier, + Set.range (N.quasilocal.ι (isAlexandrovBasisSet_smul (translationSub x) hB)) + +/-- A Haag–Kastler net is weakly additive if the translation-generated algebra `𝔄_B` is the +whole quasilocal algebra for every nonempty diamond `B`. + +Blueprint: def:weak-additivity -/ +def HaagKastlerNet.IsWeaklyAdditive (N : HaagKastlerNet) : Prop := + ∀ ⦃B : Set StandardMinkowskiSpacetime.Carrier⦄ (hB : IsAlexandrovBasisSet B), B.Nonempty → + N.translationGeneratedAlgebra hB = ⊤ + +/-- A `*`-representation `π` of the quasilocal algebra satisfies weak additivity in the von +Neumann sense if `π(𝔘) ⊆ π(𝔄_B)''` for every nonempty diamond `B`, the commutant being taken in +the bounded operators on `H` (`Set.centralizer`). + +Blueprint: def:weak-additivity-von-neumann -/ +def HaagKastlerNet.IsWeaklyAdditiveVonNeumann (N : HaagKastlerNet) + (π : N.quasilocal.carrier →⋆ₐ[ℂ] (H →L[ℂ] H)) : Prop := + ∀ ⦃B : Set StandardMinkowskiSpacetime.Carrier⦄ (hB : IsAlexandrovBasisSet B), B.Nonempty → + Set.range π ⊆ + Set.centralizer (Set.centralizer (Set.range fun a : N.translationGeneratedAlgebra hB => π a)) + +/-- If the net is weakly additive, every `*`-representation of the quasilocal algebra satisfies +weak additivity in the von Neumann sense. + +Blueprint: lmm:weak-additivity-von-neumann -/ +theorem HaagKastlerNet.IsWeaklyAdditive.isWeaklyAdditiveVonNeumann {N : HaagKastlerNet} + (hN : N.IsWeaklyAdditive) (π : N.quasilocal.carrier →⋆ₐ[ℂ] (H →L[ℂ] H)) : + N.IsWeaklyAdditiveVonNeumann π := by + intro B hB hne + refine subset_trans ?_ Set.subset_centralizer_centralizer + rintro _ ⟨c, rfl⟩ + exact ⟨⟨c, by rw [hN hB hne]; trivial⟩, rfl⟩ + +/-- **Orthogonality on the generated `*`-algebra.** In the setting of +`inner_translated_products_eq_zero`, `ψ` is orthogonal to `π(P)Ω` for every `P` in the +`*`-algebra generated by the translates `ι_{B₁ + y}(𝔘(B₁ + y))`, `y ∈ ℝ⁴`. + +The binder groups are the covariant setting (`π`, `Ω`, `U`, `hU`), positive energy (`hpos`), the +diamonds with the translation condition (`hB₁`, `hB`, `hB₁B`), and the vector `ψ` with its +orthogonality `hψ`. + +Blueprint: lmm:reeh-schlieder-star-algebra-orthogonal -/ +theorem inner_adjoin_translates_eq_zero {N : HaagKastlerNet} + (π : N.quasilocal.carrier →⋆ₐ[ℂ] (H →L[ℂ] H)) (Ω : H) + (U : StandardMinkowskiSpacetime.Carrier → (H ≃ₗᵢ[ℂ] H)) + (hU : ∀ x a, U x (π a Ω) = π (N.action (translationSub x) a) Ω) + (hpos : ∀ n : StandardMinkowskiSpacetime.Carrier, + (n : SpacetimeModel) ∈ minkowskiForwardCone 0 → IsPositiveEnergy (fun t : ℝ => U (t • n))) + {B₁ B : Set StandardMinkowskiSpacetime.Carrier} + (hB₁ : IsAlexandrovBasisSet B₁) (hB : IsAlexandrovBasisSet B) + (hB₁B : ∀ᶠ x in nhds 0, translationSub x • B₁ ⊆ B) + {ψ : H} (hψ : ∀ b : N.U.algebra B, ⟪ψ, π (N.quasilocal.ι hB b) Ω⟫_ℂ = 0) : + ∀ P ∈ StarAlgebra.adjoin ℂ + (⋃ y : StandardMinkowskiSpacetime.Carrier, + Set.range (N.quasilocal.ι (isAlexandrovBasisSet_smul (translationSub y) hB₁))), + ⟪ψ, π P Ω⟫_ℂ = 0 := by + set S := ⋃ y : StandardMinkowskiSpacetime.Carrier, + Set.range (N.quasilocal.ι (isAlexandrovBasisSet_smul (translationSub y) hB₁)) with hS + have hstar : star S ⊆ S := by + intro x hx + obtain ⟨y, b, hb⟩ := Set.mem_iUnion.1 (Set.mem_star.1 hx) + exact Set.mem_iUnion.2 ⟨y, star b, by rw [map_star, hb, star_star]⟩ + have hgen : ∀ g ∈ S, ∃ y a, N.action (translationSub y) (N.quasilocal.ι hB₁ a) = g := by + intro g hg + obtain ⟨y, hy⟩ := Set.mem_iUnion.1 hg + rw [← (action_translationSub_image_range_ι N hB₁ hB y).1] at hy + obtain ⟨_, ⟨a, rfl⟩, h⟩ := hy + exact ⟨y, a, h⟩ + have hmon : ∀ m ∈ Submonoid.closure S, ⟪ψ, π m Ω⟫_ℂ = 0 := by + intro m hm + obtain ⟨l, hl, rfl⟩ := Submonoid.exists_list_of_mem_closure hm + choose y a hya using fun i : Fin l.length => hgen _ (hl _ (List.get_mem l i)) + have : l = List.ofFn fun i => N.action (translationSub (y i)) (N.quasilocal.ι hB₁ (a i)) := by + conv_lhs => rw [← List.ofFn_get l] + exact congrArg _ (funext fun i => (hya i).symm) + rw [this] + exact inner_monomial_eq_zero π Ω U hU hpos hB₁ hB hB₁B hψ a y + intro P hP + have hP' : P ∈ Subalgebra.toSubmodule (Algebra.adjoin ℂ S) := by + have h : P ∈ (StarAlgebra.adjoin ℂ S).toSubalgebra := hP + rwa [StarAlgebra.adjoin_toSubalgebra, Set.union_eq_left.2 hstar] at h + rw [Algebra.adjoin_eq_span] at hP' + clear hP + induction hP' using Submodule.span_induction with + | mem x hx => exact hmon x hx + | zero => simp + | add x y _ _ hx hy => rw [map_add, add_apply, inner_add_right, hx, hy, add_zero] + | smul c x _ hx => rw [map_smul, smul_apply, inner_smul_right, hx, mul_zero] + +/-- **Bicommutant orbit closure.** For a `*`-representation `π` of the quasilocal algebra on `H`, +`Ω ∈ H` and a diamond `B`, every `T ∈ π(𝔄_B)''` maps `Ω` into the closure of `π(𝔄_B)Ω`. This is +`apply_mem_closure_of_mem_bicommutant` for the restriction of `π` to `𝔄_B`. + +Blueprint: lmm:bicommutant-orbit-closure -/ +theorem apply_mem_closure_translationGeneratedAlgebra {N : HaagKastlerNet} + (π : N.quasilocal.carrier →⋆ₐ[ℂ] (H →L[ℂ] H)) (Ω : H) + {B : Set StandardMinkowskiSpacetime.Carrier} (hB : IsAlexandrovBasisSet B) {T : H →L[ℂ] H} + (hT : T ∈ Set.centralizer + (Set.centralizer (Set.range fun a : N.translationGeneratedAlgebra hB => π a))) : + T Ω ∈ closure (Set.range fun a : N.translationGeneratedAlgebra hB => π a Ω) := by + exact apply_mem_closure_of_mem_bicommutant (π.comp (N.translationGeneratedAlgebra hB).subtype) + (T := T) hT Ω + +/-- **Reeh–Schlieder theorem.** Let `π` be a `*`-representation of the quasilocal algebra on `H`, +`Ω ∈ H`, and `U(x)` unitaries with `U(x)π(a)Ω = π(β_x a)Ω`, such that every future-timelike +translation subgroup `t ↦ U(t n)` has positive energy. Let `B₁, B` be diamonds with +`B₁ + x ⊆ B` for every `x` near `0`. Then `π(𝔄_{B₁})Ω` lies in the closure of `π(𝔘(B))Ω`. + +The binder groups are the covariant setting (`π`, `Ω`, `U`, `hU`), positive energy (`hpos`), and +the diamonds with the translation condition (`hB₁`, `hB`, `hB₁B`). + +Blueprint: thrm:reeh-schlieder -/ +theorem reeh_schlieder {N : HaagKastlerNet} + (π : N.quasilocal.carrier →⋆ₐ[ℂ] (H →L[ℂ] H)) (Ω : H) + (U : StandardMinkowskiSpacetime.Carrier → (H ≃ₗᵢ[ℂ] H)) + (hU : ∀ x a, U x (π a Ω) = π (N.action (translationSub x) a) Ω) + (hpos : ∀ n : StandardMinkowskiSpacetime.Carrier, + (n : SpacetimeModel) ∈ minkowskiForwardCone 0 → IsPositiveEnergy (fun t : ℝ => U (t • n))) + {B₁ B : Set StandardMinkowskiSpacetime.Carrier} + (hB₁ : IsAlexandrovBasisSet B₁) (hB : IsAlexandrovBasisSet B) + (hB₁B : ∀ᶠ x in nhds 0, translationSub x • B₁ ⊆ B) : + ∀ A ∈ N.translationGeneratedAlgebra hB₁, + π A Ω ∈ closure (Set.range fun b : N.U.algebra B => π (N.quasilocal.ι hB b) Ω) := by + intro A hA + let M : Submodule ℂ H := LinearMap.range + ((ContinuousLinearMap.apply ℂ H Ω).toLinearMap ∘ₗ + (π.comp (N.quasilocal.ι hB)).toAlgHom.toLinearMap) + have hM : closure (Set.range fun b : N.U.algebra B => π (N.quasilocal.ι hB b) Ω) = + (Mᗮᗮ : Set H) := by + rw [Submodule.orthogonal_orthogonal_eq_closure, Submodule.topologicalClosure_coe]; rfl + rw [hM] + refine (Submodule.mem_orthogonal' _ _).2 fun ψ hψ => ?_ + have hψ' : ∀ b : N.U.algebra B, ⟪ψ, π (N.quasilocal.ι hB b) Ω⟫_ℂ = 0 := fun b => + (Submodule.mem_orthogonal' _ _).1 hψ _ ⟨b, rfl⟩ + have := NonUnitalStarAlgHom.instContinuousLinearMapClassComplex + (F := N.quasilocal.carrier →⋆ₐ[ℂ] (H →L[ℂ] H)) + have hcl : IsClosed {P : N.quasilocal.carrier | ⟪ψ, π P Ω⟫_ℂ = 0} := + isClosed_eq (continuous_const.inner + ((continuous_eval_const Ω).comp (map_continuous π))) continuous_const + have hsub := closure_minimal (fun P hP => inner_adjoin_translates_eq_zero π Ω U hU hpos hB₁ hB + hB₁B hψ' P hP) hcl + have : A ∈ closure (StarAlgebra.adjoin ℂ (⋃ y : StandardMinkowskiSpacetime.Carrier, + Set.range (N.quasilocal.ι (isAlexandrovBasisSet_smul (translationSub y) hB₁))) : + Set N.quasilocal.carrier) := by + rw [← StarSubalgebra.topologicalClosure_coe]; exact hA + exact inner_eq_zero_symm.1 (hsub this) + +/-- **Reeh–Schlieder, cyclic form.** In the setting of `reeh_schlieder`, if `Ω` is cyclic for +`π(𝔄_{B'})` for every nonempty diamond `B'`, then `Ω` is cyclic for `π(𝔘(B))` for every nonempty +diamond `B`. + +The binder groups are the covariant setting (`π`, `Ω`, `U`, `hU`), positive energy (`hpos`), the +cyclicity hypothesis `hcyc`, and the nonempty diamond (`hB`, `hne`). + +Blueprint: crllr:reeh-schlieder-cyclic -/ +theorem reeh_schlieder_cyclic {N : HaagKastlerNet} + (π : N.quasilocal.carrier →⋆ₐ[ℂ] (H →L[ℂ] H)) (Ω : H) + (U : StandardMinkowskiSpacetime.Carrier → (H ≃ₗᵢ[ℂ] H)) + (hU : ∀ x a, U x (π a Ω) = π (N.action (translationSub x) a) Ω) + (hpos : ∀ n : StandardMinkowskiSpacetime.Carrier, + (n : SpacetimeModel) ∈ minkowskiForwardCone 0 → IsPositiveEnergy (fun t : ℝ => U (t • n))) + (hcyc : ∀ ⦃B' : Set StandardMinkowskiSpacetime.Carrier⦄ (hB' : IsAlexandrovBasisSet B'), + B'.Nonempty → Dense (Set.range fun a : N.translationGeneratedAlgebra hB' => π a Ω)) + {B : Set StandardMinkowskiSpacetime.Carrier} (hB : IsAlexandrovBasisSet B) + (hne : B.Nonempty) : + Dense ((fun T => T Ω) '' N.localOperators π hB) := by + obtain ⟨B₁, hB₁, hne₁, V, hV, h0, hVB⟩ := exists_diamond_translate_subset hB hne + have key := reeh_schlieder π Ω U hU hpos hB₁ hB (Filter.eventually_of_mem (hV.mem_nhds h0) hVB) + have himg : (fun T => T Ω) '' N.localOperators π hB = + Set.range fun b : N.U.algebra B => π (N.quasilocal.ι hB b) Ω := + (Set.range_comp _ _).symm + rw [himg, ← dense_closure] + refine (hcyc hB₁ hne₁).mono ?_ + rintro _ ⟨a, rfl⟩ + exact key a a.2 + +/-- **Reeh–Schlieder under von Neumann weak additivity.** In the setting of `reeh_schlieder`, if +`π` satisfies weak additivity in the von Neumann sense and `Ω` is cyclic for `π(𝔘)`, then `Ω` is +cyclic for `π(𝔘(B))` for every nonempty diamond `B`. + +Blueprint: crllr:reeh-schlieder-von-neumann -/ +theorem reeh_schlieder_cyclic_of_vonNeumann {N : HaagKastlerNet} + (π : N.quasilocal.carrier →⋆ₐ[ℂ] (H →L[ℂ] H)) (Ω : H) + (U : StandardMinkowskiSpacetime.Carrier → (H ≃ₗᵢ[ℂ] H)) + (hU : ∀ x a, U x (π a Ω) = π (N.action (translationSub x) a) Ω) + (hpos : ∀ n : StandardMinkowskiSpacetime.Carrier, + (n : SpacetimeModel) ∈ minkowskiForwardCone 0 → IsPositiveEnergy (fun t : ℝ => U (t • n))) + (hwa : N.IsWeaklyAdditiveVonNeumann π) (hcyc : GNS.IsCyclicVector π Ω) + {B : Set StandardMinkowskiSpacetime.Carrier} (hB : IsAlexandrovBasisSet B) + (hne : B.Nonempty) : + Dense ((fun T => T Ω) '' N.localOperators π hB) := by + refine reeh_schlieder_cyclic π Ω U hU hpos (fun B' hB' hne' => ?_) hB hne + rw [← dense_closure] + refine Dense.mono ?_ (hcyc : Dense (Set.range fun a => π a Ω)) + rintro _ ⟨c, rfl⟩ + exact apply_mem_closure_translationGeneratedAlgebra π Ω hB' (hwa hB' hne' ⟨c, rfl⟩) + +/-- **Reeh–Schlieder under weak additivity.** In the setting of `reeh_schlieder`, if the net is +weakly additive and `Ω` is cyclic for `π(𝔘)`, then `Ω` is cyclic for `π(𝔘(B))` for every +nonempty diamond `B`. + +Blueprint: crllr:reeh-schlieder-weak-additivity -/ +theorem reeh_schlieder_cyclic_of_weaklyAdditive {N : HaagKastlerNet} + (π : N.quasilocal.carrier →⋆ₐ[ℂ] (H →L[ℂ] H)) (Ω : H) + (U : StandardMinkowskiSpacetime.Carrier → (H ≃ₗᵢ[ℂ] H)) + (hU : ∀ x a, U x (π a Ω) = π (N.action (translationSub x) a) Ω) + (hpos : ∀ n : StandardMinkowskiSpacetime.Carrier, + (n : SpacetimeModel) ∈ minkowskiForwardCone 0 → IsPositiveEnergy (fun t : ℝ => U (t • n))) + (hwa : N.IsWeaklyAdditive) (hcyc : GNS.IsCyclicVector π Ω) + {B : Set StandardMinkowskiSpacetime.Carrier} (hB : IsAlexandrovBasisSet B) + (hne : B.Nonempty) : + Dense ((fun T => T Ω) '' N.localOperators π hB) := + reeh_schlieder_cyclic_of_vonNeumann π Ω U hU hpos (hwa.isWeaklyAdditiveVonNeumann π) hcyc hB hne + +/-- **Reeh–Schlieder for a vacuum state.** Let the net be weakly additive, and let `(π, Ω, U)` +satisfy the implementation and spectrum conditions of a vacuum state (`IsVacuumStateConcrete`): the +unitaries `U(L)` implement the Poincaré action on `π(𝔘)Ω`, and `t ↦ U(γ(t))` has positive energy +for every future-timelike translation subgroup `γ`. If `Ω` is cyclic for `π(𝔘)`, then `Ω` is +cyclic for `π(𝔘(B))` for every nonempty diamond `B`. + +The hypotheses mirror the implementation and spectrum conjuncts of the existential in +`IsVacuumState`, so the statement applies to the witnessing data of every vacuum state; the state +itself and the condition that `π` reproduces it are not needed. + +Blueprint: crllr:reeh-schlieder-vacuum -/ +theorem reeh_schlieder_cyclic_of_vacuum {N : HaagKastlerNet} (hwa : N.IsWeaklyAdditive) + (π : N.quasilocal.carrier →⋆ₐ[ℂ] (H →L[ℂ] H)) (Ω : H) + (U : InhomogeneousLorentzGroup → (H ≃ₗᵢ[ℂ] H)) + (hU : ∀ (L : InhomogeneousLorentzGroup) (a : N.quasilocal.carrier), + U L (π a Ω) = π (N.action L a) Ω) + (hpos : ∀ γ : ℝ → InhomogeneousLorentzGroup, + IsOneParameterSubgroup γ → IsFutureTimelikeTranslation γ → + IsPositiveEnergy (fun t => U (γ t))) + (hcyc : GNS.IsCyclicVector π Ω) + {B : Set StandardMinkowskiSpacetime.Carrier} (hB : IsAlexandrovBasisSet B) + (hne : B.Nonempty) : + Dense ((fun T => T Ω) '' N.localOperators π hB) := + reeh_schlieder_cyclic_of_weaklyAdditive π Ω (fun x => U (translationSub x)) + (fun x a => hU (translationSub x) a) + (fun n hn => hpos (translationFlow n) (isOneParameterSubgroup_translationFlow n) ⟨n, hn, rfl⟩) + hwa hcyc hB hne + +/-- **Reeh–Schlieder, separating form.** In the setting of `reeh_schlieder_cyclic`, `Ω` is +separating for the local von Neumann algebra `R(C)` of every diamond `C` completely spacelike to +some nonempty diamond `B`: every `R ∈ R(C)` with `R Ω = 0` is zero. + +The binder groups are the covariant setting (`π`, `Ω`, `U`, `hU`), positive energy (`hpos`), the +cyclicity hypothesis `hcyc`, the nonempty diamond (`hB`, `hne`), the diamond `C` with its spacelike +separation (`hC`, `hs`), and the operator `R` with `hR`, `hRΩ`. + +Blueprint: crllr:reeh-schlieder-separating -/ +theorem reeh_schlieder_separating {N : HaagKastlerNet} + (π : N.quasilocal.carrier →⋆ₐ[ℂ] (H →L[ℂ] H)) (Ω : H) + (U : StandardMinkowskiSpacetime.Carrier → (H ≃ₗᵢ[ℂ] H)) + (hU : ∀ x a, U x (π a Ω) = π (N.action (translationSub x) a) Ω) + (hpos : ∀ n : StandardMinkowskiSpacetime.Carrier, + (n : SpacetimeModel) ∈ minkowskiForwardCone 0 → IsPositiveEnergy (fun t : ℝ => U (t • n))) + (hcyc : ∀ ⦃B' : Set StandardMinkowskiSpacetime.Carrier⦄ (hB' : IsAlexandrovBasisSet B'), + B'.Nonempty → Dense (Set.range fun a : N.translationGeneratedAlgebra hB' => π a Ω)) + {B C : Set StandardMinkowskiSpacetime.Carrier} (hB : IsAlexandrovBasisSet B) + (hne : B.Nonempty) (hC : IsAlexandrovBasisSet C) + (hs : Spacetime.IsCompletelySpacelike StandardMinkowskiSpacetime + standardMinkowskiTimeOrientation B C) + {R : H →L[ℂ] H} (hR : R ∈ N.localVonNeumannAlgebra π hC) (hRΩ : R Ω = 0) : + R = 0 := + N.localVonNeumannAlgebra_separating π hB hC hs + (reeh_schlieder_cyclic π Ω U hU hpos hcyc hB hne) hR hRΩ + +end HaagKastler +end AQFT +end Physicslib4 diff --git a/Physicslib4/AQFT/HaagKastler/ReehSchlieder/Correlations.lean b/Physicslib4/AQFT/HaagKastler/ReehSchlieder/Correlations.lean new file mode 100644 index 0000000..8c4d591 --- /dev/null +++ b/Physicslib4/AQFT/HaagKastler/ReehSchlieder/Correlations.lean @@ -0,0 +1,296 @@ +/- +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.AQFT.HaagKastler.ReehSchlieder.CyclicSubspace + +/-! +# Correlation functions in the Reeh–Schlieder argument + +Let `π` be a `*`-representation of the quasilocal algebra `𝔘` on `H`, `Ω ∈ H`, and `x ↦ U(x)` +unitaries indexed by the translations `ℝ⁴` with `U(x)π(a)Ω = π(β_x a)Ω`, where +`β_x = N.action (translationSub x)`. The local algebra of a diamond `B` inside `𝔘` is +`Set.range (N.quasilocal.ι hB)`. + +For `a : Fin n → N.U.algebra B₁` and `ξ : Fin n → ℝ⁴` the ordered product +`U(ξ₁)π(a₁)U(ξ₂)π(a₂) ⋯ U(ξₙ)π(aₙ)` is written +`(List.ofFn fun i => (U (ξ i) : H →L[ℂ] H) * π (N.quasilocal.ι hB₁ (a i))).prod`; the empty +product is the identity. The partial sum `x_k = ξ₁ + ⋯ + ξ_k` at index `i : Fin n` is +`∑ j : Fin (i + 1), ξ (Fin.castLE i.isLt j)`, a sum of the shape used by +`exists_isOpen_sum_mem_of_mem_nhds`. The cyclic subspace `K₀` is +`(Submodule.span ℂ (Set.range fun a => π a Ω)).topologicalClosure`, as in `CyclicSubspace.lean`. + +* `action_translationSub_image_range_ι` — translates of a local subalgebra. +* `translated_products_apply` — `U(ξ₁)π(a₁) ⋯ U(ξₙ)π(aₙ)Ω = π(β_{x₁}a₁ ⋯ β_{xₙ}aₙ)Ω`. +* `inner_translated_products_eq_zero_of_mem` — the correlation function vanishes near the origin. +* `inner_translated_products_update_eq_inner` — factorization in one variable. +* `inner_translated_products_eq_zero` — the correlation function vanishes identically. +* `inner_monomial_eq_zero` — orthogonality on monomials of translated local elements. +-/ + +namespace Physicslib4 +namespace AQFT +namespace HaagKastler + +open scoped InnerProductSpace Pointwise +open Spacetime + +variable {H : Type*} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] + +/-- **Translates of a local subalgebra.** For diamonds `B₁, B` and `x ∈ ℝ⁴`, +`β_x ι_{B₁}(𝔘(B₁)) = ι_{B₁ + x}(𝔘(B₁ + x))`, and if `B₁ + x ⊆ B` this set is contained in +`ι_B(𝔘(B))`. Here `B₁ + x = translationSub x • B₁`. + +Blueprint: lmm:translate-local-subalgebra -/ +theorem action_translationSub_image_range_ι (N : HaagKastlerNet) + {B₁ B : Set StandardMinkowskiSpacetime.Carrier} + (hB₁ : IsAlexandrovBasisSet B₁) (hB : IsAlexandrovBasisSet B) + (x : StandardMinkowskiSpacetime.Carrier) : + N.action (translationSub x) '' Set.range (N.quasilocal.ι hB₁) = + Set.range (N.quasilocal.ι (isAlexandrovBasisSet_smul (translationSub x) hB₁)) ∧ + (translationSub x • B₁ ⊆ B → + N.action (translationSub x) '' Set.range (N.quasilocal.ι hB₁) ⊆ + Set.range (N.quasilocal.ι hB)) := by + have h₁ : N.action (translationSub x) '' Set.range (N.quasilocal.ι hB₁) = + Set.range (N.quasilocal.ι (isAlexandrovBasisSet_smul (translationSub x) hB₁)) := by + ext y + constructor + · rintro ⟨_, ⟨a, rfl⟩, rfl⟩ + exact ⟨N.covEquiv _ _ a, (N.action_ι _ hB₁ a).symm⟩ + · rintro ⟨b, rfl⟩ + obtain ⟨a, rfl⟩ := (N.covEquiv (translationSub x) B₁).surjective b + exact ⟨_, ⟨a, rfl⟩, N.action_ι _ hB₁ a⟩ + refine ⟨h₁, fun h => ?_⟩ + rw [h₁] + rintro _ ⟨a, rfl⟩ + exact ⟨_, N.quasilocal.ι_inclusion _ hB h a⟩ + +/-- **Translated products.** If `U(x)π(a)Ω = π(β_x a)Ω` for all `x` and `a`, then for +`a₁, …, aₙ ∈ 𝔘` and `ξ₁, …, ξₙ ∈ ℝ⁴`, +`U(ξ₁)π(a₁)U(ξ₂)π(a₂) ⋯ U(ξₙ)π(aₙ)Ω = π(β_{x₁}a₁ β_{x₂}a₂ ⋯ β_{xₙ}aₙ)Ω` with +`x_k = ξ₁ + ⋯ + ξ_k`. For `n = 0` both sides are `Ω`. + +Blueprint: lmm:reeh-schlieder-translated-products -/ +theorem translated_products_apply {N : HaagKastlerNet} + (π : N.quasilocal.carrier →⋆ₐ[ℂ] (H →L[ℂ] H)) (Ω : H) + (U : StandardMinkowskiSpacetime.Carrier → (H ≃ₗᵢ[ℂ] H)) + (hU : ∀ x a, U x (π a Ω) = π (N.action (translationSub x) a) Ω) + {n : ℕ} (a : Fin n → N.quasilocal.carrier) (ξ : Fin n → StandardMinkowskiSpacetime.Carrier) : + (List.ofFn fun i => (U (ξ i) : H →L[ℂ] H) * π (a i)).prod Ω = + π ((List.ofFn fun i : Fin n => + N.action (translationSub (∑ j : Fin (i + 1), ξ (Fin.castLE i.isLt j))) (a i)).prod) Ω := by + induction n with + | zero => simp + | succ n ih => + have hsum : ∀ i : Fin n, (∑ j : Fin (i.succ + 1), ξ (Fin.castLE i.succ.isLt j)) = + ξ 0 + ∑ j : Fin (i + 1), ξ (Fin.castLE i.isLt j).succ := by + intro i + exact Fin.sum_univ_succ (fun j : Fin (i + 1 + 1) => ξ (Fin.castLE i.succ.isLt j)) + have key : ∀ b c, π b (π c Ω) = π (b * c) Ω := fun b c => by rw [map_mul]; rfl + rw [List.ofFn_succ, List.prod_cons, List.ofFn_succ, List.prod_cons, map_mul] + refine Eq.trans (congrArg (fun v => U (ξ 0) (π (a 0) v)) + (ih (fun i => a i.succ) (fun i => ξ i.succ))) ?_ + refine Eq.trans (congrArg (fun v => U (ξ 0) v) (key _ _)) ?_ + rw [hU, ← map_mul π, map_mul, map_list_prod, List.map_ofFn] + congr 3 + · exact congrArg (fun x => N.action (translationSub x) (a 0)) (Fin.sum_univ_one + (fun j : Fin 1 => ξ (Fin.castLE (Fin.isLt (0 : Fin (n + 1))) j))).symm + · refine congrArg (fun f => (List.ofFn f).prod) (funext fun i => ?_) + rw [Function.comp_apply, hsum i, translationSub_mul, HaagKastlerNet.action_mul_apply] + +/-- **Vanishing near the origin.** Let `π`, `Ω`, `U` be as in +`covariant_translations_cyclicSubspace`. Let `B₁, B` be diamonds, let `ψ ⊥ π(𝔘(B))Ω`, and +`a₁, …, aₙ ∈ 𝔘(B₁)`. If `B₁ + (ξ₁ + ⋯ + ξₖ) ⊆ B` for every partial sum of at most `n` elements of +`V₀`, then `F(ξ) = ⟨ψ, U(ξ₁)π(a₁) ⋯ U(ξₙ)π(aₙ)Ω⟩ = 0` whenever `ξ₁, …, ξₙ ∈ V₀`. + +The blueprint's open neighbourhood `V` of `0` with `B₁ + x ⊆ B` for `x ∈ V`, and the choice of +`V₀` with partial sums in `V`, are composed into the single hypothesis `hV₀`; openness of `V` and +`V₀` is not used. The binder groups are the covariant setting (`π`, `Ω`, `U`, `hU`), the diamonds +with the translation condition (`hB₁`, `hB`, `V₀`, `hV₀`), the vector `ψ` with its orthogonality +`hψ`, and the data `n`, `a`, `ξ` with `hξ`. + +Blueprint: lmm:reeh-schlieder-vanishing-near-origin -/ +theorem inner_translated_products_eq_zero_of_mem {N : HaagKastlerNet} + (π : N.quasilocal.carrier →⋆ₐ[ℂ] (H →L[ℂ] H)) (Ω : H) + (U : StandardMinkowskiSpacetime.Carrier → (H ≃ₗᵢ[ℂ] H)) + (hU : ∀ x a, U x (π a Ω) = π (N.action (translationSub x) a) Ω) + {B₁ B : Set StandardMinkowskiSpacetime.Carrier} + (hB₁ : IsAlexandrovBasisSet B₁) (hB : IsAlexandrovBasisSet B) + {ψ : H} (hψ : ∀ b : N.U.algebra B, ⟪ψ, π (N.quasilocal.ι hB b) Ω⟫_ℂ = 0) + {n : ℕ} (a : Fin n → N.U.algebra B₁) + {V₀ : Set StandardMinkowskiSpacetime.Carrier} + (hV₀ : ∀ k ≤ n, ∀ η : Fin k → StandardMinkowskiSpacetime.Carrier, + (∀ i, η i ∈ V₀) → translationSub (∑ i, η i) • B₁ ⊆ B) + (ξ : Fin n → StandardMinkowskiSpacetime.Carrier) (hξ : ∀ i, ξ i ∈ V₀) : + ⟪ψ, (List.ofFn fun i => + (U (ξ i) : H →L[ℂ] H) * π (N.quasilocal.ι hB₁ (a i))).prod Ω⟫_ℂ = 0 := by + rw [translated_products_apply π Ω U hU] + obtain ⟨b, hb⟩ : (List.ofFn fun i : Fin n => N.action (translationSub + (∑ j : Fin (i + 1), ξ (Fin.castLE i.isLt j))) (N.quasilocal.ι hB₁ (a i))).prod ∈ + (N.quasilocal.ι hB).range := by + refine list_prod_mem fun y hy => ?_ + obtain ⟨i, rfl⟩ := List.mem_ofFn.mp hy + exact (action_translationSub_image_range_ι N hB₁ hB _).2 + (hV₀ (i + 1) i.isLt _ fun j => hξ _) ⟨_, ⟨a i, rfl⟩, rfl⟩ + rw [← hb] + exact hψ b + +/-- **Factorization in one variable.** Fix `ξ` and an index `k`. As a function of the `k`-th +variable `t`, `F = ⟨ψ, U(ξ₁)π(a₁) ⋯ U(ξₙ)π(aₙ)Ω⟩` has the form `⟨χ, U(t)φ⟩` with `χ ∈ H` and `φ` +in the cyclic subspace `K₀`; the blueprint's +`χ = (U(ξ₁)π(a₁) ⋯ U(ξ_{k-1})π(a_{k-1}))^* ψ` and +`φ = π(a_k)U(ξ_{k+1})π(a_{k+1}) ⋯ U(ξₙ)π(aₙ)Ω` are not fixed in the statement. + +Only the covariance hypothesis is needed from the blueprint's setting, and the factors `aᵢ` may +be any elements of `𝔘`, as in `translated_products_apply`. + +Blueprint: lmm:reeh-schlieder-factorization -/ +theorem inner_translated_products_update_eq_inner {N : HaagKastlerNet} + (π : N.quasilocal.carrier →⋆ₐ[ℂ] (H →L[ℂ] H)) (Ω : H) + (U : StandardMinkowskiSpacetime.Carrier → (H ≃ₗᵢ[ℂ] H)) + (hU : ∀ x a, U x (π a Ω) = π (N.action (translationSub x) a) Ω) + (ψ : H) {n : ℕ} (a : Fin n → N.quasilocal.carrier) + (ξ : Fin n → StandardMinkowskiSpacetime.Carrier) (k : Fin n) : + ∃ χ : H, ∃ φ ∈ (Submodule.span ℂ (Set.range fun a => π a Ω)).topologicalClosure, + ∀ t : StandardMinkowskiSpacetime.Carrier, + ⟪ψ, (List.ofFn fun i => + (U (Function.update ξ k t i) : H →L[ℂ] H) * π (a i)).prod Ω⟫_ℂ = + ⟪χ, U t φ⟫_ℂ := by + set K := (Submodule.span ℂ (Set.range fun a => π a Ω)).topologicalClosure + obtain ⟨hΩ, hπ, hUK⟩ := translations_cyclicSubspace_invariant π Ω U hU + have memK : ∀ {m : ℕ} (b : Fin m → N.quasilocal.carrier) + (η : Fin m → StandardMinkowskiSpacetime.Carrier), + (List.ofFn fun i => (U (η i) : H →L[ℂ] H) * π (b i)).prod Ω ∈ K := by + intro m + induction m with + | zero => + intro b η + have : π 1 Ω ∈ K := Submodule.le_topologicalClosure _ (Submodule.subset_span ⟨1, rfl⟩) + simpa using this + | succ m ih => + intro b η + rw [List.ofFn_succ, List.prod_cons] + exact hUK _ _ (hπ _ _ (ih _ _)) + induction n generalizing ψ with + | zero => exact k.elim0 + | succ m ih => + simp only [List.ofFn_succ, List.prod_cons] + refine Fin.cases ?_ (fun k' => ?_) k + · refine ⟨ψ, π (a 0) ((List.ofFn fun i => + (U (ξ i.succ) : H →L[ℂ] H) * π (a i.succ)).prod Ω), hπ _ _ (memK _ _), fun t => ?_⟩ + simp + · obtain ⟨χ, φ, hφ, h⟩ := ih (((U (ξ 0) : H →L[ℂ] H) * π (a 0)).adjoint ψ) + (fun i => a i.succ) (fun i => ξ i.succ) k' + refine ⟨χ, φ, hφ, fun t => ?_⟩ + rw [← h t] + have e : ∀ i : Fin m, Function.update ξ k'.succ t i.succ = + Function.update (fun j => ξ j.succ) k' t i := fun i => by + by_cases hi : i = k' + · subst hi; simp + · rw [Function.update_of_ne (fun h => hi (Fin.succ_injective _ h)), + Function.update_of_ne hi] + simp only [Function.update_of_ne (Fin.succ_ne_zero k').symm, e] + rw [ContinuousLinearMap.adjoint_inner_left] + rfl + +/-- **Vanishing of the correlation functions.** In the setting of +`inner_translated_products_eq_zero_of_mem`, with `B₁ + x ⊆ B` for all `x` near `0`, suppose +moreover that every future-timelike translation subgroup `t ↦ U(t n)` has positive energy. Then +`F(ξ) = ⟨ψ, U(ξ₁)π(a₁) ⋯ U(ξₙ)π(aₙ)Ω⟩` vanishes for all `ξ ∈ (ℝ⁴)ⁿ`. + +The blueprint's open neighbourhood `V` of `0` with `B₁ + x ⊆ B` for `x ∈ V` is the eventual +statement `hB₁B` in `nhds 0`, for the Euclidean topology of `ℝ⁴`. The binder groups are the +covariant setting (`π`, `Ω`, `U`, `hU`), positive energy (`hpos`), the diamonds with the +translation condition (`hB₁`, `hB`, `hB₁B`), the vector `ψ` with its orthogonality `hψ`, and the +data `n`, `a`, `ξ`. + +Blueprint: lmm:reeh-schlieder-correlations-vanish -/ +theorem inner_translated_products_eq_zero {N : HaagKastlerNet} + (π : N.quasilocal.carrier →⋆ₐ[ℂ] (H →L[ℂ] H)) (Ω : H) + (U : StandardMinkowskiSpacetime.Carrier → (H ≃ₗᵢ[ℂ] H)) + (hU : ∀ x a, U x (π a Ω) = π (N.action (translationSub x) a) Ω) + (hpos : ∀ n : StandardMinkowskiSpacetime.Carrier, + (n : SpacetimeModel) ∈ minkowskiForwardCone 0 → IsPositiveEnergy (fun t : ℝ => U (t • n))) + {B₁ B : Set StandardMinkowskiSpacetime.Carrier} + (hB₁ : IsAlexandrovBasisSet B₁) (hB : IsAlexandrovBasisSet B) + (hB₁B : ∀ᶠ x in nhds 0, translationSub x • B₁ ⊆ B) + {ψ : H} (hψ : ∀ b : N.U.algebra B, ⟪ψ, π (N.quasilocal.ι hB b) Ω⟫_ℂ = 0) + {n : ℕ} (a : Fin n → N.U.algebra B₁) (ξ : Fin n → StandardMinkowskiSpacetime.Carrier) : + ⟪ψ, (List.ofFn fun i => + (U (ξ i) : H →L[ℂ] H) * π (N.quasilocal.ι hB₁ (a i))).prod Ω⟫_ℂ = 0 := by + obtain ⟨V₀, hV₀o, hV₀0, hV₀⟩ := + exists_isOpen_sum_mem_of_mem_nhds (V := {x | translationSub x • B₁ ⊆ B}) hB₁B n + have P : ∀ m, ∀ ξ : Fin n → StandardMinkowskiSpacetime.Carrier, + (∀ i : Fin n, m ≤ i.val → ξ i ∈ V₀) → + ⟪ψ, (List.ofFn fun i => + (U (ξ i) : H →L[ℂ] H) * π (N.quasilocal.ι hB₁ (a i))).prod Ω⟫_ℂ = 0 := by + intro m + induction m with + | zero => + exact fun ξ hξ => inner_translated_products_eq_zero_of_mem π Ω U hU hB₁ hB hψ a + hV₀ ξ fun i => hξ i (Nat.zero_le _) + | succ m ih => + intro ξ hξ + by_cases hm : m < n + · obtain ⟨χ, φ, hφ, h⟩ := inner_translated_products_update_eq_inner π Ω U hU ψ + (fun i => N.quasilocal.ι hB₁ (a i)) ξ ⟨m, hm⟩ + have hz := inner_translation_eq_zero U (translations_add_cyclicSubspace π Ω U hU φ hφ) + hpos χ hV₀o ⟨0, hV₀0⟩ fun t ht => by + rw [← h t] + refine ih _ fun i hi => ?_ + by_cases hik : i = ⟨m, hm⟩ + · subst hik; simpa using ht + · have : i.val ≠ m := fun e => hik (Fin.ext e) + rw [Function.update_of_ne hik] + exact hξ i (by omega) + have e := h (ξ ⟨m, hm⟩) + rw [Function.update_eq_self] at e + exact e.trans (hz _) + · exact ih ξ fun i hi => hξ i (by omega) + exact P n ξ fun i hi => absurd i.isLt (by omega) + +/-- **Orthogonality on monomials.** In the setting of `inner_translated_products_eq_zero`, for +every `n ≥ 0`, all `y₁, …, yₙ ∈ ℝ⁴` and all `a₁, …, aₙ ∈ 𝔘(B₁)`, +`⟨ψ, π(β_{y₁}a₁ ⋯ β_{yₙ}aₙ)Ω⟩ = 0`, the empty product being `1`. + +The binder groups are the covariant setting (`π`, `Ω`, `U`, `hU`), positive energy (`hpos`), the +diamonds with the translation condition (`hB₁`, `hB`, `hB₁B`), the vector `ψ` with its +orthogonality `hψ`, and the data `n`, `a`, `y`. + +Blueprint: lmm:reeh-schlieder-monomial-orthogonal -/ +theorem inner_monomial_eq_zero {N : HaagKastlerNet} + (π : N.quasilocal.carrier →⋆ₐ[ℂ] (H →L[ℂ] H)) (Ω : H) + (U : StandardMinkowskiSpacetime.Carrier → (H ≃ₗᵢ[ℂ] H)) + (hU : ∀ x a, U x (π a Ω) = π (N.action (translationSub x) a) Ω) + (hpos : ∀ n : StandardMinkowskiSpacetime.Carrier, + (n : SpacetimeModel) ∈ minkowskiForwardCone 0 → IsPositiveEnergy (fun t : ℝ => U (t • n))) + {B₁ B : Set StandardMinkowskiSpacetime.Carrier} + (hB₁ : IsAlexandrovBasisSet B₁) (hB : IsAlexandrovBasisSet B) + (hB₁B : ∀ᶠ x in nhds 0, translationSub x • B₁ ⊆ B) + {ψ : H} (hψ : ∀ b : N.U.algebra B, ⟪ψ, π (N.quasilocal.ι hB b) Ω⟫_ℂ = 0) + {n : ℕ} (a : Fin n → N.U.algebra B₁) (y : Fin n → StandardMinkowskiSpacetime.Carrier) : + ⟪ψ, π ((List.ofFn fun i => + N.action (translationSub (y i)) (N.quasilocal.ι hB₁ (a i))).prod) Ω⟫_ℂ = 0 := by + set ξ : Fin n → StandardMinkowskiSpacetime.Carrier := fun i => + y i - (if h : (i : ℕ) = 0 then 0 else y ⟨i - 1, by omega⟩) + have hx : ∀ k (hk : k < n), ∑ j : Fin (k + 1), ξ (Fin.castLE hk j) = y ⟨k, hk⟩ := by + intro k + induction k with + | zero => intro hk; simp [ξ]; rfl + | succ k ih => + intro hk + rw [Fin.sum_univ_castSucc] + have := ih (by omega) + simp only [Fin.castLE_castSucc] at this ⊢ + rw [this] + simp [ξ, Fin.castLE, Fin.last] + have h := inner_translated_products_eq_zero π Ω U hU hpos hB₁ hB hB₁B hψ a ξ + rw [translated_products_apply π Ω U hU] at h + convert h using 6 + funext i + rw [hx i i.isLt] + +end HaagKastler +end AQFT +end Physicslib4 diff --git a/Physicslib4/AQFT/HaagKastler/ReehSchlieder/CyclicSubspace.lean b/Physicslib4/AQFT/HaagKastler/ReehSchlieder/CyclicSubspace.lean new file mode 100644 index 0000000..3e82a8a --- /dev/null +++ b/Physicslib4/AQFT/HaagKastler/ReehSchlieder/CyclicSubspace.lean @@ -0,0 +1,132 @@ +/- +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.AQFT.HaagKastler.ReehSchlieder.Translations + +/-! +# Translations on the cyclic subspace + +Let `π` be a `*`-representation of the quasilocal algebra on `H`, `Ω ∈ H`, and `x ↦ U(x)` +unitaries indexed by the translations `ℝ⁴` with `U(x)π(a)Ω = π(β_x a)Ω`, where +`β_x = N.action (translationSub x)`. The cyclic subspace `K₀` is the closure of +`π(𝔘)Ω`, written `(Submodule.span ℂ (Set.range fun a => π a Ω)).topologicalClosure`; the span +is the range itself since `π` is linear, but the closed-submodule form is the one used throughout. +Cyclicity of `Ω` is not assumed. + +* `apply_eq_of_mem_cyclicSubspace` — bounded operators agreeing on every `π(a)Ω` agree on `K₀`. +* `translations_cyclicSubspace_invariant` — `U(x)Ω = Ω`, and `K₀` is invariant under every + `π(a)` and every `U(x)`. +* `translations_intertwine_cyclicSubspace` — `U(x)π(a) = π(β_x a)U(x)` on `K₀`. +* `translations_add_cyclicSubspace` — `U(x + y) = U(x)U(y)` on `K₀`. +* `covariant_translations_cyclicSubspace` — the conjunction of the three preceding lemmas. +-/ + +namespace Physicslib4 +namespace AQFT +namespace HaagKastler + +open Spacetime + +variable {H : Type*} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] + +/-- Let `π` be a `*`-representation of the quasilocal algebra on `H` and `Ω ∈ H`. Bounded +operators `S, T` on `H` with `S π(a) Ω = T π(a) Ω` for every `a` agree on the cyclic subspace +`K₀`, the closure of `π(𝔘)Ω`. + +Blueprint: lmm:agree-on-cyclic-subspace -/ +theorem apply_eq_of_mem_cyclicSubspace {N : HaagKastlerNet} + (π : N.quasilocal.carrier →⋆ₐ[ℂ] (H →L[ℂ] H)) (Ω : H) {S T : H →L[ℂ] H} + (h : ∀ a, S (π a Ω) = T (π a Ω)) : + ∀ φ ∈ (Submodule.span ℂ (Set.range fun a => π a Ω)).topologicalClosure, S φ = T φ := + fun _ hφ => ContinuousLinearMap.eqOn_closure_span (by rintro _ ⟨a, rfl⟩; exact h a) hφ + +/-- Let `π` be a `*`-representation of the quasilocal algebra on `H`, `Ω ∈ H`, and `x ↦ U(x)` +unitaries indexed by the translations with `U(x) π(a) Ω = π(β_x a) Ω`. Then `U(x)Ω = Ω`, and the +cyclic subspace `K₀`, the closure of `π(𝔘)Ω`, is invariant under every `π(a)` and every `U(x)`. + +Blueprint: lmm:translations-cyclic-subspace-invariant -/ +theorem translations_cyclicSubspace_invariant {N : HaagKastlerNet} + (π : N.quasilocal.carrier →⋆ₐ[ℂ] (H →L[ℂ] H)) (Ω : H) + (U : StandardMinkowskiSpacetime.Carrier → (H ≃ₗᵢ[ℂ] H)) + (hU : ∀ x a, U x (π a Ω) = π (N.action (translationSub x) a) Ω) : + (∀ x, U x Ω = Ω) ∧ + (∀ a, ∀ φ ∈ (Submodule.span ℂ (Set.range fun a => π a Ω)).topologicalClosure, + π a φ ∈ (Submodule.span ℂ (Set.range fun a => π a Ω)).topologicalClosure) ∧ + (∀ x, ∀ φ ∈ (Submodule.span ℂ (Set.range fun a => π a Ω)).topologicalClosure, + U x φ ∈ (Submodule.span ℂ (Set.range fun a => π a Ω)).topologicalClosure) := by + set K := (Submodule.span ℂ (Set.range fun a => π a Ω)).topologicalClosure + have gen : ∀ b, π b Ω ∈ K := fun b => + Submodule.le_topologicalClosure _ (Submodule.subset_span ⟨b, rfl⟩) + have key : ∀ T : H →L[ℂ] H, (∀ b, T (π b Ω) ∈ K) → ∀ φ ∈ K, T φ ∈ K := fun T hT φ hφ => + Submodule.topologicalClosure_minimal _ (t := K.comap (T : H →ₗ[ℂ] H)) + (Submodule.span_le.2 (by rintro _ ⟨b, rfl⟩; exact hT b)) + ((Submodule.isClosed_topologicalClosure _).preimage T.continuous) hφ + refine ⟨fun x => by simpa using hU x 1, fun a => key (π a) fun b => ?_, + fun x => key (U x).toLinearIsometry.toContinuousLinearMap fun b => ?_⟩ + · simpa using gen (a * b) + · exact (hU x b).symm ▸ gen _ + +/-- Under the hypotheses of `translations_cyclicSubspace_invariant`, +`U(x) π(a) = π(β_x a) U(x)` on the cyclic subspace `K₀` for every translation `x` and every `a`. + +Blueprint: lmm:translations-intertwine-cyclic-subspace -/ +theorem translations_intertwine_cyclicSubspace {N : HaagKastlerNet} + (π : N.quasilocal.carrier →⋆ₐ[ℂ] (H →L[ℂ] H)) (Ω : H) + (U : StandardMinkowskiSpacetime.Carrier → (H ≃ₗᵢ[ℂ] H)) + (hU : ∀ x a, U x (π a Ω) = π (N.action (translationSub x) a) Ω) : + ∀ x a, ∀ φ ∈ (Submodule.span ℂ (Set.range fun a => π a Ω)).topologicalClosure, + U x (π a φ) = π (N.action (translationSub x) a) (U x φ) := by + intro x a φ hφ + exact apply_eq_of_mem_cyclicSubspace π Ω + (S := ((U x).toContinuousLinearEquiv : H →L[ℂ] H).comp (π a)) + (T := (π (N.action (translationSub x) a)).comp ((U x).toContinuousLinearEquiv : H →L[ℂ] H)) + (fun b => by + change U x (π a (π b Ω)) = π (N.action (translationSub x) a) (U x (π b Ω)) + rw [← mul_apply_eq_comp, ← map_mul, hU, hU, map_mul, map_mul, + mul_apply_eq_comp]) φ hφ + +/-- Under the hypotheses of `translations_cyclicSubspace_invariant`, `U(x + y) = U(x) U(y)` on +the cyclic subspace `K₀`: for every `φ ∈ K₀`, `U(x + y)φ = U(x)U(y)φ` for all translations +`x, y`. This is the hypothesis `hmul` of `inner_translation_eq_zero`. + +Blueprint: lmm:translations-group-law-cyclic-subspace -/ +theorem translations_add_cyclicSubspace {N : HaagKastlerNet} + (π : N.quasilocal.carrier →⋆ₐ[ℂ] (H →L[ℂ] H)) (Ω : H) + (U : StandardMinkowskiSpacetime.Carrier → (H ≃ₗᵢ[ℂ] H)) + (hU : ∀ x a, U x (π a Ω) = π (N.action (translationSub x) a) Ω) : + ∀ φ ∈ (Submodule.span ℂ (Set.range fun a => π a Ω)).topologicalClosure, + ∀ x y, U (x + y) φ = U x (U y φ) := fun φ hφ x y => + apply_eq_of_mem_cyclicSubspace π Ω (S := ((U (x + y) : H ≃L[ℂ] H) : H →L[ℂ] H)) + (T := ((U x : H ≃L[ℂ] H) : H →L[ℂ] H) ∘L ((U y : H ≃L[ℂ] H) : H →L[ℂ] H)) + (fun a => show U (x + y) (π a Ω) = U x (U y (π a Ω)) by + rw [hU, hU, hU, translationSub_mul, HaagKastlerNet.action_mul_apply]) φ hφ + +/-- **Translations on the cyclic subspace.** Let `π` be a `*`-representation of the quasilocal +algebra on `H`, `Ω ∈ H`, and `x ↦ U(x)` unitaries indexed by the translations with +`U(x) π(a) Ω = π(β_x a) Ω`, and let `K₀` be the closure of `π(𝔘)Ω`. Then `U(x)Ω = Ω`; `K₀` is +invariant under every `π(a)` and `U(x)`; and on `K₀`, `U(x)π(a) = π(β_x a)U(x)` and +`U(x + y) = U(x)U(y)`. + +Blueprint: lmm:covariant-translations-cyclic-subspace -/ +theorem covariant_translations_cyclicSubspace {N : HaagKastlerNet} + (π : N.quasilocal.carrier →⋆ₐ[ℂ] (H →L[ℂ] H)) (Ω : H) + (U : StandardMinkowskiSpacetime.Carrier → (H ≃ₗᵢ[ℂ] H)) + (hU : ∀ x a, U x (π a Ω) = π (N.action (translationSub x) a) Ω) : + (∀ x, U x Ω = Ω) ∧ + (∀ a, ∀ φ ∈ (Submodule.span ℂ (Set.range fun a => π a Ω)).topologicalClosure, + π a φ ∈ (Submodule.span ℂ (Set.range fun a => π a Ω)).topologicalClosure) ∧ + (∀ x, ∀ φ ∈ (Submodule.span ℂ (Set.range fun a => π a Ω)).topologicalClosure, + U x φ ∈ (Submodule.span ℂ (Set.range fun a => π a Ω)).topologicalClosure) ∧ + (∀ x a, ∀ φ ∈ (Submodule.span ℂ (Set.range fun a => π a Ω)).topologicalClosure, + U x (π a φ) = π (N.action (translationSub x) a) (U x φ)) ∧ + (∀ φ ∈ (Submodule.span ℂ (Set.range fun a => π a Ω)).topologicalClosure, + ∀ x y, U (x + y) φ = U x (U y φ)) := + let ⟨h1, h2, h3⟩ := translations_cyclicSubspace_invariant π Ω U hU + ⟨h1, h2, h3, translations_intertwine_cyclicSubspace π Ω U hU, + translations_add_cyclicSubspace π Ω U hU⟩ + +end HaagKastler +end AQFT +end Physicslib4 diff --git a/Physicslib4/AQFT/HaagKastler/ReehSchlieder/Translations.lean b/Physicslib4/AQFT/HaagKastler/ReehSchlieder/Translations.lean new file mode 100644 index 0000000..95e2a65 --- /dev/null +++ b/Physicslib4/AQFT/HaagKastler/ReehSchlieder/Translations.lean @@ -0,0 +1,242 @@ +/- +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.AQFT.HaagKastler.VacuumState +import Physicslib4.AQFT.PositiveEnergyHolomorphic +import Physicslib4.Analysis.EdgeVanishing +import Physicslib4.Spacetime.LorentzCausality +import Physicslib4.Spacetime.MinkowskiDirected + +/-! +# Translations of diamonds and timelike spreading + +The geometric and analytic lemmas on spacetime translations used by the Reeh–Schlieder +theorem. + +* `translationSub_smul_diamond` — the translate `B + x = translationSub x • B` of the diamond + `I⁺(p) ∩ I⁻(q)` is the diamond `I⁺(p + x) ∩ I⁻(q + x)`. +* `exists_diamond_translate_subset` — a nonempty diamond contains every small translate of + some smaller nonempty diamond. +* `exists_isOpen_sum_mem_of_mem_nhds` — small enough summands keep a bounded number of partial + sums inside a given neighbourhood of `0`. +* `futureTimelike_basis` — the vectors `e₀` and `e₀ + ½ eᵢ` are future-pointing timelike and + form a basis of `ℝ⁴`. +* `inner_translation_eq_zero_add_smul` and `inner_translation_eq_zero` — under positive energy + a matrix coefficient `x ↦ ⟨χ, U(x)φ⟩` that vanishes on an open set spreads its vanishing along + every future-timelike direction, and hence vanishes identically when the open set is nonempty. + +Throughout, `ℝ⁴` is the carrier of standard Minkowski spacetime with its manifold topology, +which is the Euclidean topology of `EuclideanSpace ℝ (Fin 4)`. A family of unitaries indexed by +translations is a function `U : StandardMinkowskiSpacetime.Carrier → (H ≃ₗᵢ[ℂ] H)`; the +unitaries `U' : InhomogeneousLorentzGroup → (H ≃ₗᵢ[ℂ] H)` of a vacuum state give such a family +as `fun x => U' (translationSub x)`, and then `fun t => U' (translationFlow n t)` is +definitionally `fun t => U' (translationSub (t • n))`. +-/ + +namespace Physicslib4 +namespace AQFT +namespace HaagKastler + +open scoped InnerProductSpace Pointwise +open Spacetime + +variable {H : Type*} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] + +/-- The translate of a diamond is a diamond: for all `p, q, x ∈ ℝ⁴`, +`translationSub x • (I⁺(p) ∩ I⁻(q)) = I⁺(p + x) ∩ I⁻(q + x)`. + +Blueprint: lmm:diamond-translate -/ +theorem translationSub_smul_diamond (p q x : StandardMinkowskiSpacetime.Carrier) : + translationSub x • + (chronologicalFuture StandardMinkowskiSpacetime standardMinkowskiTimeOrientation p ∩ + chronologicalPast StandardMinkowskiSpacetime standardMinkowskiTimeOrientation q) = + chronologicalFuture StandardMinkowskiSpacetime standardMinkowskiTimeOrientation (p + x) ∩ + chronologicalPast StandardMinkowskiSpacetime standardMinkowskiTimeOrientation (q + x) := by + have hg : ∀ y, translationSub x • y = y + x := fun _ => rfl + ext y + simp only [Set.mem_inter_iff, chronologicalFuture, chronologicalPast, Set.mem_ofPred_eq, + Set.mem_smul_set_iff_inv_smul_mem, ← hg p, ← hg q] + conv_rhs => rw [← smul_inv_smul (translationSub x) y] + rw [chronologicallyPrecedes_smul_iff, chronologicallyPrecedes_smul_iff] + +/-- Every nonempty diamond `B` contains all small translates of a smaller nonempty diamond: +there are a nonempty diamond `B₁` and an open neighbourhood `V` of `0` in `ℝ⁴` with +`B₁ + x = translationSub x • B₁ ⊆ B` for every `x ∈ V`. + +Openness of `V` refers to the manifold topology of standard Minkowski spacetime, the Euclidean +topology of `ℝ⁴`. + +Blueprint: lmm:diamond-small-translates -/ +theorem exists_diamond_translate_subset {B : Set StandardMinkowskiSpacetime.Carrier} + (hB : IsAlexandrovBasisSet B) (hBne : B.Nonempty) : + ∃ B₁ : Set StandardMinkowskiSpacetime.Carrier, IsAlexandrovBasisSet B₁ ∧ B₁.Nonempty ∧ + ∃ V : Set StandardMinkowskiSpacetime.Carrier, IsOpen V ∧ 0 ∈ V ∧ + ∀ x ∈ V, translationSub x • B₁ ⊆ B := by + have trans := @StandardMinkowskiSpacetime.chronologicallyPrecedes_trans + standardMinkowskiTimeOrientation + have interp : ∀ a c : StandardMinkowskiSpacetime.Carrier, + (a ≪[StandardMinkowskiSpacetime, standardMinkowskiTimeOrientation] c) → + ∃ b, (a ≪[StandardMinkowskiSpacetime, standardMinkowskiTimeOrientation] b) ∧ + b ≪[StandardMinkowskiSpacetime, standardMinkowskiTimeOrientation] c := by + intro a c h + have e := fun c => Set.ext_iff.mp (chronologicalPast_standardMinkowski c) + obtain ⟨b, hb, -, hab⟩ := + exists_future_between_standardMinkowski ((e c a).mp h) ((e c a).mp h) + exact ⟨b, (e b a).mpr hab, (e c b).mpr hb⟩ + obtain ⟨p, q, rfl⟩ := hB + obtain ⟨y, hpy, hyq⟩ := hBne + obtain ⟨p', hpp', hp'q⟩ := interp p q (trans hpy hyq) + obtain ⟨q', hp'q', hq'q⟩ := interp p' q hp'q + obtain ⟨z, hp'z, hzq'⟩ := interp p' q' hp'q' + refine ⟨_, ⟨p', q', rfl⟩, ⟨z, hp'z, hzq'⟩, + (p' + ·) ⁻¹' chronologicalFuture StandardMinkowskiSpacetime + standardMinkowskiTimeOrientation p ∩ + (q' + ·) ⁻¹' chronologicalPast StandardMinkowskiSpacetime + standardMinkowskiTimeOrientation q, ?_, ?_, ?_⟩ + · exact ((isOpen_chronologicalFuture_standardMinkowski p).preimage + (continuous_const.add continuous_id)).inter + ((isOpen_chronologicalPast_standardMinkowski q).preimage + (continuous_const.add continuous_id)) + · exact ⟨by simp only [Set.mem_preimage, add_zero]; exact hpp', + by simp only [Set.mem_preimage, add_zero]; exact hq'q⟩ + · rintro x ⟨hx₁, hx₂⟩ + rw [translationSub_smul_diamond] + rintro w ⟨hw₁, hw₂⟩ + exact ⟨trans hx₁ hw₁, trans hw₂ hx₂⟩ + +/-- For every neighbourhood `V` of `0` and every `n` there is an open neighbourhood `V₀` of `0` +such that `ξ₁ + ⋯ + ξₖ ∈ V` whenever `k ≤ n` and `ξ₁, …, ξₖ ∈ V₀`. + +The statement is made for any commutative topological additive monoid with continuous addition; +the blueprint uses it for `ℝ⁴`. The blueprint's side conditions `n ≥ 1` and `k ≥ 1` are +omitted: the case `k = 0` holds because the empty sum `0` lies in `V`. + +Blueprint: lmm:neighbourhood-partial-sums -/ +theorem exists_isOpen_sum_mem_of_mem_nhds {G : Type*} [AddCommMonoid G] [TopologicalSpace G] + [ContinuousAdd G] {V : Set G} (hV : V ∈ nhds (0 : G)) (n : ℕ) : + ∃ V₀ : Set G, IsOpen V₀ ∧ (0 : G) ∈ V₀ ∧ + ∀ k ≤ n, ∀ ξ : Fin k → G, (∀ i, ξ i ∈ V₀) → ∑ i, ξ i ∈ V := by + have key : ∀ k, ∃ W ∈ nhds (0 : G), ∀ ξ : Fin k → G, (∀ i, ξ i ∈ W) → ∑ i, ξ i ∈ V := by + intro k + have h : Filter.Tendsto (fun ξ : Fin k → G => ∑ i, ξ i) (nhds 0) (nhds 0) := by + simpa using (continuous_finsetSum Finset.univ fun i _ => continuous_apply i).tendsto + (0 : Fin k → G) + have h2 := h hV + rw [nhds_pi] at h2 + obtain ⟨I, t, ht, hs⟩ := Filter.mem_pi'.1 h2 + exact ⟨⋂ i, t i, Filter.iInter_mem.2 ht, fun ξ hξ => hs fun i _ => Set.mem_iInter.1 (hξ i) i⟩ + choose W hW hWV using key + refine ⟨interior (⋂ k ∈ Finset.range (n + 1), W k), isOpen_interior, + mem_interior_iff_mem_nhds.2 ((Filter.biInter_finset_mem _).2 fun k _ => hW k), + fun k hk ξ hξ => hWV k ξ fun i => ?_⟩ + exact Set.mem_iInter₂.1 (interior_subset (hξ i)) k (Finset.mem_range.2 (Nat.lt_succ_of_le hk)) + +/-- The vectors `n₀ = e₀` and `nᵢ = e₀ + ½ eᵢ`, `i = 1, 2, 3`, are future-pointing timelike (they +lie in the open forward cone `minkowskiForwardCone 0`, the notion used by +`IsFutureTimelikeTranslation`) and form a basis of `ℝ⁴`. + +The family is passed as `n` together with its defining equation `hn`; "form a basis" is the +existence of a basis of `ℝ⁴` indexed by `Fin 4` whose vectors are `n`. + +Blueprint: lmm:future-timelike-basis -/ +theorem futureTimelike_basis (n : Fin 4 → SpacetimeModel) + (hn : ∀ i, n i = EuclideanSpace.single 0 1 + + (if i = 0 then 0 else (2⁻¹ : ℝ) • EuclideanSpace.single i 1)) : + (∀ i, n i ∈ minkowskiForwardCone 0) ∧ ∃ b : Module.Basis (Fin 4) ℝ SpacetimeModel, ⇑b = n := by + obtain rfl : n = _ := funext hn + refine ⟨fun i => ?_, ?_⟩ + · fin_cases i <;> simp [minkowskiForwardCone] <;> norm_num + · have hli : LinearIndependent ℝ (fun i : Fin 4 => EuclideanSpace.single (0 : Fin 4) (1 : ℝ) + + (if i = 0 then 0 else (2⁻¹ : ℝ) • EuclideanSpace.single i 1)) := by + rw [Fintype.linearIndependent_iff] + intro g hg + have h0 := congrArg (· 0) hg; have h1 := congrArg (· 1) hg + have h2 := congrArg (· 2) hg; have h3 := congrArg (· 3) hg + simp [Fin.sum_univ_four] at h0 h1 h2 h3 + intro i; fin_cases i <;> simp <;> linarith + refine ⟨basisOfLinearIndependentOfCardEqFinrank hli (by simp), ?_⟩ + simp + +/-- **Timelike spreading in one direction.** Let `x ↦ U(x)` be unitaries on `H` indexed by the +translations `ℝ⁴`, let `φ ∈ H` satisfy `U(x + y)φ = U(x)U(y)φ`, and let `n` be a direction for +which `t ↦ U(t n)` has positive energy. If `h(x) = ⟨χ, U(x)φ⟩` vanishes on an open set `W`, it +vanishes on `W + ℝn = {x + t n | x ∈ W, t ∈ ℝ}`. + +The unitaries are a function of the translation vector; for a vacuum state with unitaries `U'` +indexed by the inhomogeneous Lorentz group, take `U = fun x => U' (translationSub x)`. Only the +group law at `φ` is used; the blueprint's closed invariant subspace `K₀ ∋ φ`, on which the group law +holds, supplies it, and its timelike condition on `n` enters only through positive energy, which +is assumed directly. Openness of `W` refers to the Euclidean topology of `ℝ⁴`. + +Blueprint: lmm:timelike-spreading-direction -/ +theorem inner_translation_eq_zero_add_smul + (U : StandardMinkowskiSpacetime.Carrier → (H ≃ₗᵢ[ℂ] H)) + {φ : H} (hmul : ∀ x y, U (x + y) φ = U x (U y φ)) + {n : StandardMinkowskiSpacetime.Carrier} (hpos : IsPositiveEnergy (fun t : ℝ => U (t • n))) + (χ : H) + {W : Set StandardMinkowskiSpacetime.Carrier} (hW : IsOpen W) + (hzero : ∀ x ∈ W, ⟪χ, U x φ⟫_ℂ = 0) : + ∀ x ∈ W, ∀ t : ℝ, ⟪χ, U (x + t • n) φ⟫_ℂ = 0 := by + intro x hx t + obtain ⟨F, hFd, hFc, -, hF⟩ := hpos.exists_holomorphic_extension χ (U x φ) + have hsh : ∀ s : ℝ, ⟪χ, U (x + s • n) φ⟫_ℂ = F s := fun s => by + rw [hF, add_comm, hmul] + have hcont : Continuous fun s : ℝ => x + s • n := + continuous_const.add (continuous_id.smul continuous_const) + have hmem : {s : ℝ | x + s • n ∈ W} ∈ nhds (0 : ℝ) := + hcont.continuousAt.preimage_mem_nhds (by simpa using hW.mem_nhds hx) + obtain ⟨ε, hε, hball⟩ := Metric.mem_nhds_iff.1 hmem + have hvan : ∀ s ∈ Set.Ioo (-ε) ε, F s = 0 := fun s hs => by + rw [← hsh] + exact hzero _ (hball (by rw [Metric.mem_ball, Real.dist_0_eq_abs, abs_lt]; exact hs)) + rw [hsh] + exact eq_zero_of_eq_zero_on_Ioo (by linarith) hFc hFd hvan t (by simp) + +/-- **Timelike spreading.** Let `U` and `φ` be as in `inner_translation_eq_zero_add_smul`, and +suppose every future-timelike translation subgroup `t ↦ U(t n)`, `n` in the open forward cone, +has positive energy. If `χ ∈ H` and `x ↦ ⟨χ, U(x)φ⟩` vanishes on a nonempty open set `W`, it +vanishes identically. + +Only the group law at `φ` is used; the blueprint's closed invariant subspace `K₀ ∋ φ` supplies it. + +For a vacuum state with unitaries `U'` indexed by the inhomogeneous Lorentz group, the +positive-energy hypothesis for `U = fun x => U' (translationSub x)` is the spectrum condition of +`HaagKastlerNet.IsVacuumStateConcrete` applied to `translationFlow n`. + +Blueprint: lmm:timelike-spreading -/ +theorem inner_translation_eq_zero + (U : StandardMinkowskiSpacetime.Carrier → (H ≃ₗᵢ[ℂ] H)) + {φ : H} (hmul : ∀ x y, U (x + y) φ = U x (U y φ)) + (hpos : ∀ n : StandardMinkowskiSpacetime.Carrier, + (n : SpacetimeModel) ∈ minkowskiForwardCone 0 → IsPositiveEnergy (fun t : ℝ => U (t • n))) + (χ : H) + {W : Set StandardMinkowskiSpacetime.Carrier} (hW : IsOpen W) (hWne : W.Nonempty) + (hzero : ∀ x ∈ W, ⟪χ, U x φ⟫_ℂ = 0) : + ∀ x, ⟪χ, U x φ⟫_ℂ = 0 := by + obtain ⟨hcone, b, hb⟩ := futureTimelike_basis _ fun _ => rfl + let n : Fin 4 → StandardMinkowskiSpacetime.Carrier := fun i => b i + have hn : ∀ i, (n i : SpacetimeModel) ∈ minkowskiForwardCone 0 := fun i => + show b i ∈ _ by rw [hb]; exact hcone i + let P : StandardMinkowskiSpacetime.Carrier → Prop := fun v => ∀ y ∈ W, ⟪χ, U (y + v) φ⟫_ℂ = 0 + have step : ∀ v, P v → ∀ i (t : ℝ), P (v + t • n i) := by + intro v hv i t y hy + have h := inner_translation_eq_zero_add_smul U hmul (hpos _ (hn i)) χ + (W := (· - v) ⁻¹' W) (hW.preimage (continuous_id.sub continuous_const)) + (fun z hz => by simpa using hv _ hz) (y + v) (by simpa using hy) t + rwa [← add_assoc] + have key : ∀ s : Finset (Fin 4), ∀ c : Fin 4 → ℝ, P (∑ i ∈ s, c i • n i) := by + intro s c + induction s using Finset.induction_on with + | empty => simpa [P] using hzero + | insert j s hj ih => rw [Finset.sum_insert hj, add_comm]; exact step _ ih j (c j) + obtain ⟨w, hw⟩ := hWne + intro x + have hx : ∑ i, b.repr (x - w) i • n i = x - w := b.sum_repr (x - w) + have := key Finset.univ (b.repr (x - w)) w hw + rwa [hx, add_sub_cancel] at this + +end HaagKastler +end AQFT +end Physicslib4 diff --git a/Physicslib4/AQFT/PositiveEnergyHolomorphic.lean b/Physicslib4/AQFT/PositiveEnergyHolomorphic.lean new file mode 100644 index 0000000..eea05ab --- /dev/null +++ b/Physicslib4/AQFT/PositiveEnergyHolomorphic.lean @@ -0,0 +1,288 @@ +/- +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.AQFT.PositiveEnergy +import Physicslib4.Spectral.Stone.Exponential +import Physicslib4.Spectral.Unbounded.FunctionalCalculus +import Mathlib.Analysis.Calculus.ParametricIntegral +import Mathlib.MeasureTheory.Integral.DominatedConvergence + +/-! +# Holomorphic extension under positive energy + +If a one-parameter unitary group V has positive energy, every matrix coefficient +t ↦ ⟨χ, V(t)φ⟩ extends to a function holomorphic on the open upper half-plane and bounded and +continuous on the closed upper half-plane (`IsPositiveEnergy.exists_holomorphic_extension`). +This is the form in which the Reeh–Schlieder theorem uses the spectrum condition. + +The route is spectral. Writing V(t) = e^(itA) with A positive and self-adjoint, the spectral +measure of A vanishes on (−∞, 0) (`spectralMeasure_Iio_zero_eq_zero`), each matrix coefficient +is a combination of Fourier transforms of finite measures μ^A_ψ by polarization +(`exists_inner_expUnitary_eq_sum`), and the Fourier–Laplace transform z ↦ ∫ e^(izλ) dν(λ) of a +finite measure carried by [0, ∞) is bounded and continuous on {Im z ≥ 0} +(`fourierLaplace_bounded_continuousOn`) and holomorphic on {Im z > 0} +(`differentiableOn_fourierLaplace`). + +## Main results + +* `spectralMeasure_Ioo_neg_eq_zero` — μ^A((−n, −1/n)) = 0 for A positive. +* `spectralMeasure_Iio_zero_eq_zero` — μ^A((−∞, 0)) = 0 for A positive. +* `exists_inner_expUnitary_eq_sum` — matrix coefficients of e^(itA) by polarization. +* `fourierLaplace_bounded_continuousOn` — the Fourier–Laplace transform on {Im z ≥ 0}. +* `differentiableOn_fourierLaplace` — the Fourier–Laplace transform on {Im z > 0}. +* `IsPositiveEnergy.exists_holomorphic_extension` — the holomorphic extension. +-/ + +namespace Physicslib4 +namespace AQFT + +open scoped InnerProductSpace +open MeasureTheory Complex Spectral Spectral.Stone + +variable {H : Type*} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] + +/-- +The spectral measure μ^A of a positive self-adjoint operator A vanishes on (−n, −1/n) for +every integer n ≥ 1. + +A vector ψ in the range of μ^A((−n, −1/n)) has its distribution μ^A_ψ concentrated on +(−n, −1/n), so ψ lies in Dom(A) with ⟨ψ, Aψ⟩ ≤ −‖ψ‖²/n; positivity of A forces ψ = 0. + +Implementation note: μ^A is `Spectral.Unbounded.spectralMeasure hA`, a projection-valued +measure on ℝ, and the integer n ≥ 1 is a natural number with `1 ≤ n`. + +Blueprint: lmm:positive-spectral-support-interval +-/ +theorem spectralMeasure_Ioo_neg_eq_zero {A : H →ₗ.[ℂ] H} (hA : IsSelfAdjoint A) + (hpos : Unbounded.IsPositive A) (n : ℕ) (hn : 1 ≤ n) : + Unbounded.spectralMeasure hA (Set.Ioo (-(n : ℝ)) (-(1 / (n : ℝ)))) = 0 := by + set μ := Unbounded.spectralMeasure hA + set E := Set.Ioo (-(n : ℝ)) (-(1 / (n : ℝ))) + have hE : MeasurableSet E := measurableSet_Ioo + have hf : Measurable (fun x : ℝ => (x : ℂ)) := Complex.measurable_ofReal + have hpos' : Unbounded.IsPositive (Unbounded.pmapIntegral μ (fun x : ℝ => (x : ℂ))) := + (Unbounded.pmapIntegral_spectralMeasure hA).symm ▸ hpos + have hn' : (0 : ℝ) < 1 / n := by positivity + ext ψ + set η := μ E ψ + have hη : η ∈ Set.range (μ E) := ⟨ψ, rfl⟩ + have hdom := Unbounded.range_subset_integralDomain μ hf hE (c := n) (fun x hx => by + rw [Complex.norm_real, Real.norm_eq_abs, abs_le] + exact ⟨hx.1.le, hx.2.le.trans (by linarith)⟩) hη + have h1 : 0 ≤ (∫ x, (x : ℂ) ∂(μ.assoc η)).re := (hpos'.2 ⟨η, hdom⟩).trans_eq + (congrArg Complex.re (Unbounded.inner_self_pmapIntegral μ hf ⟨η, hdom⟩)) + have hae : ∀ᵐ x ∂(μ.assoc η), x ∈ E := + (ae_iff (p := fun x => x ∈ E)).mpr (Unbounded.assoc_compl_eq_zero μ hE hη) + have hint : Integrable (fun x : ℝ => x) (μ.assoc η) := by + simpa using (MemLp.integrable one_le_two (Unbounded.mem_integralDomain μ |>.mp hdom)).re + have h2 : ∫ x, x ∂(μ.assoc η) ≤ ∫ _, -(1 / (n : ℝ)) ∂(μ.assoc η) := + integral_mono_ae hint (integrable_const _) (hae.mono fun x hx => hx.2.le) + rw [integral_const, smul_eq_mul, measureReal_def, Unbounded.assoc_univ_eq, + ENNReal.toReal_ofReal (by positivity)] at h2 + have h3 : (∫ x, (x : ℂ) ∂(μ.assoc η)).re = ∫ x, x ∂(μ.assoc η) := by + rw [integral_complex_ofReal]; rfl + simp only [h3] at h1 + have : ‖η‖ ^ 2 = 0 := by nlinarith [sq_nonneg ‖η‖] + simpa using this + +/-- +The spectral measure μ^A of a positive self-adjoint operator A vanishes on (−∞, 0): the +spectrum of A lies in [0, ∞). + +The intervals (−n, −1/n) increase to (−∞, 0), and each carries no spectral weight +(`spectralMeasure_Ioo_neg_eq_zero`), so ⟨ψ, μ^A((−∞, 0))ψ⟩ = 0 for every ψ by continuity of the +measure μ^A_ψ from below; the projection μ^A((−∞, 0)) is therefore zero. + +Blueprint: lmm:positive-spectral-support +-/ +theorem spectralMeasure_Iio_zero_eq_zero {A : H →ₗ.[ℂ] H} (hA : IsSelfAdjoint A) + (hpos : Unbounded.IsPositive A) : + Unbounded.spectralMeasure hA (Set.Iio 0) = 0 := by + set μ := Unbounded.spectralMeasure hA + ext ψ + have hU : Set.Iio (0 : ℝ) ⊆ + ⋃ n : ℕ, Set.Ioo (-((n + 1 : ℕ) : ℝ)) (-(1 / ((n + 1 : ℕ) : ℝ))) := by + intro x (hx : x < 0) + obtain ⟨n, hn⟩ := exists_nat_gt (-x + 1 / (-x)) + have hx' : 0 < 1 / (-x) := one_div_pos.2 (neg_pos.2 hx) + have hn1 : (0 : ℝ) < ((n + 1 : ℕ) : ℝ) := by positivity + refine Set.mem_iUnion.2 ⟨n, ?_, ?_⟩ <;> push_cast at hn1 ⊢ + · linarith + · have : 1 / (n + 1 : ℝ) < -x := (one_div_lt hn1 (by linarith)).2 (by linarith) + linarith + have h0 : μ.assoc ψ (Set.Iio 0) = 0 := measure_mono_null hU (measure_iUnion_null fun n => by + rw [Unbounded.assoc_apply_eq_norm_sq μ ψ measurableSet_Ioo, + spectralMeasure_Ioo_neg_eq_zero hA hpos (n + 1) (by omega)] + simp) + rw [Unbounded.assoc_apply_eq_norm_sq μ ψ measurableSet_Iio, ENNReal.ofReal_eq_zero] at h0 + have : ‖μ (Set.Iio 0) ψ‖ = 0 := by nlinarith [norm_nonneg (μ (Set.Iio 0) ψ)] + simpa using this + +/-- +For a self-adjoint operator A and vectors χ, φ, the matrix coefficient ⟨χ, e^(itA)φ⟩ is a fixed +linear combination of the Fourier transforms ∫ e^(itλ) dμ^A_ψₖ(λ) of four scalar spectral +measures, with vectors ψ₀, …, ψ₃ and constants c₀, …, c₃ independent of t. + +The vectors are ψₖ = χ + iᵏφ with the constants of the polarization identity, and each +diagonal term ⟨ψₖ, e^(itA)ψₖ⟩ is ∫ e^(itλ) dμ^A_ψₖ because e^(itA) = ∫ e^(itλ) dμ^A. + +Implementation note: e^(itA) is `expUnitary hA t`, and μ^A_ψ is +`(Spectral.Unbounded.spectralMeasure hA).assoc ψ`, the finite measure E ↦ ⟨ψ, μ^A(E)ψ⟩. The +integrand e^(itλ) is written `Complex.exp (Complex.I * t * x)`. + +Blueprint: lmm:exp-matrix-coefficient-polarization +-/ +theorem exists_inner_expUnitary_eq_sum {A : H →ₗ.[ℂ] H} (hA : IsSelfAdjoint A) (χ φ : H) : + ∃ (ψ : Fin 4 → H) (c : Fin 4 → ℂ), ∀ t : ℝ, + ⟪χ, expUnitary hA t φ⟫_ℂ = + ∑ k, c k * ∫ x : ℝ, Complex.exp (Complex.I * t * x) + ∂((Unbounded.spectralMeasure hA).assoc (ψ k)) := by + refine ⟨![χ + φ, χ - φ, χ + I • φ, χ - I • φ], ![1 / 4, -1 / 4, -I / 4, I / 4], fun t => ?_⟩ + rw [expUnitary_apply] + set T := (Unbounded.spectralMeasure hA).integral (expFun t) + have h : ∀ v : H, ∫ x : ℝ, Complex.exp (I * t * x) + ∂((Unbounded.spectralMeasure hA).assoc v) = ⟪v, T v⟫_ℂ := fun v => by + rw [ProjectionValuedMeasure.inner_integral _ (expFun_mem_bddMeasurable t)] + simp [expFun, mul_assoc] + simp only [Fin.sum_univ_four, h] + simp [map_add, map_sub, inner_add_left, inner_add_right, inner_sub_left, inner_sub_right, + inner_smul_left, inner_smul_right] + linear_combination ((1:ℂ)/2 * (⟪χ, T φ⟫_ℂ - ⟪φ, T χ⟫_ℂ)) * I_sq + +/-- +**The Fourier–Laplace transform on the closed upper half-plane.** Let ν be a finite positive +Borel measure on ℝ with ν((−∞, 0)) = 0, and G(z) = ∫ e^(izλ) dν(λ). For Im z ≥ 0 the integrand +is ν-integrable, so G(z) is defined; |G(z)| ≤ ν(ℝ); and G is continuous on {Im z ≥ 0}. + +For λ ≥ 0 and Im z ≥ 0, |e^(izλ)| = e^(−λ Im z) ≤ 1, and ν is carried by [0, ∞), so the +integrand is dominated by the constant 1; dominated convergence gives continuity. + +Implementation note: the three conclusions (integrability, the bound, continuity) are the three +components of the conjunction; ν(ℝ) is `ν.real Set.univ`, and G is written inline as +`fun z => ∫ x, Complex.exp (Complex.I * z * x) ∂ν`. + +Blueprint: lmm:fourier-laplace-continuous +-/ +theorem fourierLaplace_bounded_continuousOn (ν : Measure ℝ) [IsFiniteMeasure ν] + (hν : ν (Set.Iio 0) = 0) : + (∀ z : ℂ, 0 ≤ z.im → Integrable (fun x : ℝ => Complex.exp (Complex.I * z * x)) ν) ∧ + (∀ z : ℂ, 0 ≤ z.im → ‖∫ x : ℝ, Complex.exp (Complex.I * z * x) ∂ν‖ ≤ ν.real Set.univ) ∧ + ContinuousOn (fun z : ℂ => ∫ x : ℝ, Complex.exp (Complex.I * z * x) ∂ν) + {z : ℂ | 0 ≤ z.im} := by + have hae : ∀ᵐ x ∂ν, 0 ≤ x := by + rw [ae_iff] + exact measure_mono_null (fun x (hx : ¬ 0 ≤ x) => (not_le.mp hx : x < 0)) hν + have hb : ∀ᵐ x : ℝ ∂ν, ∀ z : ℂ, 0 ≤ z.im → ‖Complex.exp (Complex.I * z * (x : ℂ))‖ ≤ 1 := + hae.mono fun x hx z (hz : 0 ≤ z.im) => by + rw [Complex.norm_exp, Real.exp_le_one_iff] + simp only [mul_re, I_re, I_im, ofReal_re, ofReal_im, mul_im] + nlinarith + have hmeas : ∀ z : ℂ, AEStronglyMeasurable (fun x : ℝ => Complex.exp (Complex.I * z * x)) ν := + fun z => (by fun_prop : Continuous fun x : ℝ => Complex.exp (Complex.I * z * x)) + |>.aestronglyMeasurable + refine ⟨fun z hz => (integrable_const (1 : ℝ)).mono' (hmeas z) (hb.mono fun x hx => hx z hz), + fun z hz => ?_, ?_⟩ + · simpa using norm_integral_le_of_norm_le_const (hb.mono fun x hx => hx z hz) + · exact continuousOn_of_dominated (fun z _ => hmeas z) (fun z hz => hb.mono fun x hx => hx z hz) + (integrable_const 1) (ae_of_all _ fun x => by fun_prop) + +/-- +**Holomorphy of the Fourier–Laplace transform.** For a finite positive Borel measure ν on ℝ with +ν((−∞, 0)) = 0, the function G(z) = ∫ e^(izλ) dν(λ) is holomorphic on the open upper half-plane. + +Near a point z₀ with Im z₀ > 0 the z-derivative iλe^(izλ) of the integrand is bounded by +1/(e δ), δ = Im z₀ / 2, for λ ≥ 0, so differentiation under the integral sign applies. + +Implementation note: G is written inline as `fun z => ∫ x, Complex.exp (Complex.I * z * x) ∂ν`. + +Blueprint: lmm:fourier-laplace-holomorphic +-/ +theorem differentiableOn_fourierLaplace (ν : Measure ℝ) [IsFiniteMeasure ν] + (hν : ν (Set.Iio 0) = 0) : + DifferentiableOn ℂ (fun z : ℂ => ∫ x : ℝ, Complex.exp (Complex.I * z * x) ∂ν) + {z : ℂ | 0 < z.im} := by + have h0 : ∀ᵐ x ∂ν, 0 ≤ x := by + rw [ae_iff]; convert hν using 2; ext; simp + intro z₀ hz₀ + have hz₀ : 0 < z₀.im := hz₀ + set δ := z₀.im / 2 with hδ + have δpos : 0 < δ := by positivity + have hball : ∀ z ∈ Metric.ball z₀ δ, δ ≤ z.im := by + intro z hz + rw [Metric.mem_ball, dist_eq_norm] at hz + have := (abs_le.1 (abs_im_le_norm (z - z₀))).1 + simp only [sub_im] at this + linarith + have hnorm : ∀ z : ℂ, ∀ x : ℝ, ‖Complex.exp (Complex.I * z * x)‖ = Real.exp (-(z.im * x)) := by + intro z x; rw [Complex.norm_exp]; congr 1; simp + have key := hasDerivAt_integral_of_dominated_loc_of_deriv_le (μ := ν) (x₀ := z₀) + (F := fun z x => Complex.exp (Complex.I * z * x)) + (F' := fun z x => Complex.I * x * Complex.exp (Complex.I * z * x)) + (bound := fun _ => 1 / δ) (Metric.ball_mem_nhds z₀ δpos) + (Filter.Eventually.of_forall fun z => by fun_prop) + (Integrable.of_bound (by fun_prop) 1 (h0.mono fun x hx => by + rw [hnorm]; exact Real.exp_le_one_iff.2 (by nlinarith))) + (by fun_prop) + (h0.mono fun x hx z hz => by + have hzδ := hball z hz + rw [norm_mul, norm_mul, hnorm, norm_I, one_mul, Complex.norm_real, Real.norm_of_nonneg hx] + rw [le_div_iff₀ δpos] + have h1 := Real.add_one_le_exp (x * δ) + have h2 : Real.exp (-(z.im * x)) ≤ Real.exp (-(x * δ)) := + Real.exp_le_exp.2 (by nlinarith) + have h3 : Real.exp (x * δ) * Real.exp (-(x * δ)) = 1 := by + rw [← Real.exp_add]; simp + have h4 := Real.exp_pos (-(x * δ)) + nlinarith [mul_le_mul_of_nonneg_left h2 (mul_nonneg hx δpos.le)]) + (integrable_const _) + (Filter.Eventually.of_forall fun x z _ => by + have := (((hasDerivAt_id' z).const_mul Complex.I).mul_const (x : ℂ)).cexp + convert this using 1; ring) + exact key.2.differentiableAt.differentiableWithinAt + +/-- +**Holomorphic extension under positive energy.** If a family V of unitaries indexed by ℝ has +positive energy and χ, φ are vectors, then t ↦ ⟨χ, V(t)φ⟩ is the restriction to ℝ of a function +F that is holomorphic on the open upper half-plane and bounded and continuous on the closed upper +half-plane. + +By `isPositiveEnergy_iff_exists_exp`, V(t) = e^(itA) with A positive and self-adjoint. The matrix +coefficient is a combination of Fourier transforms of the finite measures μ^A_ψₖ +(`exists_inner_expUnitary_eq_sum`), which vanish on (−∞, 0) +(`spectralMeasure_Iio_zero_eq_zero`), and F is the same combination of their Fourier–Laplace +transforms (`fourierLaplace_bounded_continuousOn`, `differentiableOn_fourierLaplace`). + +Implementation note: boundedness is the existence of a constant C with ‖F z‖ ≤ C for Im z ≥ 0, +and the restriction property reads `F t = ⟪χ, V t φ⟫_ℂ` for real t. + +Blueprint: lmm:positive-energy-holomorphic +-/ +theorem IsPositiveEnergy.exists_holomorphic_extension {V : ℝ → (H ≃ₗᵢ[ℂ] H)} + (hV : IsPositiveEnergy V) (χ φ : H) : + ∃ F : ℂ → ℂ, DifferentiableOn ℂ F {z : ℂ | 0 < z.im} ∧ + ContinuousOn F {z : ℂ | 0 ≤ z.im} ∧ + (∃ C : ℝ, ∀ z : ℂ, 0 ≤ z.im → ‖F z‖ ≤ C) ∧ + ∀ t : ℝ, F t = ⟪χ, V t φ⟫_ℂ := by + obtain ⟨A, hA, hpos, hVe⟩ := isPositiveEnergy_iff_exists_exp.1 hV + obtain ⟨ψ, c, hsum⟩ := exists_inner_expUnitary_eq_sum hA χ φ + set μ := Unbounded.spectralMeasure hA + have hν : ∀ k, μ.assoc (ψ k) (Set.Iio 0) = 0 := fun k => by + rw [Unbounded.assoc_apply_eq_norm_sq μ (ψ k) measurableSet_Iio, + spectralMeasure_Iio_zero_eq_zero hA hpos] + simp + refine ⟨fun z => ∑ k, c k * ∫ x : ℝ, Complex.exp (Complex.I * z * x) ∂(μ.assoc (ψ k)), + ?_, ?_, ⟨∑ k, ‖c k‖ * (μ.assoc (ψ k)).real Set.univ, fun z hz => ?_⟩, fun t => ?_⟩ + · exact DifferentiableOn.fun_sum fun k _ => + (differentiableOn_fourierLaplace _ (hν k)).const_mul (c k) + · exact continuousOn_finsetSum _ fun k _ => + ((fourierLaplace_bounded_continuousOn _ (hν k)).2.2).const_smul (c k) + · refine (norm_sum_le _ _).trans (Finset.sum_le_sum fun k _ => ?_) + rw [norm_mul] + exact mul_le_mul_of_nonneg_left ((fourierLaplace_bounded_continuousOn _ (hν k)).2.1 z hz) + (norm_nonneg _) + · simp only [hVe, hsum] + +end AQFT +end Physicslib4 diff --git a/Physicslib4/Analysis/EdgeVanishing.lean b/Physicslib4/Analysis/EdgeVanishing.lean new file mode 100644 index 0000000..d1534c3 --- /dev/null +++ b/Physicslib4/Analysis/EdgeVanishing.lean @@ -0,0 +1,193 @@ +/- +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.Analysis.HorizontalLineRemovable +import Mathlib.Analysis.Analytic.Uniqueness +import Mathlib.Analysis.Complex.CauchyIntegral +import Mathlib.Analysis.Calculus.Deriv.Star + +/-! +# Vanishing on an edge + +A function continuous on the closed upper half-plane, holomorphic on the open upper half-plane, +and zero on a nonempty open interval of the real axis vanishes identically +(`eq_zero_of_eq_zero_on_Ioo`). The proof reflects the function across the interval: the +reflected function g(z) = f(z) for Im z ≥ 0 and g(z) = conj(f(conj z)) for Im z < 0 is +holomorphic on the reflection domain D = {Im z ≠ 0} ∪ I, which is open and connected, and the +identity theorem applies there. This is the uniqueness step of the Reeh–Schlieder theorem. + +## Main results + +* `isOpen_im_ne_zero_union_image_ofReal` — the reflection domain is open. +* `isConnected_im_ne_zero_union_image_ofReal` — the reflection domain is connected. +* `continuousOn_schwarzReflection_of_eq_zero` — the reflected function is continuous on it. +* `differentiableOn_schwarzReflection_of_eq_zero` — the reflected function is holomorphic on it. +* `eq_zero_of_eq_zero_on_Ioo` — vanishing on an edge. + +Throughout, I is a set `I : Set ℝ`. Openness and holomorphy of the reflection need only +`IsOpen I`; continuity needs only that f vanishes on I, and connectedness only that I is +nonempty. The blueprint's open interval is a special case of each. The reflection domain is +written `{z : ℂ | z.im ≠ 0} ∪ Complex.ofReal '' I`, and the +reflected function is written inline as `fun z => if 0 ≤ z.im then f z else conj (f (conj z))`. +-/ + +namespace Physicslib4 + +open Complex ComplexConjugate + +/-- +For an open set I ⊆ ℝ, the reflection domain D = {Im z ≠ 0} ∪ I is open in ℂ. + +Its complement is ℝ \ I, which is closed in ℝ and therefore in ℂ. + +Implementation note: the blueprint's open interval I is a special case of the open set here. + +Blueprint: lmm:reflection-domain-open +-/ +theorem isOpen_im_ne_zero_union_image_ofReal {I : Set ℝ} (hI : IsOpen I) : + IsOpen ({z : ℂ | z.im ≠ 0} ∪ Complex.ofReal '' I) := by + have h : {z : ℂ | z.im ≠ 0} ∪ Complex.ofReal '' I = (Complex.ofReal '' Iᶜ)ᶜ := by + ext z + by_cases hz : z.im = 0 + · have hz' : z = (z.re : ℂ) := Complex.ext rfl (by simp [hz]) + rw [hz'] + simp [Complex.ofReal_injective.eq_iff] + · simp only [Set.mem_union, Set.mem_ofPred_eq, Set.mem_compl_iff, Set.mem_image] + exact ⟨fun _ ⟨x, _, hx⟩ => hz (hx ▸ Complex.ofReal_im x), fun _ => Or.inl hz⟩ + rw [h] + exact (Complex.isometry_ofReal.isClosedEmbedding.isClosedMap _ hI.isClosed_compl).isOpen_compl + +/-- +For a nonempty set I ⊆ ℝ, the reflection domain D = {Im z ≠ 0} ∪ I is connected. + +D is the union of {Im z > 0} ∪ I and {Im z < 0} ∪ I. Each lies between an open half-plane and its +closure, hence is preconnected, and the two share the nonempty set I. + +Implementation note: the blueprint's nonempty open interval I is a special case; connectedness is +Mathlib's `IsConnected`, which includes nonemptiness. + +Blueprint: lmm:reflection-domain-connected +-/ +theorem isConnected_im_ne_zero_union_image_ofReal {I : Set ℝ} (hne : I.Nonempty) : + IsConnected ({z : ℂ | z.im ≠ 0} ∪ Complex.ofReal '' I) := by + obtain ⟨x, hx⟩ := hne + have hxI : (x : ℂ) ∈ Complex.ofReal '' I := ⟨x, hx, rfl⟩ + have hup : IsPreconnected ({z : ℂ | 0 < z.im} ∪ Complex.ofReal '' I) := + (convex_halfSpace_im_gt 0).isPreconnected.subset_closure Set.subset_union_left <| by + rw [closure_setOfPred_lt_im] + rintro z (hz | ⟨r, -, rfl⟩) <;> simp_all [le_of_lt] + have hlo : IsPreconnected ({z : ℂ | z.im < 0} ∪ Complex.ofReal '' I) := + (convex_halfSpace_im_lt 0).isPreconnected.subset_closure Set.subset_union_left <| by + rw [closure_setOfPred_im_lt] + rintro z (hz | ⟨r, -, rfl⟩) <;> simp_all [le_of_lt] + have heq : {z : ℂ | z.im ≠ 0} ∪ Complex.ofReal '' I = + ({z : ℂ | 0 < z.im} ∪ Complex.ofReal '' I) ∪ ({z : ℂ | z.im < 0} ∪ Complex.ofReal '' I) := by + ext z; simp only [Set.mem_union, Set.mem_ofPred_eq, ne_iff_lt_or_gt]; tauto + rw [heq] + exact ⟨⟨x, Or.inl (Or.inr hxI)⟩, hup.union (x : ℂ) (Or.inr hxI) (Or.inr hxI) hlo⟩ + +/-- +If f is continuous on the closed upper half-plane and zero on a set I ⊆ ℝ, the +reflected function g, equal to f on {Im z ≥ 0} and to z ↦ conj(f(conj z)) on {Im z < 0}, is +continuous on the reflection domain D = {Im z ≠ 0} ∪ I. + +On D ∩ {Im z ≥ 0} the function g is f, and on D ∩ {Im z ≤ 0} it agrees with the continuous +function z ↦ conj(f(conj z)), since both vanish on I; the two pieces are relatively closed and +cover D. + +Implementation note: the blueprint's open interval I is a special case of the set here. + +Blueprint: lmm:schwarz-reflection-continuous +-/ +theorem continuousOn_schwarzReflection_of_eq_zero {f : ℂ → ℂ} {I : Set ℝ} + (hf : ContinuousOn f {z : ℂ | 0 ≤ z.im}) + (hzero : ∀ x ∈ I, f x = 0) : + ContinuousOn (fun z : ℂ => if 0 ≤ z.im then f z else conj (f (conj z))) + ({z : ℂ | z.im ≠ 0} ∪ Complex.ofReal '' I) := by + refine ContinuousOn.if (fun z ⟨hz, hzf⟩ => ?_) ?_ ?_ + · rw [Complex.frontier_setOfPred_le_im, Set.mem_ofPred_eq] at hzf + obtain ⟨x, hx, rfl⟩ := hz.resolve_left (not_not.2 hzf) + simp [hzero x hx] + · exact hf.mono fun z hz => + (isClosed_le continuous_const Complex.continuous_im).closure_subset hz.2 + · refine (Complex.continuous_conj.comp_continuousOn + (hf.comp Complex.continuous_conj.continuousOn fun z hz => ?_)).mono fun z hz => hz.2 + simp only [not_le, Complex.closure_setOfPred_im_lt, Set.mem_ofPred_eq] at hz ⊢ + simpa using hz + +/-- +**Schwarz reflection across a zero interval.** If f is continuous on the closed upper +half-plane, holomorphic on the open upper half-plane, and zero on an open set I ⊆ ℝ, the +reflected function g, equal to f on {Im z ≥ 0} and to z ↦ conj(f(conj z)) on {Im z < 0}, is +holomorphic on the reflection domain D = {Im z ≠ 0} ∪ I. + +Off the real axis g is holomorphic, being f or the conjugate reflection of f. It is continuous +on the open set D (`continuousOn_schwarzReflection_of_eq_zero`, +`isOpen_im_ne_zero_union_image_ofReal`), so the horizontal line Im z = 0 is removable +(`differentiableOn_of_continuousOn_off_horizontal_line`). + +Implementation note: the blueprint's open interval I is a special case of the open set here. + +Blueprint: lmm:schwarz-reflection-zero +-/ +theorem differentiableOn_schwarzReflection_of_eq_zero {f : ℂ → ℂ} {I : Set ℝ} + (hI : IsOpen I) (hf : ContinuousOn f {z : ℂ | 0 ≤ z.im}) + (hf' : DifferentiableOn ℂ f {z : ℂ | 0 < z.im}) (hzero : ∀ x ∈ I, f x = 0) : + DifferentiableOn ℂ (fun z : ℂ => if 0 ≤ z.im then f z else conj (f (conj z))) + ({z : ℂ | z.im ≠ 0} ∪ Complex.ofReal '' I) := by + have hU : IsOpen {z : ℂ | 0 < z.im} := isOpen_lt continuous_const Complex.continuous_im + refine differentiableOn_of_continuousOn_off_horizontal_line + (isOpen_im_ne_zero_union_image_ofReal hI) 0 _ + (continuousOn_schwarzReflection_of_eq_zero hf hzero) fun z hz => ?_ + refine DifferentiableAt.differentiableWithinAt ?_ + rcases (show z.im ≠ 0 from hz.2).lt_or_gt with h | h + · have hc := DifferentiableAt.conj_conj + (hf'.differentiableAt (hU.mem_nhds (show 0 < (conj z).im by simpa using h))) + rw [Complex.conj_conj] at hc + refine hc.congr_of_eventuallyEq ?_ + filter_upwards [(isOpen_lt Complex.continuous_im continuous_const).mem_nhds h] with w hw + simp [not_le.2 hw] + · refine (hf'.differentiableAt (hU.mem_nhds h)).congr_of_eventuallyEq ?_ + filter_upwards [hU.mem_nhds h] with w hw + simp [hw.le] + +/-- +**Vanishing on an edge.** A function continuous on the closed upper half-plane, holomorphic on +the open upper half-plane, and zero on a nonempty open interval (a, b) of the real axis vanishes +on the whole closed upper half-plane. + +The reflected function of `differentiableOn_schwarzReflection_of_eq_zero` is analytic on the +open connected reflection domain and vanishes on (a, b), so it vanishes on the domain by the +identity theorem; continuity extends the vanishing of f to the real axis. + +Blueprint: lmm:edge-vanishing +-/ +theorem eq_zero_of_eq_zero_on_Ioo {f : ℂ → ℂ} {a b : ℝ} (hab : a < b) + (hf : ContinuousOn f {z : ℂ | 0 ≤ z.im}) (hf' : DifferentiableOn ℂ f {z : ℂ | 0 < z.im}) + (hzero : ∀ x ∈ Set.Ioo a b, f x = 0) : + ∀ z : ℂ, 0 ≤ z.im → f z = 0 := by + set g : ℂ → ℂ := fun z => if 0 ≤ z.im then f z else conj (f (conj z)) + set m : ℝ := (a + b) / 2 + have hm : m ∈ Set.Ioo a b := ⟨by simp only [m]; linarith, by simp only [m]; linarith⟩ + have hD := isOpen_im_ne_zero_union_image_ofReal (isOpen_Ioo (a := a) (b := b)) + have hfr : ∃ᶠ z in nhdsWithin (m : ℂ) {(m : ℂ)}ᶜ, g z = 0 := by + have ht : Filter.Tendsto Complex.ofReal (nhdsWithin m {m}ᶜ) (nhdsWithin (m : ℂ) {(m : ℂ)}ᶜ) := + tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within _ + (Complex.continuous_ofReal.tendsto' _ _ rfl |>.mono_left nhdsWithin_le_nhds) + (eventually_nhdsWithin_of_forall fun x hx => by simpa using hx) + refine ht.frequently (Filter.Eventually.frequently ?_) + filter_upwards [eventually_nhdsWithin_of_eventually_nhds (Ioo_mem_nhds hm.1 hm.2)] with x hx + simp [g, hzero x hx] + have hgz := ((differentiableOn_schwarzReflection_of_eq_zero isOpen_Ioo hf hf' + hzero).analyticOnNhd hD).eqOn_zero_of_preconnected_of_frequently_eq_zero + (isConnected_im_ne_zero_union_image_ofReal ⟨m, hm⟩).isPreconnected (Or.inr ⟨m, hm, rfl⟩) hfr + have hpos : Set.EqOn f 0 {z : ℂ | 0 < z.im} := fun z (hz : 0 < z.im) => by + simpa [g, hz.le] using hgz (Or.inl (ne_of_gt hz)) + intro z hz + refine Set.EqOn.of_subset_closure hpos hf continuousOn_const + (fun w (hw : 0 < w.im) => hw.le) ?_ hz + rw [closure_setOfPred_lt_im] + +end Physicslib4 diff --git a/blueprint/src/content.tex b/blueprint/src/content.tex index dd43ac6..93cbbc3 100644 --- a/blueprint/src/content.tex +++ b/blueprint/src/content.tex @@ -65,3 +65,4 @@ \chapter{Haag Kastler Axioms Blueprint}\label{chptr:haag-kastler-axioms-blueprin \input{sections/sec10/haag-kastler-axioms} \input{sections/sec10/haag-kastler-axioms-in-curved-spacetime} \input{sections/sec10/general-covariance-in-curved-spacetime} +\input{sections/sec10/reeh-schlieder} diff --git a/blueprint/src/sections/sec10/haag-kastler-axioms.tex b/blueprint/src/sections/sec10/haag-kastler-axioms.tex index 7f7ee52..dbe34ea 100644 --- a/blueprint/src/sections/sec10/haag-kastler-axioms.tex +++ b/blueprint/src/sections/sec10/haag-kastler-axioms.tex @@ -2313,6 +2313,7 @@ \subsection{The KMS Condition and Thermal Equilibrium} \end{theorem} \begin{proof} \leanok + \uses{lmm:horizontal-line-removable} The extension is the $i\beta$-periodic continuation $H(z) = F\!\left(z - \lfloor \operatorname{Im} z / \beta \rfloor\, i\beta\right)$, which folds every point into the fundamental strip: it is continuous across each gluing line $\operatorname{Im} z = k\beta$ because the boundary values match by periodicity, holomorphic off the lines as $F$ composed with a holomorphic shift, and holomorphic on the lines by the horizontal-line removable-singularity theorem (Morera). \end{proof} diff --git a/blueprint/src/sections/sec10/reeh-schlieder.tex b/blueprint/src/sections/sec10/reeh-schlieder.tex new file mode 100644 index 0000000..57d6022 --- /dev/null +++ b/blueprint/src/sections/sec10/reeh-schlieder.tex @@ -0,0 +1,520 @@ +\section{The Reeh--Schlieder Theorem}\label{sctn:reeh-schlieder} + +In a vacuum representation the vacuum vector is cyclic not only for the quasilocal algebra but for the algebra of every nonempty diamond: states prepared by local operations in an arbitrarily small region approximate every state of the theory. The section proves this in two stages. The main theorem, which assumes no additivity property of the net, says that the vectors obtained from a diamond's algebra already approximate those obtained from all translates of a smaller diamond's algebra. Three corollaries then give cyclicity under successively stronger hypotheses: cyclicity for the translation-generated algebras, the von Neumann form of weak additivity, and weak additivity itself. The proof uses the spectrum condition through analytic continuation in one complex variable at a time, along one future-timelike direction at a time, so it needs neither a joint spectral measure for the energy--momentum operators nor any structure beyond the positive energy of \ref{def:positive-energy}. The section concerns Haag--Kastler nets in Minkowski spacetime only. + +\subsection{Analytic Preliminaries} + +The lemmas of this subsection concern a single positive self-adjoint operator and functions of one complex variable; they involve no net. + +\begin{lemma}[A Positive Operator Has No Spectrum in $(-n, -1/n)$] + \label{lmm:positive-spectral-support-interval} + \lean{Physicslib4.AQFT.spectralMeasure_Ioo_neg_eq_zero} + \uses{def:spectral-measure, def:positive-unbounded-operator} + \leanok + Let $A$ be a positive self-adjoint operator with spectral measure $\mu^A$. Then $\mu^A((-n, -1/n)) = 0$ for every integer $n \ge 1$. +\end{lemma} +\begin{proof} + \leanok + \uses{lmm:range-membership-concentrates-measure, lmm:associated-measure-total-mass, prpstn:hall-10.2, def:spectral-measure} + Let $\psi$ be in the range of $\mu^A((-n, -1/n))$. By Lemma~\ref{lmm:range-membership-concentrates-measure}, $\mu^A_\psi$ is concentrated on $(-n, -1/n)$, and it has total mass $\|\psi\|^2$ (Lemma~\ref{lmm:associated-measure-total-mass}). So $\int \lambda^2 \, d\mu^A_\psi \le n^2\|\psi\|^2 < \infty$, that is, $\psi \in \text{Dom}(A)$ (\ref{def:spectral-measure}), and by Proposition~\ref{prpstn:hall-10.2}, $\left< \psi, A\psi \right> = \int \lambda \, d\mu^A_\psi(\lambda) \le -\|\psi\|^2/n$. Positivity of $A$ forces $\psi = 0$. A projection with zero range is zero. +\end{proof} + +\begin{lemma}[Spectral Support of a Positive Operator] + \label{lmm:positive-spectral-support} + \lean{Physicslib4.AQFT.spectralMeasure_Iio_zero_eq_zero} + \uses{def:spectral-measure, def:positive-unbounded-operator} + \leanok + The spectral measure $\mu^A$ of a positive self-adjoint operator $A$ satisfies $\mu^A((-\infty, 0)) = 0$. +\end{lemma} +\begin{proof} + \leanok + \uses{lmm:positive-spectral-support-interval, thrm:projection-valued-measures-associated-measure, def:projection-valued-measure} + Let $\psi \in H$. The scalar measure $\mu^A_\psi(E) = \left< \psi, \mu^A(E)\psi \right>$ is a positive measure (Theorem~\ref{thrm:projection-valued-measures-associated-measure}), and $\mu^A_\psi((-n, -1/n)) = 0$ for every $n \ge 1$ by Lemma~\ref{lmm:positive-spectral-support-interval}. The intervals $(-n, -1/n)$ increase to $(-\infty, 0)$, so continuity of measures from below (in Mathlib, \texttt{tendsto\_measure\_iUnion\_atTop}) gives $\mu^A_\psi((-\infty, 0)) = 0$. Since $P = \mu^A((-\infty, 0))$ is an orthogonal projection (\ref{def:projection-valued-measure}), $\|P\psi\|^2 = \left< \psi, P\psi \right> = \mu^A_\psi((-\infty, 0)) = 0$. So $P\psi = 0$ for every $\psi$, and $P = 0$. +\end{proof} + +\begin{lemma}[Matrix Coefficients of $e^{itA}$ by Polarization] + \label{lmm:exp-matrix-coefficient-polarization} + \lean{Physicslib4.AQFT.exists_inner_expUnitary_eq_sum} + \uses{def:exp-unitary-group, def:spectral-measure} + \leanok + Let $A$ be a self-adjoint operator on $H$ and $\chi, \varphi \in H$. There are vectors $\psi_0, \dots, \psi_3 \in H$ and constants $c_0, \dots, c_3 \in \mathbb{C}$, independent of $t$, with + \begin{align} + \left< \chi, e^{itA}\varphi \right> = \sum_{k=0}^{3} c_k \int_{\mathbb{R}} e^{it\lambda} \, d\mu^A_{\psi_k}(\lambda) \qquad \text{for all } t \in \mathbb{R}. + \end{align} +\end{lemma} +\begin{proof} + \leanok + \uses{thrm:operator-valued-integration, def:exp-unitary-group} + Take $\psi_k = \chi + i^k\varphi$ and the constants of the polarization identity, which writes $\left< \chi, T\varphi \right>$ as a fixed combination of the diagonal terms $\left< \psi_k, T\psi_k \right>$ for any bounded $T$. For $T = e^{itA} = \int e^{it\lambda} \, d\mu^A$ (\ref{def:exp-unitary-group}), each diagonal term is $\int e^{it\lambda} \, d\mu^A_{\psi_k}$ by Theorem~\ref{thrm:operator-valued-integration}. +\end{proof} + +\begin{lemma}[Boundedness and Continuity of the Fourier--Laplace Transform] + \label{lmm:fourier-laplace-continuous} + \lean{Physicslib4.AQFT.fourierLaplace_bounded_continuousOn} + \leanok + Let $\nu$ be a finite positive Borel measure on $\mathbb{R}$ with $\nu((-\infty, 0)) = 0$, and let $G(z) = \int e^{iz\lambda} \, d\nu(\lambda)$. Then $G$ is defined, bounded by $\nu(\mathbb{R})$, and continuous on $\{\operatorname{Im} z \ge 0\}$. +\end{lemma} +\begin{proof} + \leanok + For $\lambda \ge 0$ and $\operatorname{Im} z \ge 0$, $\lvert e^{iz\lambda} \rvert = e^{-\lambda \operatorname{Im} z} \le 1$, and $\nu$ is carried by $[0, \infty)$. So the integrand is dominated by the $\nu$-integrable constant $1$, which gives the bound, and continuity follows by dominated convergence since $z \mapsto e^{iz\lambda}$ is continuous. +\end{proof} + +\begin{lemma}[Holomorphy of the Fourier--Laplace Transform] + \label{lmm:fourier-laplace-holomorphic} + \lean{Physicslib4.AQFT.differentiableOn_fourierLaplace} + \leanok + Let $\nu$ and $G$ be as in Lemma~\ref{lmm:fourier-laplace-continuous}. Then $G$ is holomorphic on $\{\operatorname{Im} z > 0\}$. +\end{lemma} +\begin{proof} + \leanok + Fix $z_0$ with $\operatorname{Im} z_0 > 0$ and let $\delta = \operatorname{Im} z_0 / 2$. On the neighbourhood $\{\operatorname{Im} z > \delta\}$ of $z_0$ the $z$-derivative of the integrand is $i\lambda e^{iz\lambda}$, and for $\lambda \ge 0$, $\lvert i\lambda e^{iz\lambda} \rvert \le \lambda e^{-\lambda\delta} \le 1/(e\delta)$, a $\nu$-integrable constant. Differentiation under the integral sign (in Mathlib, \texttt{hasDerivAt\_integral\_of\_dominated\_loc\_of\_deriv\_le}) gives complex differentiability at $z_0$. +\end{proof} + +\begin{lemma}[Holomorphic Extension under Positive Energy] + \label{lmm:positive-energy-holomorphic} + \lean{Physicslib4.AQFT.IsPositiveEnergy.exists_holomorphic_extension} + \uses{def:positive-energy} + \leanok + Let $V$ be a family of unitary operators on $H$, indexed by $\mathbb{R}$, with positive energy, and let $\chi, \varphi \in H$. Then $t \mapsto \left< \chi, V(t)\varphi \right>$ is the restriction to $\mathbb{R}$ of a function that is holomorphic on $\{\operatorname{Im} z > 0\}$ and bounded and continuous on $\{\operatorname{Im} z \ge 0\}$. +\end{lemma} +\begin{proof} + \leanok + \uses{thrm:positive-energy-iff-exp, lmm:exp-matrix-coefficient-polarization, lmm:positive-spectral-support, lmm:associated-measure-total-mass, lmm:fourier-laplace-continuous, lmm:fourier-laplace-holomorphic} + By Theorem~\ref{thrm:positive-energy-iff-exp}, $V(t) = e^{itA}$ with $A$ positive and self-adjoint. By Lemma~\ref{lmm:exp-matrix-coefficient-polarization}, $\left< \chi, V(t)\varphi \right> = \sum_k c_k \int e^{it\lambda} \, d\mu^A_{\psi_k}$. Each $\mu^A_{\psi_k}$ is finite (Lemma~\ref{lmm:associated-measure-total-mass}) and vanishes on $(-\infty, 0)$ (Lemma~\ref{lmm:positive-spectral-support}). The function $\sum_k c_k G_k(z)$, with $G_k$ the Fourier--Laplace transform of $\mu^A_{\psi_k}$, has the required properties by Lemmas~\ref{lmm:fourier-laplace-continuous} and~\ref{lmm:fourier-laplace-holomorphic}. +\end{proof} + +\begin{lemma}[Removability of a Horizontal Line] + \label{lmm:horizontal-line-removable} + \lean{Physicslib4.differentiableOn_of_continuousOn_off_horizontal_line} + \leanok + Let $U \subseteq \mathbb{C}$ be open, $\ell \in \mathbb{R}$, and $f$ a function on $U$ with values in a complex Banach space. If $f$ is continuous on $U$ and complex-differentiable on $U \setminus \{\operatorname{Im} z = \ell\}$, then $f$ is complex-differentiable on $U$. +\end{lemma} +\begin{proof} + \leanok + By Morera's theorem (in Mathlib, \texttt{Complex.isConservativeOn\_and\_continuousOn\_iff\_isDifferentiableOn}) it suffices that the integral of $f$ around the boundary of every rectangle in $U$ vanishes. For a rectangle meeting the line, split it along the line and approximate each half by rectangles off the line; the integrals over those vanish by the Cauchy--Goursat theorem, and continuity of $f$ passes to the limit. +\end{proof} + +\begin{lemma}[The Reflection Domain is Open] + \label{lmm:reflection-domain-open} + \lean{Physicslib4.isOpen_im_ne_zero_union_image_ofReal} + \leanok + For an open interval $I \subseteq \mathbb{R}$, the set $D = \{\operatorname{Im} z \ne 0\} \cup I$ is open in $\mathbb{C}$. +\end{lemma} +\begin{proof} + \leanok + $D$ is the complement of $\mathbb{R} \setminus I$, which is closed in $\mathbb{R}$ and hence in $\mathbb{C}$, since $\mathbb{R}$ is closed in $\mathbb{C}$. +\end{proof} + +\begin{lemma}[The Reflection Domain is Connected] + \label{lmm:reflection-domain-connected} + \lean{Physicslib4.isConnected_im_ne_zero_union_image_ofReal} + \leanok + For a nonempty open interval $I \subseteq \mathbb{R}$, the set $D = \{\operatorname{Im} z \ne 0\} \cup I$ is connected. +\end{lemma} +\begin{proof} + \leanok + $D = S_+ \cup S_-$ with $S_+ = \{\operatorname{Im} z > 0\} \cup I$ and $S_- = \{\operatorname{Im} z < 0\} \cup I$. Each is convex: a segment between two points of $I$ stays in the interval $I$, and a segment with an endpoint off the real axis has all its other points strictly on that endpoint's side. Convex sets are preconnected (in Mathlib, \texttt{Convex.isPreconnected}), and two preconnected sets sharing the nonempty set $I$ have preconnected union (\texttt{IsPreconnected.union}). +\end{proof} + +\begin{lemma}[Continuity of the Reflected Function] + \label{lmm:schwarz-reflection-continuous} + \lean{Physicslib4.continuousOn_schwarzReflection_of_eq_zero} + \leanok + Let $f$ be continuous on $\{\operatorname{Im} z \ge 0\}$ and zero on an open interval $I \subseteq \mathbb{R}$. Let $g(z) = f(z)$ for $\operatorname{Im} z \ge 0$ and $g(z) = \overline{f(\bar z)}$ for $\operatorname{Im} z < 0$. Then $g$ is continuous on $D = \{\operatorname{Im} z \ne 0\} \cup I$. +\end{lemma} +\begin{proof} + \leanok + $D$ is covered by the two pieces $D \cap \{\operatorname{Im} z \ge 0\}$ and $D \cap \{\operatorname{Im} z \le 0\}$, each closed in $D$. On the first, $g = f$ is continuous. On the second, $g$ agrees with the continuous function $z \mapsto \overline{f(\bar z)}$: off the axis by definition, and on $I$ because there both equal $0$. A function continuous on each of two relatively closed pieces covering $D$ is continuous on $D$. +\end{proof} + +\begin{lemma}[Schwarz Reflection across a Zero Interval] + \label{lmm:schwarz-reflection-zero} + \lean{Physicslib4.differentiableOn_schwarzReflection_of_eq_zero} + \uses{lmm:horizontal-line-removable} + \leanok + Let $f$ be continuous on $\{\operatorname{Im} z \ge 0\}$, holomorphic on $\{\operatorname{Im} z > 0\}$, and zero on an open interval $I \subseteq \mathbb{R}$. Let $g(z) = f(z)$ for $\operatorname{Im} z \ge 0$ and $g(z) = \overline{f(\bar z)}$ for $\operatorname{Im} z < 0$. Then $g$ is holomorphic on $D = \{\operatorname{Im} z \ne 0\} \cup I$. +\end{lemma} +\begin{proof} + \leanok + \uses{lmm:horizontal-line-removable, lmm:reflection-domain-open, lmm:schwarz-reflection-continuous} + Off the real axis $g$ is holomorphic: on the upper half-plane it is $f$, and on the lower half-plane it is the conjugate reflection of a holomorphic function (in Mathlib, \texttt{DifferentiableAt.conj\_conj}). $g$ is continuous on $D$ by Lemma~\ref{lmm:schwarz-reflection-continuous}, and $D$ is open by Lemma~\ref{lmm:reflection-domain-open}. Lemma~\ref{lmm:horizontal-line-removable} with $\ell = 0$ gives holomorphy on all of $D$. +\end{proof} + +\begin{lemma}[Vanishing on an Edge] + \label{lmm:edge-vanishing} + \lean{Physicslib4.eq_zero_of_eq_zero_on_Ioo} + \leanok + Let $f$ be continuous on the closed upper half-plane $\{\operatorname{Im} z \ge 0\}$, holomorphic on the open upper half-plane, and zero on a nonempty open interval $I = (a, b)$, $a < b$, of the real axis. Then $f$ vanishes on the closed upper half-plane. +\end{lemma} +\begin{proof} + \leanok + \uses{lmm:schwarz-reflection-zero, lmm:reflection-domain-open, lmm:reflection-domain-connected} + The reflected function $g$ of Lemma~\ref{lmm:schwarz-reflection-zero} is holomorphic, hence analytic (in Mathlib, \texttt{DifferentiableOn.analyticOnNhd}), on the set $D$, which is open and connected (Lemmas~\ref{lmm:reflection-domain-open} and~\ref{lmm:reflection-domain-connected}). It vanishes on $I$, so every point of $I$ is an accumulation point of zeros, and the identity theorem (\texttt{AnalyticOnNhd.eqOn\_zero\_of\_preconnected\_of\_frequently\_eq\_zero}) gives $g = 0$ on $D$. Hence $f = 0$ on the open upper half-plane, and on its closure by continuity. +\end{proof} + +\subsection{The Theorem and its Corollaries} + +Throughout, $\mathfrak{U}$ is the quasilocal algebra of a Haag--Kastler net with embeddings $\iota_{\mathbf{B}} : \mathfrak{U}(\mathbf{B}) \to \mathfrak{U}$ (\ref{def:quasilocal-algebra}) and covariance action $L \mapsto \beta_L$ (\ref{def:covariant-quasilocal-algebra}). A \emph{diamond} is an Alexandrov basis set $I^+(p) \cap I^-(q)$ (\ref{def:causal-diamond}); the empty set is one. Axiom 1 assigns the empty diamond the trivial algebra $\mathbb{C}\mathbf{1}$, and every translate of the empty set is empty, so its translation-generated algebra is $\mathbb{C}\mathbf{1}$; the additivity conditions and the cyclicity statements below therefore quantify over nonempty diamonds. For $x \in \mathbb{R}^4$ we write $\beta_x = \beta_{\mathrm{translationSub}(x)}$ for the translation automorphism and $\mathbf{B} + x = \mathrm{translationSub}(x) \cdot \mathbf{B}$ for the translate of a diamond, again a diamond (\ref{def:future-timelike-translation}). A family of unitaries indexed by translations is written $x \mapsto U(x)$, and a \emph{future-timelike translation subgroup} of it is $t \mapsto U(tn)$ with $n$ future-pointing timelike. For a $*$-representation $\pi$ of $\mathfrak{U}$ on $H$, $\pi(\mathfrak{U}(\mathbf{B}))$ is the set of local observable operators of \ref{def:local-von-neumann}. + +\begin{definition}[Translation-Generated Algebra] + \label{def:translation-generated-algebra} + \lean{Physicslib4.AQFT.HaagKastler.HaagKastlerNet.translationGeneratedAlgebra} + \uses{def:covariant-quasilocal-algebra, def:causal-diamond, def:future-timelike-translation} + \leanok + For a diamond $\mathbf{B}$, $\mathfrak{A}_{\mathbf{B}}$ is the C*-subalgebra of the quasilocal algebra $\mathfrak{U}$ generated by the translates $\iota_{\mathbf{B}+x}(\mathfrak{U}(\mathbf{B}+x))$, $x \in \mathbb{R}^4$: the norm closure of the $*$-algebra they generate. +\end{definition} + +\begin{definition}[Weak Additivity] + \label{def:weak-additivity} + \lean{Physicslib4.AQFT.HaagKastler.HaagKastlerNet.IsWeaklyAdditive} + \uses{def:translation-generated-algebra} + \leanok + A Haag--Kastler net is \emph{weakly additive} if $\mathfrak{A}_{\mathbf{B}} = \mathfrak{U}$ for every nonempty diamond $\mathbf{B}$. +\end{definition} + +\begin{definition}[Weak Additivity, von Neumann Form] + \label{def:weak-additivity-von-neumann} + \lean{Physicslib4.AQFT.HaagKastler.HaagKastlerNet.IsWeaklyAdditiveVonNeumann} + \uses{def:translation-generated-algebra} + \leanok + A $*$-representation $\pi$ of $\mathfrak{U}$ satisfies \emph{weak additivity in the von Neumann sense} if $\pi(\mathfrak{U}) \subseteq \pi(\mathfrak{A}_{\mathbf{B}})''$ for every nonempty diamond $\mathbf{B}$, the commutant being taken in $\mathcal{B}(H)$. +\end{definition} + +\begin{lemma}[Weak Additivity Implies the von Neumann Form] + \label{lmm:weak-additivity-von-neumann} + \lean{Physicslib4.AQFT.HaagKastler.HaagKastlerNet.IsWeaklyAdditive.isWeaklyAdditiveVonNeumann} + \uses{def:weak-additivity, def:weak-additivity-von-neumann} + \leanok + If the net is weakly additive, every $*$-representation of $\mathfrak{U}$ satisfies weak additivity in the von Neumann sense. +\end{lemma} +\begin{proof} + \leanok + \uses{def:weak-additivity, def:weak-additivity-von-neumann} + For a nonempty diamond $\mathbf{B}$, $\pi(\mathfrak{U}) = \pi(\mathfrak{A}_{\mathbf{B}}) \subseteq \pi(\mathfrak{A}_{\mathbf{B}})''$, since every set lies in its bicommutant. +\end{proof} + +\begin{lemma}[Translate of a Diamond] + \label{lmm:diamond-translate} + \lean{Physicslib4.AQFT.HaagKastler.translationSub_smul_diamond} + \uses{def:causal-diamond, def:future-timelike-translation} + \leanok + For all $p, q, x \in \mathbb{R}^4$, $\mathrm{translationSub}(x) \cdot (I^+(p) \cap I^-(q)) = I^+(p + x) \cap I^-(q + x)$. +\end{lemma} +\begin{proof} + \leanok + \uses{def:inhomogeneous-lorentz-group, lmm:minkowski-chronological-open} + $\mathrm{translationSub}(x) = (\mathrm{id}, x)$ acts on points by $y \mapsto y + x$, by the affine action $(L, a) \cdot y = Ly + a$ of \ref{def:inhomogeneous-lorentz-group}. On standard Minkowski spacetime $a \ll b$ says that $b - a$ lies in the open forward cone (\ref{lmm:minkowski-chronological-open}), which is unchanged when $a$ and $b$ are both translated by $x$. So $y \in I^+(p) \cap I^-(q)$ if and only if $y + x \in I^+(p + x) \cap I^-(q + x)$. +\end{proof} + +\begin{lemma}[Translates of a Smaller Diamond] + \label{lmm:diamond-small-translates} + \lean{Physicslib4.AQFT.HaagKastler.exists_diamond_translate_subset} + \uses{def:causal-diamond, def:future-timelike-translation} + \leanok + For every nonempty diamond $\mathbf{B}$ there are a nonempty diamond $\mathbf{B}_1$ and an open neighbourhood $V$ of $0$ in $\mathbb{R}^4$ with $\mathbf{B}_1 + x \subseteq \mathbf{B}$ for every $x \in V$. +\end{lemma} +\begin{proof} + \leanok + \uses{lmm:diamond-translate, thrm:precedence-transitive, lmm:minkowski-future-between, lmm:minkowski-chronological-open} + Write $\mathbf{B} = I^+(p) \cap I^-(q)$; it is nonempty, so $p \ll q$ by transitivity of $\ll$ (\ref{thrm:precedence-transitive}). Lemma~\ref{lmm:minkowski-future-between}, applied twice, gives $p \ll p' \ll q' \ll q$; take $\mathbf{B}_1 = I^+(p') \cap I^-(q')$, nonempty by the same lemma applied to $p' \ll q'$. Since $I^+(p)$ and $I^-(q)$ are open (\ref{lmm:minkowski-chronological-open}), there is an open neighbourhood $V$ of $0$ with $p \ll p' + x$ and $q' + x \ll q$ for $x \in V$. For such $x$, $\mathbf{B}_1 + x = I^+(p'+x) \cap I^-(q'+x) \subseteq \mathbf{B}$ by Lemma~\ref{lmm:diamond-translate} and transitivity of $\ll$. +\end{proof} + +\begin{lemma}[Spreading Along One Timelike Direction] + \label{lmm:timelike-spreading-direction} + \lean{Physicslib4.AQFT.HaagKastler.inner_translation_eq_zero_add_smul} + \uses{def:positive-energy, def:future-timelike-translation} + \leanok + Let $x \mapsto U(x)$ be unitaries on $H$ indexed by the translations $\mathbb{R}^4$, and $K_0 \subseteq H$ a closed subspace invariant under every $U(x)$, on which $U(x+y) = U(x)U(y)$. Let $n$ be future-pointing timelike with $t \mapsto U(tn)$ of positive energy, $\chi \in H$ and $\varphi \in K_0$. If $h(x) = \left< \chi, U(x)\varphi \right>$ vanishes on an open set $W$, it vanishes on $W + \mathbb{R}n$. +\end{lemma} +\begin{proof} + \leanok + \uses{lmm:positive-energy-holomorphic, lmm:edge-vanishing} + Let $v \in W$. Since $\varphi \in K_0$, $h(v + tn) = \left< \chi, U(tn)U(v)\varphi \right>$, which vanishes for $t$ in a nonempty open interval around $0$ because $W$ is open. By Lemma~\ref{lmm:positive-energy-holomorphic} it is the boundary value of a function holomorphic on the upper half-plane and continuous on its closure, so by Lemma~\ref{lmm:edge-vanishing} it vanishes for all $t$. +\end{proof} + +\begin{lemma}[A Basis of Future-Timelike Vectors] + \label{lmm:future-timelike-basis} + \lean{Physicslib4.AQFT.HaagKastler.futureTimelike_basis} + \uses{def:future-timelike-translation} + \leanok + The vectors $n_0 = e_0$ and $n_i = e_0 + \tfrac{1}{2}e_i$, $i = 1, 2, 3$, are future-pointing timelike and form a basis of $\mathbb{R}^4$. +\end{lemma} +\begin{proof} + \leanok + Each has time component $1 > 0$ and spatial length at most $\tfrac{1}{2} < 1$, so lies in the open forward cone. They span, since $e_i = 2(n_i - n_0)$, and four spanning vectors in $\mathbb{R}^4$ form a basis. +\end{proof} + +\begin{lemma}[Spreading Along Timelike Directions] + \label{lmm:timelike-spreading} + \lean{Physicslib4.AQFT.HaagKastler.inner_translation_eq_zero} + \uses{def:positive-energy, def:future-timelike-translation} + \leanok + Let $U$ and $K_0$ be as in Lemma~\ref{lmm:timelike-spreading-direction}, and suppose every future-timelike translation subgroup $t \mapsto U(tn)$ has positive energy. If $\chi \in H$, $\varphi \in K_0$, and $x \mapsto \left< \chi, U(x)\varphi \right>$ vanishes on a nonempty open set $W$, it vanishes identically. +\end{lemma} +\begin{proof} + \leanok + \uses{lmm:timelike-spreading-direction, lmm:future-timelike-basis} + Apply Lemma~\ref{lmm:timelike-spreading-direction} successively with $n_0, \dots, n_3$ of Lemma~\ref{lmm:future-timelike-basis}; each set $W + \mathbb{R}n_0 + \dots + \mathbb{R}n_j$ is open, being a union of translates of $W$. The final set is $W + \mathbb{R}^4 = \mathbb{R}^4$, since the $n_j$ form a basis and $W$ is nonempty. +\end{proof} + +\begin{lemma}[Agreement on the Cyclic Subspace] + \label{lmm:agree-on-cyclic-subspace} + \lean{Physicslib4.AQFT.HaagKastler.apply_eq_of_mem_cyclicSubspace} + \leanok + Let $\pi$ be a $*$-representation of $\mathfrak{U}$ on $H$, $\Omega \in H$, and $K_0$ the closure of $\pi(\mathfrak{U})\Omega$. Bounded operators $S, T$ on $H$ with $S\pi(a)\Omega = T\pi(a)\Omega$ for every $a \in \mathfrak{U}$ agree on $K_0$. +\end{lemma} +\begin{proof} + \leanok + $\{\xi : S\xi = T\xi\}$ is closed, since $S - T$ is continuous, and contains $\pi(\mathfrak{U})\Omega$. +\end{proof} + +\begin{lemma}[The Cyclic Subspace is Invariant] + \label{lmm:translations-cyclic-subspace-invariant} + \lean{Physicslib4.AQFT.HaagKastler.translations_cyclicSubspace_invariant} + \uses{def:covariant-quasilocal-algebra, def:future-timelike-translation} + \leanok + Let $\pi$ be a $*$-representation of $\mathfrak{U}$ on $H$, $\Omega \in H$, and $x \mapsto U(x)$ unitaries with $U(x)\pi(a)\Omega = \pi(\beta_x a)\Omega$ for all translations $x$ and all $a \in \mathfrak{U}$. Let $K_0$ be the closure of $\pi(\mathfrak{U})\Omega$. Then $U(x)\Omega = \Omega$, and $K_0$ is invariant under every $\pi(a)$ and every $U(x)$. +\end{lemma} +\begin{proof} + \leanok + Take $a = 1$: $U(x)\Omega = \pi(\beta_x 1)\Omega = \Omega$. The operators $\pi(a)$ and $U(x)$ map $\pi(\mathfrak{U})\Omega$ into itself, since $\pi(a)\pi(b)\Omega = \pi(ab)\Omega$ and $U(x)\pi(b)\Omega = \pi(\beta_x b)\Omega$; being continuous, they map its closure $K_0$ into $K_0$. +\end{proof} + +\begin{lemma}[Intertwining on the Cyclic Subspace] + \label{lmm:translations-intertwine-cyclic-subspace} + \lean{Physicslib4.AQFT.HaagKastler.translations_intertwine_cyclicSubspace} + \uses{lmm:translations-cyclic-subspace-invariant} + \leanok + Under the hypotheses of Lemma~\ref{lmm:translations-cyclic-subspace-invariant}, $U(x)\pi(a) = \pi(\beta_x a)U(x)$ on $K_0$ for every translation $x$ and every $a \in \mathfrak{U}$. +\end{lemma} +\begin{proof} + \leanok + \uses{lmm:agree-on-cyclic-subspace} + On $\pi(b)\Omega$, $U(x)\pi(a)\pi(b)\Omega = \pi(\beta_x(ab))\Omega = \pi(\beta_x a)\pi(\beta_x b)\Omega = \pi(\beta_x a)U(x)\pi(b)\Omega$, as $\beta_x$ is multiplicative. Lemma~\ref{lmm:agree-on-cyclic-subspace} extends this to $K_0$. +\end{proof} + +\begin{lemma}[Group Law on the Cyclic Subspace] + \label{lmm:translations-group-law-cyclic-subspace} + \lean{Physicslib4.AQFT.HaagKastler.translations_add_cyclicSubspace} + \uses{lmm:translations-cyclic-subspace-invariant} + \leanok + Under the hypotheses of Lemma~\ref{lmm:translations-cyclic-subspace-invariant}, $U(x+y) = U(x)U(y)$ on $K_0$ for all translations $x, y$. +\end{lemma} +\begin{proof} + \leanok + \uses{lmm:agree-on-cyclic-subspace, lmm:quasilocal-action-coherence, def:future-timelike-translation} + Since $\mathrm{translationSub}(x+y) = \mathrm{translationSub}(x)\,\mathrm{translationSub}(y)$ (\ref{def:future-timelike-translation}) and $\beta$ is a group action (\ref{lmm:quasilocal-action-coherence}), $\beta_{x+y} = \beta_x\beta_y$. So $U(x+y)\pi(a)\Omega = \pi(\beta_x\beta_y a)\Omega = U(x)\pi(\beta_y a)\Omega = U(x)U(y)\pi(a)\Omega$, and Lemma~\ref{lmm:agree-on-cyclic-subspace} extends this to $K_0$. +\end{proof} + +\begin{lemma}[Translations on the Cyclic Subspace] + \label{lmm:covariant-translations-cyclic-subspace} + \lean{Physicslib4.AQFT.HaagKastler.covariant_translations_cyclicSubspace} + \uses{def:covariant-quasilocal-algebra, def:future-timelike-translation} + \leanok + Let $\pi$ be a $*$-representation of $\mathfrak{U}$ on $H$, $\Omega \in H$, and $x \mapsto U(x)$ unitaries with $U(x)\pi(a)\Omega = \pi(\beta_x a)\Omega$ for all translations $x$ and all $a \in \mathfrak{U}$. Let $K_0$ be the closure of $\pi(\mathfrak{U})\Omega$. Then $U(x)\Omega = \Omega$; $K_0$ is invariant under every $\pi(a)$ and $U(x)$; and on $K_0$, $U(x)\pi(a) = \pi(\beta_x a)U(x)$ and $U(x+y) = U(x)U(y)$. +\end{lemma} +\begin{proof} + \leanok + \uses{lmm:translations-cyclic-subspace-invariant, lmm:translations-intertwine-cyclic-subspace, lmm:translations-group-law-cyclic-subspace} + The conjunction of Lemmas~\ref{lmm:translations-cyclic-subspace-invariant}, \ref{lmm:translations-intertwine-cyclic-subspace} and~\ref{lmm:translations-group-law-cyclic-subspace}. +\end{proof} + +\begin{lemma}[Translated Products] + \label{lmm:reeh-schlieder-translated-products} + \lean{Physicslib4.AQFT.HaagKastler.translated_products_apply} + \uses{lmm:covariant-translations-cyclic-subspace, def:future-timelike-translation} + \leanok + Under the hypotheses of Lemma~\ref{lmm:covariant-translations-cyclic-subspace}, for $a_1, \dots, a_n \in \mathfrak{U}$ and $\xi_1, \dots, \xi_n \in \mathbb{R}^4$, + \begin{align} + U(\xi_1)\pi(a_1)U(\xi_2)\pi(a_2) \cdots U(\xi_n)\pi(a_n)\Omega = \pi(\beta_{x_1}a_1 \, \beta_{x_2}a_2 \cdots \beta_{x_n}a_n)\Omega, \qquad x_k = \xi_1 + \dots + \xi_k. + \end{align} +\end{lemma} +\begin{proof} + \leanok + \uses{lmm:quasilocal-action-coherence, def:future-timelike-translation} + Induction on $n$, peeling off the leftmost pair. For $n = 1$ this is the hypothesis. For $n > 1$, the induction hypothesis applied to $a_2, \dots, a_n$ and $\xi_2, \dots, \xi_n$ writes the vector to the right of $U(\xi_1)\pi(a_1)$ as $\pi(b)\Omega$ with $b = \beta_{\xi_2}a_2 \cdots \beta_{\xi_2 + \dots + \xi_n}a_n$. Then $U(\xi_1)\pi(a_1 b)\Omega = \pi(\beta_{\xi_1}a_1 \, \beta_{\xi_1}b)\Omega$, and $\beta_{\xi_1}\beta_y = \beta_{\xi_1 + y}$ (\ref{lmm:quasilocal-action-coherence}, with $\mathrm{translationSub}(\xi_1 + y) = \mathrm{translationSub}(\xi_1)\,\mathrm{translationSub}(y)$) gives the claim. +\end{proof} + +\begin{lemma}[Translates of a Local Subalgebra] + \label{lmm:translate-local-subalgebra} + \lean{Physicslib4.AQFT.HaagKastler.action_translationSub_image_range_ι} + \uses{def:covariant-quasilocal-algebra, def:future-timelike-translation} + \leanok + For diamonds $\mathbf{B}_1, \mathbf{B}$ and $x \in \mathbb{R}^4$, $\beta_x\,\iota_{\mathbf{B}_1}(\mathfrak{U}(\mathbf{B}_1)) = \iota_{\mathbf{B}_1 + x}(\mathfrak{U}(\mathbf{B}_1 + x))$, and if $\mathbf{B}_1 + x \subseteq \mathbf{B}$ this set is contained in $\iota_{\mathbf{B}}(\mathfrak{U}(\mathbf{B}))$. +\end{lemma} +\begin{proof} + \leanok + \uses{def:quasilocal-lift, def:quasilocal-algebra, def:lorentz-covariance} + By \ref{def:quasilocal-lift}, $\beta_x\,\iota_{\mathbf{B}_1}(c) = \iota_{\mathbf{B}_1 + x}(\alpha_x c)$, and $\alpha_x : \mathfrak{U}(\mathbf{B}_1) \to \mathfrak{U}(\mathbf{B}_1 + x)$ is a $*$-isomorphism (\ref{def:lorentz-covariance}), so the two sets agree. If $\mathbf{B}_1 + x \subseteq \mathbf{B}$, the cocone condition $\iota_{\mathbf{B}} \circ i_{\mathbf{B}_1 + x,\,\mathbf{B}} = \iota_{\mathbf{B}_1 + x}$ of \ref{def:quasilocal-algebra} gives the inclusion. +\end{proof} + +\begin{lemma}[Small Partial Sums] + \label{lmm:neighbourhood-partial-sums} + \lean{Physicslib4.AQFT.HaagKastler.exists_isOpen_sum_mem_of_mem_nhds} + \leanok + For every neighbourhood $V$ of $0$ in $\mathbb{R}^4$ and every $n \ge 1$ there is an open neighbourhood $V_0$ of $0$ such that $\xi_1 + \dots + \xi_k \in V$ whenever $1 \le k \le n$ and $\xi_1, \dots, \xi_k \in V_0$. +\end{lemma} +\begin{proof} + \leanok + Take $V_0$ the open ball of radius $r/n$, where the ball of radius $r$ lies in $V$: a sum of $k \le n$ vectors of norm less than $r/n$ has norm less than $r$. +\end{proof} + +\begin{lemma}[Correlation Functions Vanish near the Origin] + \label{lmm:reeh-schlieder-vanishing-near-origin} + \lean{Physicslib4.AQFT.HaagKastler.inner_translated_products_eq_zero_of_mem} + \uses{lmm:covariant-translations-cyclic-subspace, def:local-von-neumann} + \leanok + Let $\pi$, $\Omega$ and $U$ be as in Lemma~\ref{lmm:covariant-translations-cyclic-subspace}. Let $\mathbf{B}_1$ and $\mathbf{B}$ be diamonds with $\mathbf{B}_1 + x \subseteq \mathbf{B}$ for every $x$ in an open neighbourhood $V$ of $0$, let $\psi \in H$ be orthogonal to $\pi(\mathfrak{U}(\mathbf{B}))\Omega$, and let $a_1, \dots, a_n \in \iota_{\mathbf{B}_1}(\mathfrak{U}(\mathbf{B}_1))$. Write + \begin{align} + F(\xi_1, \dots, \xi_n) = \left< \psi, U(\xi_1)\pi(a_1)U(\xi_2)\pi(a_2) \cdots U(\xi_n)\pi(a_n)\Omega \right>. + \end{align} + Let $V_0 \subseteq \mathbb{R}^4$ be an open set such that every partial sum $\xi_1 + \dots + \xi_k$, $k \le n$, of elements of $V_0$ lies in $V$. Then $F = 0$ whenever $\xi_1, \dots, \xi_n \in V_0$. +\end{lemma} +\begin{proof} + \leanok + \uses{lmm:reeh-schlieder-translated-products, lmm:translate-local-subalgebra} + By Lemma~\ref{lmm:reeh-schlieder-translated-products}, $F = \left< \psi, \pi(\beta_{x_1}a_1 \cdots \beta_{x_n}a_n)\Omega \right>$ with $x_k = \xi_1 + \dots + \xi_k$, which lies in $V$ by the choice of $V_0$. By Lemma~\ref{lmm:translate-local-subalgebra} each factor lies in the subalgebra $\iota_{\mathbf{B}}(\mathfrak{U}(\mathbf{B}))$, so the product does, and $F = 0$ by the choice of $\psi$. +\end{proof} + +\begin{lemma}[Factorization in One Variable] + \label{lmm:reeh-schlieder-factorization} + \lean{Physicslib4.AQFT.HaagKastler.inner_translated_products_update_eq_inner} + \uses{lmm:covariant-translations-cyclic-subspace} + \leanok + In the setting of Lemma~\ref{lmm:reeh-schlieder-vanishing-near-origin}, fix $1 \le k \le n$ and all variables except $\xi_k$. Then $F = \left< \chi, U(\xi_k)\varphi \right>$ as a function of $\xi_k$, with $\chi = (U(\xi_1)\pi(a_1) \cdots U(\xi_{k-1})\pi(a_{k-1}))^*\psi \in H$ and $\varphi = \pi(a_k)U(\xi_{k+1})\pi(a_{k+1}) \cdots U(\xi_n)\pi(a_n)\Omega \in K_0$. +\end{lemma} +\begin{proof} + \leanok + \uses{lmm:covariant-translations-cyclic-subspace} + The identity is the definition of the adjoint. $\Omega \in K_0$, and $K_0$ is invariant under every $\pi(a)$ and $U(x)$ (Lemma~\ref{lmm:covariant-translations-cyclic-subspace}), so $\varphi \in K_0$. +\end{proof} + +\begin{lemma}[Vanishing of the Correlation Functions] + \label{lmm:reeh-schlieder-correlations-vanish} + \lean{Physicslib4.AQFT.HaagKastler.inner_translated_products_eq_zero} + \uses{lmm:covariant-translations-cyclic-subspace, def:local-von-neumann, def:future-timelike-translation} + \leanok + Let $\pi$, $\Omega$, $U$, $\mathbf{B}_1$, $\mathbf{B}$, $V$, $\psi$, $a_1, \dots, a_n$ and $F$ be as in Lemma~\ref{lmm:reeh-schlieder-vanishing-near-origin}, and suppose moreover that every future-timelike translation subgroup $t \mapsto U(tn)$ has positive energy. Then $F$ vanishes identically on $(\mathbb{R}^4)^n$. +\end{lemma} +\begin{proof} + \leanok + \uses{lmm:neighbourhood-partial-sums, lmm:reeh-schlieder-vanishing-near-origin, lmm:reeh-schlieder-factorization, lmm:timelike-spreading, lmm:covariant-translations-cyclic-subspace} + Choose an open neighbourhood $V_0$ of $0$ whose partial sums of at most $n$ elements lie in $V$ (Lemma~\ref{lmm:neighbourhood-partial-sums}); it is nonempty. Let $P(k)$ say that $F = 0$ whenever $\xi_{k+1}, \dots, \xi_n \in V_0$, the earlier variables being arbitrary. $P(0)$ is Lemma~\ref{lmm:reeh-schlieder-vanishing-near-origin}. Given $P(k-1)$, fix $\xi_j$ for $j \ne k$ with $\xi_{k+1}, \dots, \xi_n \in V_0$. By Lemma~\ref{lmm:reeh-schlieder-factorization}, $F = \left< \chi, U(\xi_k)\varphi \right>$ with $\varphi \in K_0$; it vanishes for $\xi_k \in V_0$ by $P(k-1)$, hence for all $\xi_k$ by Lemma~\ref{lmm:timelike-spreading}, applied with the closed subspace $K_0$ of Lemma~\ref{lmm:covariant-translations-cyclic-subspace}. This is $P(k)$, and $P(n)$ is the claim. +\end{proof} + +\begin{lemma}[Orthogonality on Monomials] + \label{lmm:reeh-schlieder-monomial-orthogonal} + \lean{Physicslib4.AQFT.HaagKastler.inner_monomial_eq_zero} + \uses{lmm:reeh-schlieder-correlations-vanish} + \leanok + In the setting of Lemma~\ref{lmm:reeh-schlieder-correlations-vanish}, for every $n \ge 0$, all $y_1, \dots, y_n \in \mathbb{R}^4$ and all $a_1, \dots, a_n \in \iota_{\mathbf{B}_1}(\mathfrak{U}(\mathbf{B}_1))$, $\left< \psi, \pi(\beta_{y_1}a_1 \cdots \beta_{y_n}a_n)\Omega \right> = 0$, the empty product being $1$. +\end{lemma} +\begin{proof} + \leanok + \uses{lmm:reeh-schlieder-translated-products, lmm:reeh-schlieder-correlations-vanish, def:quasilocal-algebra} + For $n = 0$ the claim is $\left< \psi, \Omega \right> = 0$, which holds because $\Omega = \pi(\iota_{\mathbf{B}}(1))\Omega \in \pi(\mathfrak{U}(\mathbf{B}))\Omega$, $\iota_{\mathbf{B}}$ being unital (\ref{def:quasilocal-algebra}). For $n \ge 1$, set $\xi_1 = y_1$ and $\xi_k = y_k - y_{k-1}$; Lemma~\ref{lmm:reeh-schlieder-translated-products} identifies the inner product with $F(\xi_1, \dots, \xi_n)$, which is $0$ by Lemma~\ref{lmm:reeh-schlieder-correlations-vanish}. +\end{proof} + +\begin{lemma}[Orthogonality on the Generated $*$-Algebra] + \label{lmm:reeh-schlieder-star-algebra-orthogonal} + \lean{Physicslib4.AQFT.HaagKastler.inner_adjoin_translates_eq_zero} + \uses{lmm:reeh-schlieder-correlations-vanish} + \leanok + In the setting of Lemma~\ref{lmm:reeh-schlieder-correlations-vanish}, $\psi$ is orthogonal to $\pi(P)\Omega$ for every $P$ in the $*$-algebra generated by the translates $\iota_{\mathbf{B}_1 + y}(\mathfrak{U}(\mathbf{B}_1 + y))$, $y \in \mathbb{R}^4$. +\end{lemma} +\begin{proof} + \leanok + \uses{lmm:translate-local-subalgebra, lmm:reeh-schlieder-monomial-orthogonal} + Each translate is a $*$-subalgebra, so the generating set $S$ is closed under $*$ and the $*$-algebra it generates is the algebra it generates (in Mathlib, \texttt{StarSubalgebra.adjoin\_eq\_starClosure\_adjoin}). That algebra is the linear span of the finite products of elements of $S$, the empty product included (\texttt{Algebra.adjoin\_eq\_span}). By Lemma~\ref{lmm:translate-local-subalgebra} each such product has the form $\beta_{y_1}a_1 \cdots \beta_{y_n}a_n$ with $a_k \in \iota_{\mathbf{B}_1}(\mathfrak{U}(\mathbf{B}_1))$, so $\psi$ is orthogonal to $\pi(\cdot)\Omega$ of it by Lemma~\ref{lmm:reeh-schlieder-monomial-orthogonal}. Linearity gives the claim. +\end{proof} + +\begin{theorem}[Reeh--Schlieder] + \label{thrm:reeh-schlieder} + \lean{Physicslib4.AQFT.HaagKastler.reeh_schlieder} + \uses{def:translation-generated-algebra, def:local-von-neumann, def:covariant-quasilocal-algebra, def:positive-energy, def:future-timelike-translation} + \leanok + Let $\pi$ be a $*$-representation of $\mathfrak{U}$ on $H$, $\Omega \in H$, and $x \mapsto U(x)$ unitaries with $U(x)\pi(a)\Omega = \pi(\beta_x a)\Omega$ for all translations $x$ and all $a \in \mathfrak{U}$, such that every future-timelike translation subgroup $t \mapsto U(tn)$ has positive energy. Let $\mathbf{B}_1$ and $\mathbf{B}$ be diamonds with $\mathbf{B}_1 + x \subseteq \mathbf{B}$ for every $x$ in an open neighbourhood of $0$. Then $\pi(\mathfrak{A}_{\mathbf{B}_1})\Omega$ lies in the closure of $\pi(\mathfrak{U}(\mathbf{B}))\Omega$. +\end{theorem} +\begin{proof} + \leanok + \uses{lmm:reeh-schlieder-star-algebra-orthogonal, def:translation-generated-algebra} + The closure of the subspace $\pi(\mathfrak{U}(\mathbf{B}))\Omega$ is the orthogonal complement of its orthogonal complement, so it suffices that every $\psi$ orthogonal to $\pi(\mathfrak{U}(\mathbf{B}))\Omega$ is orthogonal to $\pi(P)\Omega$ for every $P \in \mathfrak{A}_{\mathbf{B}_1}$. This holds on the generated $*$-algebra by Lemma~\ref{lmm:reeh-schlieder-star-algebra-orthogonal}, and $P \mapsto \left< \psi, \pi(P)\Omega \right>$ is continuous, so it holds on the norm closure $\mathfrak{A}_{\mathbf{B}_1}$. +\end{proof} + +\begin{corollary}[Reeh--Schlieder under Cyclicity for the Translation-Generated Algebras] + \label{crllr:reeh-schlieder-cyclic} + \lean{Physicslib4.AQFT.HaagKastler.reeh_schlieder_cyclic} + \uses{thrm:reeh-schlieder, def:cyclic-vector} + \leanok + Under the hypotheses of Theorem~\ref{thrm:reeh-schlieder} on $\pi$, $\Omega$ and $U$, if $\Omega$ is cyclic for $\pi(\mathfrak{A}_{\mathbf{B}'})$ for every nonempty diamond $\mathbf{B}'$, then $\Omega$ is cyclic for $\pi(\mathfrak{U}(\mathbf{B}))$ for every nonempty diamond $\mathbf{B}$. +\end{corollary} +\begin{proof} + \leanok + \uses{thrm:reeh-schlieder, lmm:diamond-small-translates} + Choose a nonempty $\mathbf{B}_1$ for $\mathbf{B}$ by Lemma~\ref{lmm:diamond-small-translates}. By Theorem~\ref{thrm:reeh-schlieder} the closure of $\pi(\mathfrak{U}(\mathbf{B}))\Omega$ contains $\pi(\mathfrak{A}_{\mathbf{B}_1})\Omega$, which is dense by hypothesis. +\end{proof} + +\begin{lemma}[Closure of a Bicommutant Orbit] + \label{lmm:bicommutant-orbit-closure} + \lean{Physicslib4.AQFT.HaagKastler.apply_mem_closure_translationGeneratedAlgebra} + \uses{def:translation-generated-algebra} + \leanok + Let $\pi$ be a $*$-representation of $\mathfrak{U}$ on $H$, $\Omega \in H$ and $\mathbf{B}$ a diamond. Then $\pi(\mathfrak{A}_{\mathbf{B}})''\Omega$ lies in the closure of $\pi(\mathfrak{A}_{\mathbf{B}})\Omega$. +\end{lemma} +\begin{proof} + \leanok + \uses{lmm:bicommutant-single-vector, def:quasilocal-algebra} + $\mathfrak{A}_{\mathbf{B}}$ contains $\iota_{\mathbf{B}}(1) = 1$, since $\iota_{\mathbf{B}}$ is unital (\ref{def:quasilocal-algebra}), so it is a unital $*$-subalgebra of $\mathfrak{U}$ and the restriction of $\pi$ to it is a unital $*$-algebra homomorphism. Apply Lemma~\ref{lmm:bicommutant-single-vector} to this restriction. +\end{proof} + +\begin{corollary}[Reeh--Schlieder under the von Neumann Form of Weak Additivity] + \label{crllr:reeh-schlieder-von-neumann} + \lean{Physicslib4.AQFT.HaagKastler.reeh_schlieder_cyclic_of_vonNeumann} + \uses{thrm:reeh-schlieder, def:weak-additivity-von-neumann, def:cyclic-vector} + \leanok + Under the hypotheses of Theorem~\ref{thrm:reeh-schlieder} on $\pi$, $\Omega$ and $U$, if $\pi$ satisfies weak additivity in the von Neumann sense and $\Omega$ is cyclic for $\pi(\mathfrak{U})$, then $\Omega$ is cyclic for $\pi(\mathfrak{U}(\mathbf{B}))$ for every nonempty diamond $\mathbf{B}$. +\end{corollary} +\begin{proof} + \leanok + \uses{crllr:reeh-schlieder-cyclic, lmm:bicommutant-orbit-closure} + For every nonempty diamond $\mathbf{B}'$, the closure of $\pi(\mathfrak{A}_{\mathbf{B}'})\Omega$ contains $\pi(\mathfrak{A}_{\mathbf{B}'})''\Omega$ (Lemma~\ref{lmm:bicommutant-orbit-closure}), hence $\pi(\mathfrak{U})\Omega$, which is dense. So $\Omega$ is cyclic for every such $\pi(\mathfrak{A}_{\mathbf{B}'})$; apply Corollary~\ref{crllr:reeh-schlieder-cyclic}. +\end{proof} + +\begin{corollary}[Reeh--Schlieder under Weak Additivity] + \label{crllr:reeh-schlieder-weak-additivity} + \lean{Physicslib4.AQFT.HaagKastler.reeh_schlieder_cyclic_of_weaklyAdditive} + \uses{thrm:reeh-schlieder, def:weak-additivity, def:cyclic-vector} + \leanok + Under the hypotheses of Theorem~\ref{thrm:reeh-schlieder} on $\pi$, $\Omega$ and $U$, if the net is weakly additive and $\Omega$ is cyclic for $\pi(\mathfrak{U})$, then $\Omega$ is cyclic for $\pi(\mathfrak{U}(\mathbf{B}))$ for every nonempty diamond $\mathbf{B}$. +\end{corollary} +\begin{proof} + \leanok + \uses{crllr:reeh-schlieder-von-neumann, lmm:weak-additivity-von-neumann} + By Lemma~\ref{lmm:weak-additivity-von-neumann}, $\pi$ satisfies weak additivity in the von Neumann sense; apply Corollary~\ref{crllr:reeh-schlieder-von-neumann}. +\end{proof} + +\begin{corollary}[Reeh--Schlieder for a Vacuum State] + \label{crllr:reeh-schlieder-vacuum} + \lean{Physicslib4.AQFT.HaagKastler.reeh_schlieder_cyclic_of_vacuum} + \uses{def:vacuum-state-concrete, def:weak-additivity, def:cyclic-vector} + \leanok + Let the net be weakly additive, and let $(K, \pi, \Omega)$ be a representation and $U(L)$ unitaries satisfying the implementation and spectrum conditions of a vacuum state (\ref{def:vacuum-state-concrete}): $U(L)\pi(a)\Omega = \pi(\beta_L a)\Omega$ for every $L$ and $a$, and $t \mapsto U(\gamma(t))$ has positive energy for every future-timelike translation subgroup $\gamma$. If $\Omega$ is cyclic for $\pi(\mathfrak{U})$, then $\Omega$ is cyclic for $\pi(\mathfrak{U}(\mathbf{B}))$ for every nonempty diamond $\mathbf{B}$. In particular this holds for the witnessing data of any vacuum state $\omega$ with $\Omega$ cyclic; the state itself, and the condition that the representation reproduces it, play no role. +\end{corollary} +\begin{proof} + \leanok + \uses{crllr:reeh-schlieder-weak-additivity, def:future-timelike-translation} + Write $U(x)$ for $U(\mathrm{translationSub}(x))$. Then the implementation condition for $L = \mathrm{translationSub}(x)$ is the hypothesis $U(x)\pi(a)\Omega = \pi(\beta_x a)\Omega$ of Theorem~\ref{thrm:reeh-schlieder}, and for $n$ future-pointing timelike, $\mathrm{translationFlow}(n)$ is a future-timelike translation subgroup (\ref{def:future-timelike-translation}) with $U(\mathrm{translationFlow}(n)(t)) = U(tn)$, so each $t \mapsto U(tn)$ has positive energy. Apply Corollary~\ref{crllr:reeh-schlieder-weak-additivity}. +\end{proof} + +\begin{corollary}[The Vacuum is Separating] + \label{crllr:reeh-schlieder-separating} + \lean{Physicslib4.AQFT.HaagKastler.reeh_schlieder_separating} + \uses{crllr:reeh-schlieder-cyclic, def:local-von-neumann, def:completely-spacelike} + \leanok + Under the hypotheses of Corollary~\ref{crllr:reeh-schlieder-cyclic}, $\Omega$ is separating for the local von Neumann algebra $R(\mathbf{C})$ of every diamond $\mathbf{C}$ that is completely spacelike to some nonempty diamond $\mathbf{B}$: every $R \in R(\mathbf{C})$ with $R\Omega = 0$ is zero. +\end{corollary} +\begin{proof} + \leanok + \uses{crllr:reeh-schlieder-cyclic, thrm:statistical-independence} + $\Omega$ is cyclic for $\pi(\mathfrak{U}(\mathbf{B}))$ by Corollary~\ref{crllr:reeh-schlieder-cyclic}; apply Theorem~\ref{thrm:statistical-independence}. +\end{proof} diff --git a/notes/agents/manual-ch-reeh-schlieder-progress.md b/notes/agents/manual-ch-reeh-schlieder-progress.md new file mode 100644 index 0000000..638d53e --- /dev/null +++ b/notes/agents/manual-ch-reeh-schlieder-progress.md @@ -0,0 +1,7 @@ +# Manual chapter: The Reeh–Schlieder theorem (progress) + +- 2026-11-08: read README, Manual.lean, Stone/HaagKastler chapters, blueprint §10.9 and the Lean module docstrings; collecting `#check` outputs. +- 2026-11-08: wrote web/Manual/ReehSchlieder.lean (Overview, Design, Main definitions and theorems, Where to look); next: wire into Manual.lean/README and build. +- 2026-11-08: wired into Manual.lean and README Layout; building. +- 2026-11-08: lake build Manual and generate-manual pass; reeh-schlieder refs from HaagKastler/Curved/NotProved resolve; temporal-wording check passes. Chapter complete (not committed). +- 2026-11-08: review REVISE (4 wording fixes) applied by the orchestrator; Manual rebuilds; wording check OK. diff --git a/notes/agents/proposal-reeh-schlieder-2026-11-05.md b/notes/agents/proposal-reeh-schlieder-2026-11-05.md new file mode 100644 index 0000000..fcad546 --- /dev/null +++ b/notes/agents/proposal-reeh-schlieder-2026-11-05.md @@ -0,0 +1,380 @@ +# Proposal: a Reeh–Schlieder section for Chapter 10 + +Status: D1–D4 approved as recommended (2026-11-07). The section is in the blueprint (`sec10/reeh-schlieder.tex`), reviewed and passed; not yet formalized. Log: +`reeh-schlieder-blueprint-progress.md`. + +## Summary + +Add a section proving the Reeh–Schlieder theorem for Haag–Kastler nets in Minkowski spacetime. The +section is organised as one hypothesis-free theorem and four corollaries. + +- **Main theorem (no additivity hypothesis).** Let π be a representation of the quasilocal algebra + and Ω a vector, with unitaries U implementing the translations on the vectors π(a)Ω and positive + energy along every future-timelike direction. If small translates of a diamond B₁ stay inside a + diamond B, then every vector π(A)Ω, for A in the algebra 𝔄_{B₁} generated by the translates of + 𝔘(B₁), lies in the closure of π(𝔘(B))Ω. + + Neither cyclicity of Ω nor any additivity property of the net is assumed. +- **Corollary A, under cyclicity for 𝔄.** If Ω is cyclic for π(𝔄_{B'}) for every diamond B', it is + cyclic for π(𝔘(B)) for every diamond B. This is the minimal hypothesis, and it is checked per + representation. +- **Corollary B, under weak additivity.** If the net is weakly additive (each 𝔄_{B'} is dense in + 𝔘) and Ω is cyclic for π(𝔘), then Ω is cyclic for every π(𝔘(B)). This is the textbook statement, + with a hypothesis on the net alone. +- **Corollary C, under the von Neumann form.** If π(𝔄_{B'})'' contains π(𝔘) for every diamond B' + and Ω is cyclic for π(𝔘), the same conclusion holds. The hypothesis depends on the + representation but holds when weak-operator density holds and norm density fails. +- **Corollaries D and E.** D is the vacuum-state form of Corollary B; E says Ω is also separating + for the local von Neumann algebras, through the existing `thrm:statistical-independence`. + +The implications between the hypotheses are: weak additivity ⟹ von Neumann form ⟹ cyclicity +for 𝔄 (the last two given Ω cyclic for π(𝔘)). Corollary B follows from C, and C from A. + +### Why the main theorem uses a smaller diamond + +The proof needs room to translate: the function F in the proof outline vanishes on an *open* set +of translations only because small translates of B₁ stay inside B. With B₁ = B it vanishes only +at the origin, and analytic continuation needs more than that. + +A statement with 𝔄_B for the same diamond B, "π(𝔘(B))Ω and π(𝔄_B)Ω have the same closure", would +need 𝔘(B) to be generated by the algebras of smaller diamonds inside it, which is again an +additivity property. The hypothesis-free theorem therefore relates B₁ to B, and the corollaries +quantify over all diamonds, which is harmless because every diamond contains smaller ones with +room to translate (`lmm:diamond-small-translates`). + +### The analytic route + +There is no joint spectral measure for the four translation generators. Analytic continuation is +done in one complex variable at a time, along one future-timelike direction at a time. This needs +only the library's per-direction positive energy (`IsPositiveEnergy`) and Stone's theorem in the +form `isPositiveEnergy_iff_exists_exp`. + +## Decisions needed + +- **D1. New definitions.** + - `def:translation-generated-algebra`, the algebra 𝔄_B. + - `def:weak-additivity`, a predicate on the net. + - `def:weak-additivity-von-neumann`, a predicate on a net and a representation. + + None of them changes `HaagKastlerNet`; weak additivity is used only as a hypothesis. + **Recommended:** add all three as definitions. Making weak additivity an axiom field is your + design decision and is not proposed. +- **D2. The form of the hypotheses.** The theorem and Corollaries A to C are stated for explicit + data `(K, π, Ω, U)`, using only translations. Corollary D states the result for a vacuum state + (`IsVacuumStateConcrete`) with a cyclic representative, since `IsVacuumState` itself requires + neither cyclicity nor a group law for U. **Recommended.** +- **D3. Placement.** + - (a) A new section 10.9, `sections/sec10/reeh-schlieder.tex`, after general covariance; no + existing section is renumbered. **Recommended.** + - (b) A subsection of 10.6, which is already about 2,200 lines long. +- **D4. Scope.** Minkowski spacetime only. Reeh–Schlieder in curved spacetime needs different + methods, such as analytic microlocal analysis, and is out of scope. + +## Gaps in the library to fill first + +These are general facts, and each is a separate node below. + +- **G1. Spectral support.** The spectral measure of a positive self-adjoint operator is supported + on `[0, ∞)`. No such lemma was found in `Physicslib4/Spectral/Unbounded/`. +- **G2. Off-diagonal matrix elements.** `ProjectionValuedMeasure.inner_integral` gives + `⟪ψ, (∫ f dE) ψ⟫ = ∫ f d(E.assoc ψ)` for the diagonal only. The off-diagonal `⟪χ, (∫ f dE) φ⟫` + follows by polarization; it may be easier to work with polarized diagonal terms throughout. +- **G3. Holomorphy of the extension.** `z ↦ ∫_{[0,∞)} e^{izλ} dμ(λ)` is holomorphic for `Im z > 0`, + continuous and bounded on `Im z ≥ 0`, for a finite measure μ. This is differentiation under the + integral sign plus dominated convergence, both in Mathlib. +- **G4. Edge uniqueness.** A function holomorphic on the open upper half-plane, continuous up to the + real axis, and zero on a real interval, is identically zero. + - Proof: Schwarz reflection across the interval, then the identity theorem. + - The reflection step reuses `differentiableOn_of_continuousOn_off_horizontal_line` + (`Physicslib4/Analysis/HorizontalLineRemovable.lean`, with `ℓ = 0`). + - No Schwarz reflection principle was found in Mathlib. +- **G5. Closure under the bicommutant.** For a unital \*-algebra S of bounded operators and any + vector Ω, S Ω and S'' Ω have the same closure. The existing `lmm:cyclic-subspace-reduces` may + supply most of it; check before adding a node. + +## Proof outline of the main theorem + +Let B₁ + x ⊆ B for every x in an open neighbourhood V of 0. Let K₀ be the closure of π(𝔘)Ω, and +let ψ be orthogonal to π(𝔘(B))Ω. + +1. **Translations on K₀.** From U(x)π(a)Ω = π(β_x a)Ω: + - with a = 1, U(x)Ω = Ω; + - on K₀, U(x)π(a) = π(β_x a)U(x) and U(x + y) = U(x)U(y); + - K₀ is invariant under π and U. + + No cyclicity is needed. +2. **Vanishing near the origin.** For B₁, …, Bₙ ∈ 𝔘(B₁), set + `F(ξ₁, …, ξₙ) = ⟨ψ, U(ξ₁) π(B₁) U(ξ₂) π(B₂) ⋯ U(ξₙ) π(Bₙ) Ω⟩`. + + By step 1 this equals `⟨ψ, π(β_{x₁}B₁ ⋯ β_{xₙ}Bₙ) Ω⟩` with x_k = ξ₁ + ⋯ + ξ_k, and each + factor lies in 𝔘(B₁ + x_k). If every x_k is in V, the product is in 𝔘(B), so F = 0 when each + ξ_k is small. +3. **One variable, one direction.** With all variables but ξ_k fixed, F = ⟨χ, U(ξ_k) φ⟩ with φ in + K₀. Along a future-timelike direction e, `t ↦ ⟨χ, U(te) U(v) φ⟩` extends holomorphically to the + upper half-plane (by G1–G3), so by G4, vanishing for small t implies vanishing for all t. +4. **Spreading.** Vanishing on a nonempty open set W ⊆ ℝ⁴ spreads to W + ℝe for every + future-timelike e. Four linearly independent future-timelike directions give + W + ℝe₁ + ⋯ + ℝe₄ = ℝ⁴. +5. **All variables.** Apply step 4 to ξ₁ with the others small, then to ξ₂ with ξ₁ arbitrary and the + rest small, and so on. Then F ≡ 0. +6. **Closure.** ψ is orthogonal to π(P)Ω for every P in the \*-algebra generated by the translates + of 𝔘(B₁), and by continuity of π, for every P in its closure 𝔄_{B₁}. Since ψ was any vector + orthogonal to π(𝔘(B))Ω, π(𝔄_{B₁})Ω lies in the closure of π(𝔘(B))Ω. + +## Draft blueprint entries + +Labels follow the chapter's conventions (`def:`, `lmm:`, `thrm:`, `crllr:`). No `\lean{}` or +`\leanok` tags yet; the formalizer adds them. + +```latex +\section{The Reeh--Schlieder Theorem}\label{sctn:reeh-schlieder} + +In a vacuum representation the vacuum vector is cyclic not only for the quasilocal algebra but for +the algebra of every diamond: states prepared by local operations in an arbitrarily small region +approximate every state of the theory. The section proves this in two stages. The main theorem, +which assumes no additivity property of the net, says that the vectors obtained from a diamond's +algebra already approximate those obtained from all translates of a smaller diamond's algebra. +Three corollaries then give cyclicity under successively stronger hypotheses: cyclicity for the +translation-generated algebras, the von Neumann form of weak additivity, and weak additivity +itself. The proof uses the spectrum condition through analytic continuation in one complex +variable at a time, along one future-timelike direction at a time. + +\begin{definition}[Translation-Generated Algebra] + \label{def:translation-generated-algebra} + \uses{def:covariant-quasilocal-algebra, def:causal-diamond, def:future-timelike-translation} + For a diamond $\mathbf{B}$, $\mathfrak{A}_{\mathbf{B}}$ is the C*-subalgebra of the quasilocal + algebra $\mathfrak{U}$ generated by the translates + $\iota_{\mathbf{B}+x}(\mathfrak{U}(\mathbf{B}+x))$, $x \in \mathbb{R}^4$: the norm closure of + the $*$-algebra they generate. +\end{definition} + +\begin{definition}[Weak Additivity] + \label{def:weak-additivity} + \uses{def:translation-generated-algebra} + A Haag--Kastler net is \emph{weakly additive} if $\mathfrak{A}_{\mathbf{B}} = \mathfrak{U}$ for + every diamond $\mathbf{B}$. +\end{definition} + +\begin{definition}[Weak Additivity, von Neumann Form] + \label{def:weak-additivity-von-neumann} + \uses{def:translation-generated-algebra} + A representation $\pi$ of $\mathfrak{U}$ satisfies \emph{weak additivity in the von Neumann + sense} if $\pi(\mathfrak{U}) \subseteq \pi(\mathfrak{A}_{\mathbf{B}})''$ for every diamond + $\mathbf{B}$. +\end{definition} + +\begin{lemma}[Weak Additivity Implies the von Neumann Form] + \label{lmm:weak-additivity-von-neumann} + \uses{def:weak-additivity, def:weak-additivity-von-neumann} + If the net is weakly additive, every representation satisfies weak additivity in the von + Neumann sense. +\end{lemma} +\begin{proof} + $\pi(\mathfrak{U}) = \pi(\mathfrak{A}_{\mathbf{B}}) \subseteq \pi(\mathfrak{A}_{\mathbf{B}})''$. +\end{proof} + +\begin{lemma}[Translates of a Smaller Diamond] + \label{lmm:diamond-small-translates} + \uses{def:causal-diamond} + For every diamond $\mathbf{B}$ there are a diamond $\mathbf{B}_1$ and an open neighbourhood $V$ + of $0$ in $\mathbb{R}^4$ with $\mathbf{B}_1 + x \subseteq \mathbf{B}$ for every $x \in V$. +\end{lemma} +\begin{proof} + Write $\mathbf{B} = I^+(p) \cap I^-(q)$ and choose $p \ll p' \ll q' \ll q$. Take + $\mathbf{B}_1 = I^+(p') \cap I^-(q')$; its translate by $x$ is $I^+(p'+x) \cap I^-(q'+x)$. Since + $I^+(p)$ and $I^-(q)$ are open, $p \ll p' + x$ and $q' + x \ll q$ for $x$ near $0$, and then + $\mathbf{B}_1 + x \subseteq \mathbf{B}$ by transitivity of $\ll$. +\end{proof} + +\begin{lemma}[Spectral Support of a Positive Operator] + \label{lmm:positive-spectral-support} + The spectral measure $E$ of a positive self-adjoint operator $A$ satisfies + $E((-\infty, 0)) = 0$. +\end{lemma} +\begin{proof} + For $\psi$ in the range of $E((-n, -1/n))$, $\psi$ is in the domain of $A$ and + $\langle \psi, A\psi \rangle \le -\|\psi\|^2/n$, contradicting positivity unless $\psi = 0$. + Take the union over $n$. +\end{proof} + +\begin{lemma}[Holomorphic Extension under Positive Energy] + \label{lmm:positive-energy-holomorphic} + \uses{def:positive-energy, thrm:positive-energy-iff-exp, lmm:positive-spectral-support} + Let $V$ be a one-parameter unitary group with positive energy and let $\chi, \varphi \in H$. + Then $t \mapsto \langle \chi, V(t)\varphi \rangle$ is the restriction to $\mathbb{R}$ of a + function that is holomorphic on $\{\operatorname{Im} z > 0\}$ and bounded and continuous on + $\{\operatorname{Im} z \ge 0\}$. +\end{lemma} +\begin{proof} + By Stone's theorem $V(t) = e^{itA}$ with $A$ positive and self-adjoint. By polarization, + $\langle \chi, V(t)\varphi \rangle$ is a combination of integrals + $\int_{[0,\infty)} e^{it\lambda} \, d\mu(\lambda)$ against finite positive measures + (Lemma~\ref{lmm:positive-spectral-support}). Replace $t$ by $z$: for $\operatorname{Im} z \ge 0$ + the integrand is bounded by $1$, so the integral is bounded and continuous by dominated + convergence, and holomorphic for $\operatorname{Im} z > 0$ by differentiation under the + integral sign. +\end{proof} + +\begin{lemma}[Vanishing on an Edge] + \label{lmm:edge-vanishing} + A function holomorphic on the open upper half-plane, continuous on its closure, and zero on an + open interval of the real axis is identically zero. +\end{lemma} +\begin{proof} + Extend the function to the lower half-plane by $f(z) = \overline{f(\bar z)}$. The extension is + continuous on a neighbourhood of the interval and holomorphic off the real axis, hence + holomorphic there. It vanishes on the interval, so it vanishes on the connected upper + half-plane by the identity theorem. +\end{proof} + +\begin{lemma}[Spreading Along Timelike Directions] + \label{lmm:timelike-spreading} + \uses{lmm:positive-energy-holomorphic, lmm:edge-vanishing, def:future-timelike-translation} + Let $U$ be unitaries on $H$ indexed by the translations $\mathbb{R}^4$, and $K_0 \subseteq H$ a + closed subspace invariant under every $U(x)$, on which $U(x+y) = U(x)U(y)$. Suppose every + future-timelike translation subgroup has positive energy. If $\chi \in H$, $\varphi \in K_0$, + and $x \mapsto \langle \chi, U(x)\varphi \rangle$ vanishes on a nonempty open set, it vanishes + identically. +\end{lemma} +\begin{proof} + If it vanishes on an open $W$, then for $v \in W$ and $e$ future timelike, the function + $t \mapsto \langle \chi, U(te) U(v)\varphi \rangle$ vanishes for small $t$, hence for all $t$ + (Lemmas~\ref{lmm:positive-energy-holomorphic} and~\ref{lmm:edge-vanishing}). So it vanishes on + $W + \mathbb{R}e$. Four linearly independent future-timelike directions give + $W + \mathbb{R}e_1 + \dots + \mathbb{R}e_4 = \mathbb{R}^4$. +\end{proof} + +\begin{lemma}[Translations on the Cyclic Subspace] + \label{lmm:covariant-translations-cyclic-subspace} + \uses{def:covariant-quasilocal-algebra} + Let $\pi$ be a representation of $\mathfrak{U}$ on $H$, $\Omega \in H$, and $U(x)$ unitaries + with $U(x)\pi(a)\Omega = \pi(\beta_x a)\Omega$ for all translations $x$ and all $a$. Let $K_0$ + be the closure of $\pi(\mathfrak{U})\Omega$. Then $U(x)\Omega = \Omega$; $K_0$ is invariant + under every $\pi(a)$ and $U(x)$; and on $K_0$, $U(x)\pi(a) = \pi(\beta_x a)U(x)$ and + $U(x+y) = U(x)U(y)$. +\end{lemma} +\begin{proof} + Take $a = 1$ for invariance of $\Omega$. The identities hold on the vectors $\pi(b)\Omega$ + because $\beta$ is a group action by $*$-automorphisms, for instance + $U(x)\pi(a)\pi(b)\Omega = \pi(\beta_x(ab))\Omega = \pi(\beta_x a)U(x)\pi(b)\Omega$, and extend + to $K_0$ by continuity. +\end{proof} + +\begin{theorem}[Reeh--Schlieder] + \label{thrm:reeh-schlieder} + \uses{def:translation-generated-algebra, lmm:timelike-spreading, + lmm:covariant-translations-cyclic-subspace, def:local-von-neumann} + Let $\pi$ be a representation of $\mathfrak{U}$ on $H$, $\Omega \in H$, and $U(x)$ unitaries + with $U(x)\pi(a)\Omega = \pi(\beta_x a)\Omega$ for all translations $x$ and all $a$, such that + every future-timelike translation subgroup has positive energy. Let $\mathbf{B}_1$ and + $\mathbf{B}$ be diamonds with $\mathbf{B}_1 + x \subseteq \mathbf{B}$ for every $x$ in a + neighbourhood of $0$. Then $\pi(\mathfrak{A}_{\mathbf{B}_1})\Omega$ lies in the closure of + $\pi(\mathfrak{U}(\mathbf{B}))\Omega$. +\end{theorem} +\begin{proof} + Let $\psi$ be orthogonal to $\pi(\mathfrak{U}(\mathbf{B}))\Omega$. For + $B_1, \dots, B_n \in \mathfrak{U}(\mathbf{B}_1)$, the function + $F(\xi_1, \dots, \xi_n) = \langle \psi, U(\xi_1)\pi(B_1)U(\xi_2)\pi(B_2) \cdots U(\xi_n)\pi(B_n)\Omega \rangle$ + equals $\langle \psi, \pi(\beta_{x_1}B_1 \cdots \beta_{x_n}B_n)\Omega \rangle$ with + $x_k = \xi_1 + \dots + \xi_k$ + (Lemma~\ref{lmm:covariant-translations-cyclic-subspace}), so it vanishes when every $x_k$ is + small. Applying Lemma~\ref{lmm:timelike-spreading} to one variable at a time, with the earlier + variables arbitrary and the later ones small, shows $F \equiv 0$. Hence $\psi$ is orthogonal to + $\pi(P)\Omega$ for every $P$ in the $*$-algebra generated by the translates of + $\mathfrak{U}(\mathbf{B}_1)$, and by continuity for every $P \in \mathfrak{A}_{\mathbf{B}_1}$. +\end{proof} + +\begin{corollary}[Reeh--Schlieder under Cyclicity for the Translation-Generated Algebras] + \label{crllr:reeh-schlieder-cyclic} + \uses{thrm:reeh-schlieder, lmm:diamond-small-translates} + Under the hypotheses of Theorem~\ref{thrm:reeh-schlieder} on $\pi$, $\Omega$ and $U$, if + $\Omega$ is cyclic for $\pi(\mathfrak{A}_{\mathbf{B}'})$ for every diamond $\mathbf{B}'$, then + $\Omega$ is cyclic for $\pi(\mathfrak{U}(\mathbf{B}))$ for every diamond $\mathbf{B}$. +\end{corollary} +\begin{proof} + Choose $\mathbf{B}_1$ for $\mathbf{B}$ by Lemma~\ref{lmm:diamond-small-translates}. The closure + of $\pi(\mathfrak{U}(\mathbf{B}))\Omega$ contains $\pi(\mathfrak{A}_{\mathbf{B}_1})\Omega$ by + Theorem~\ref{thrm:reeh-schlieder}, which is dense. +\end{proof} + +\begin{lemma}[Closure of a Bicommutant Orbit] + \label{lmm:bicommutant-orbit-closure} + \uses{lmm:cyclic-subspace-reduces} + For a unital $*$-algebra $S$ of bounded operators on $H$ and $\Omega \in H$, the vectors + $S\Omega$ and $S''\Omega$ have the same closure. +\end{lemma} +\begin{proof} + The projection $P$ onto the closure of $S\Omega$ commutes with $S$, since the closure is + invariant under the $*$-closed set $S$; so $P \in S'$. For $T \in S''$, + $T\Omega = TP\Omega = PT\Omega$ lies in the range of $P$. +\end{proof} + +\begin{corollary}[Reeh--Schlieder under the von Neumann Form of Weak Additivity] + \label{crllr:reeh-schlieder-von-neumann} + \uses{crllr:reeh-schlieder-cyclic, def:weak-additivity-von-neumann, + lmm:bicommutant-orbit-closure} + Under the hypotheses of Theorem~\ref{thrm:reeh-schlieder} on $\pi$, $\Omega$ and $U$, if $\pi$ + satisfies weak additivity in the von Neumann sense and $\Omega$ is cyclic for $\pi(\mathfrak{U})$, + then $\Omega$ is cyclic for $\pi(\mathfrak{U}(\mathbf{B}))$ for every diamond $\mathbf{B}$. +\end{corollary} +\begin{proof} + By Lemma~\ref{lmm:bicommutant-orbit-closure}, the closure of + $\pi(\mathfrak{A}_{\mathbf{B}'})\Omega$ contains $\pi(\mathfrak{A}_{\mathbf{B}'})''\Omega$, hence + $\pi(\mathfrak{U})\Omega$, which is dense. Apply + Corollary~\ref{crllr:reeh-schlieder-cyclic}. +\end{proof} + +\begin{corollary}[Reeh--Schlieder under Weak Additivity] + \label{crllr:reeh-schlieder-weak-additivity} + \uses{crllr:reeh-schlieder-von-neumann, lmm:weak-additivity-von-neumann} + Under the hypotheses of Theorem~\ref{thrm:reeh-schlieder} on $\pi$, $\Omega$ and $U$, if the + net is weakly additive and $\Omega$ is cyclic for $\pi(\mathfrak{U})$, then $\Omega$ is cyclic + for $\pi(\mathfrak{U}(\mathbf{B}))$ for every diamond $\mathbf{B}$. +\end{corollary} +\begin{proof} + Lemma~\ref{lmm:weak-additivity-von-neumann} and + Corollary~\ref{crllr:reeh-schlieder-von-neumann}. +\end{proof} + +\begin{corollary}[Reeh--Schlieder for a Vacuum State] + \label{crllr:reeh-schlieder-vacuum} + \uses{crllr:reeh-schlieder-weak-additivity, def:vacuum-state-concrete} + If the net is weakly additive, $\omega$ is a vacuum state, and $(K, \pi, \Omega, U)$ is a + representative of $\omega$ with $\Omega$ cyclic for $\pi(\mathfrak{U})$, then $\Omega$ is cyclic + for every local algebra. +\end{corollary} +\begin{proof} + The vacuum conditions restricted to translations are the hypotheses of + Theorem~\ref{thrm:reeh-schlieder}; apply + Corollary~\ref{crllr:reeh-schlieder-weak-additivity}. +\end{proof} + +\begin{corollary}[The Vacuum is Separating] + \label{crllr:reeh-schlieder-separating} + \uses{crllr:reeh-schlieder-cyclic, thrm:statistical-independence} + Under the hypotheses of Corollary~\ref{crllr:reeh-schlieder-cyclic}, $\Omega$ is separating for + the local von Neumann algebra $R(\mathbf{B}_2)$ of every diamond $\mathbf{B}_2$ that is spacelike + to some diamond $\mathbf{B}_1$. +\end{corollary} +\begin{proof} + $\Omega$ is cyclic for $\pi(\mathfrak{U}(\mathbf{B}_1))$ by + Corollary~\ref{crllr:reeh-schlieder-cyclic}; apply Theorem~\ref{thrm:statistical-independence}. +\end{proof} +``` + +## Notes for the formalizer + +- **Translations.** Use `translationSub` and `isAlexandrovBasisSet_smul` for translates of + diamonds. 𝔄_B can be the topological closure of + `StarSubalgebra.adjoin ℂ (⋃ x, Set.range (N.quasilocal.ι (isAlexandrovBasisSet_smul (translationSub x) hB)))`, + or be stated through `N.action (translationSub x)` and `action_ι`. +- **Cyclicity.** Local cyclicity is `Dense ((fun T => T Ω) '' N.localOperators π hB)`, the form + `localVonNeumann_separating` already takes, so Corollary E is a direct application. +- **The von Neumann form.** It uses the library's commutant convention, `Set.centralizer` in the + bounded operators. +- **Lemma sizes.** The analytic lemmas (`lmm:positive-energy-holomorphic`, `lmm:edge-vanishing`) + are the largest. Each may need splitting further when formalized, following the chapter's rule of + short proofs. +- **Restrictions.** The section needs no `**Restriction:**` line: the theorem is stated in full + generality for Minkowski nets, and the additivity hypotheses belong to the corollaries, as in the + standard theory. diff --git a/notes/agents/reeh-schlieder-blueprint-progress.md b/notes/agents/reeh-schlieder-blueprint-progress.md new file mode 100644 index 0000000..81439f5 --- /dev/null +++ b/notes/agents/reeh-schlieder-blueprint-progress.md @@ -0,0 +1,38 @@ +# Reeh–Schlieder blueprint section: progress + +Source: `proposal-reeh-schlieder-2026-11-05.md` (D1–D4 approved as recommended). + +- 2026-11-07. Read the proposal and every existing node the draft cites. Findings: + - All ten cited labels exist in `sections/sec10/`. + - `lmm:bicommutant-single-vector` (haag-kastler-axioms.tex) already proves G5 for a unital + *-homomorphism; `lmm:bicommutant-orbit-closure` is restated as its instance for + π restricted to 𝔄_B and cites it, not `lmm:cyclic-subspace-reduces`. + - Alexandrov basis sets include the empty set, so `lmm:diamond-small-translates` needs an + empty case. + - `IsVacuumState` is existential in its representation, so Corollary D is stated for the + witnessing data, not for an arbitrary representative. + - Statistical independence takes completely spacelike regions. + - House notation: spectral measure μ^A, translates written L·B, β_L for the quasilocal lift. +- 2026-11-07. Steps 1-2: wrote `blueprint/src/sections/sec10/reeh-schlieder.tex` (draft plus + fixes) and added its `\input` after general covariance in `content.tex`. `print.tex` and + `web.tex` only `\input{content}`; nothing else to change. Split the theorem's proof into + `lmm:reeh-schlieder-translated-products` and `lmm:reeh-schlieder-correlations-vanish`. +- 2026-11-07. Step 6: refresh parsed 702 declarations including all 20 new ones; validate reports only the 14 pre-existing `conv:` unknown-dependency errors. +- 2026-11-07. Step 7a: `leanblueprint pdf` succeeds; the new section has no undefined refs or overfull boxes (two underfull lines reworded away). +- 2026-11-07. Step 7b: `leanblueprint web` succeeds (warnings are the pre-existing includegraphics/PostScript ones); the section is rendered and its nodes appear in the dependency graph. `scripts/check_temporal_wording.py` passes. Done. +- 2026-11-07. Reviewer REVISE round. Rewrote `reeh-schlieder.tex` (my own file) with: nonempty + diamonds in the additivity definitions and corollaries A–E; nonempty interval in + `lmm:edge-vanishing`; the removability node `lmm:horizontal-line-removable`; the requested + splits; the missing `\uses`; an "Analytic Preliminaries" subsection. Added + `\uses{lmm:horizontal-line-removable}` to the proof of `thrm:strip-periodic-extension` in + `haag-kastler-axioms.tex` (the only edit to an existing section). +- 2026-11-07. Set `lmm:horizontal-line-removable` leanDeclaration/leanFile and status proved (tool + wrote its `\lean`/`\leanok`). Refresh: 721 declarations; validate: only the 14 pre-existing + `conv:` errors. `leanblueprint pdf` and `web` succeed; final print.log has no undefined + references and no overfull boxes; three cosmetic underfull lines in the section. Temporal check + passes. Revision done. +- 2026-11-07. Second review: added `lmm:reeh-schlieder-monomial-orthogonal` (covers n = 0), + `lmm:reflection-domain-open`, `lmm:schwarz-reflection-continuous`; spectral-support union step + through the scalar measure μ_ψ; `lmm:diamond-translate` cites `def:inhomogeneous-lorentz-group` + (which states (L, a)·x = Lx + a); optional items 5 and 6 applied. +- 2026-11-07. Second-review checks: refresh 724 declarations; validate only the 14 pre-existing `conv:` errors; pdf and web succeed (no undefined refs, no overfull boxes, one cosmetic underfull heading); temporal check passes; cited Mathlib names confirmed by grep. Done. diff --git a/notes/agents/reeh-schlieder-formalization-progress.md b/notes/agents/reeh-schlieder-formalization-progress.md new file mode 100644 index 0000000..1f7c49d --- /dev/null +++ b/notes/agents/reeh-schlieder-formalization-progress.md @@ -0,0 +1,31 @@ +# Reeh–Schlieder formalization progress + +- 2026-11-07: Physicslib4/Analysis/EdgeVanishing.lean written (lmm:reflection-domain-open, lmm:reflection-domain-connected, lmm:schwarz-reflection-continuous, lmm:schwarz-reflection-zero, lmm:edge-vanishing); sorry-only diagnostics. +- 2026-11-07: Physicslib4/AQFT/PositiveEnergyHolomorphic.lean written (lmm:positive-spectral-support-interval, lmm:positive-spectral-support, lmm:exp-matrix-coefficient-polarization, lmm:fourier-laplace-continuous, lmm:fourier-laplace-holomorphic, lmm:positive-energy-holomorphic); sorry-only diagnostics. Root imports added. +- 2026-11-07: metadata recorded for all 11 labels and status set to formalized; Physicslib4 builds (only sorry warnings in the new files). +- 2026-11-07: reviewer fix: dropped unused `hIc : I.OrdConnected` from isOpen_im_ne_zero_union_image_ofReal, continuousOn_schwarzReflection_of_eq_zero, differentiableOn_schwarzReflection_of_eq_zero (docstrings now say open set I ⊆ ℝ); kept it in isConnected_im_ne_zero_union_image_ofReal. Names unchanged; EdgeVanishing and Physicslib4 rebuild. +- 2026-11-07: Physicslib4/AQFT/HaagKastler/ReehSchlieder/Translations.lean written (lmm:diamond-translate, lmm:diamond-small-translates, lmm:neighbourhood-partial-sums, lmm:future-timelike-basis); sorry-only diagnostics. +- 2026-11-07: same file, lmm:timelike-spreading-direction and lmm:timelike-spreading (U indexed by the translation vector, K₀ a closed Submodule); sorry-only diagnostics. Root import added; module and Physicslib4 build. Metadata recorded for all 6 labels, status formalized. +- 2026-11-07: batch 1 (analytic, 11 labels) reviewed: PASS after the hIc fix. Batch 2a (Translations.lean, 6 labels) review was cut off by the session limit; rerun pending. +- Next: batch 2b (cyclic-subspace and correlation lemmas, no new defs); batch 3 (def:translation-generated-algebra, def:weak-additivity, def:weak-additivity-von-neumann, then the theorem and corollaries) needs the user's lean_guard approval for new defs. +- 2026-11-07: batch 2a review rerun: four statements pass; the two spreading lemmas trimmed (orchestrator edit) to the group law at φ (`hmul : ∀ x y, U (x + y) φ = U x (U y φ)`), dropping K₀, hK₀, hinv, hφ, hn; docstrings note the blueprint's K₀ supplies it. Diagnostics: only sorry warnings. Optional later: restate the two blueprint nodes the same way. +- 2026-11-07: batch 2b part 1: Physicslib4/AQFT/HaagKastler/ReehSchlieder/CyclicSubspace.lean written (lmm:agree-on-cyclic-subspace, lmm:translations-cyclic-subspace-invariant, lmm:translations-intertwine-cyclic-subspace, lmm:translations-group-law-cyclic-subspace, lmm:covariant-translations-cyclic-subspace); K₀ = (Submodule.span ℂ (Set.range fun a => π a Ω)).topologicalClosure inline; group-law lemma gives `∀ φ ∈ K₀, ∀ x y, U (x + y) φ = U x (U y φ)` for inner_translation_eq_zero. Root import added; module builds (sorry warnings only). Metadata recorded, status formalized. +- 2026-11-07: batch 2b part 2: Physicslib4/AQFT/HaagKastler/ReehSchlieder/Correlations.lean written (lmm:translate-local-subalgebra, lmm:reeh-schlieder-translated-products, lmm:reeh-schlieder-vanishing-near-origin, lmm:reeh-schlieder-factorization, lmm:reeh-schlieder-correlations-vanish, lmm:reeh-schlieder-monomial-orthogonal). Ordered product = (List.ofFn fun i => (U (ξ i) : H →L[ℂ] H) * π (ι hB₁ (a i))).prod; partial sums ∑ j : Fin (i + 1), ξ (Fin.castLE i.isLt j); factorization via Function.update ξ k t. Root import added; module builds (sorry warnings only). Metadata recorded, status formalized. +- 2026-11-07: Correlations.lean review fixes (names unchanged): correlations-vanish and monomial-orthogonal take hB₁B : ∀ᶠ x in nhds 0, translationSub x • B₁ ⊆ B in place of V/hV/hV0/hVB; vanishing-near-origin drops V/hVB, hV₀ now concludes translationSub (∑ i, η i) • B₁ ⊆ B; factorization takes a : Fin n → N.quasilocal.carrier (no B₁); docstrings account for binder groups. +- 2026-11-07: batch 2b (11 labels, CyclicSubspace.lean + Correlations.lean) reviewed: all true and composable; signature-size fixes applied exactly as the reviewer specified (not re-reviewed). Remaining: batch 3 (needs guard approval for 3 defs), then proofs. +- 2026-11-07: batch 3: Physicslib4/AQFT/HaagKastler/ReehSchlieder/Additivity.lean written (3 defs: translationGeneratedAlgebra = topologicalClosure of StarAlgebra.adjoin of ⋃ x, range ι_{B+x}; IsWeaklyAdditive; IsWeaklyAdditiveVonNeumann with Set.range-over-subalgebra form; plus 3 lemmas, the theorem and 5 corollaries). lmm:bicommutant-orbit-closure checked to close by `apply_mem_closure_of_mem_bicommutant (π.comp (N.translationGeneratedAlgebra hB).subtype) (T := T) hT Ω` (left as sorry). Root import added; module builds (sorry warnings only). Metadata recorded for 12 labels (13th listed label lmm:bicommutant-single-vector was already recorded upstream). +- 2026-11-07: batch 3 status set to formalized (the 3 defs normalized to terminal by the tool); Physicslib4 builds (sorry warnings only in new file). Review pending. +- 2026-11-07: batch 3 (Additivity.lean: 3 defs + 9 theorems) reviewed: PASS. Optional: drop ω/hω/hrep from reeh_schlieder_cyclic_of_vacuum (unused) after rewording crllr:reeh-schlieder-vacuum. All 41 nodes of §10.9 now formalized (statements); next: proofs. +- 2026-11-07: EdgeVanishing.lean fully proved (5 lemmas). Unused-hypothesis warnings: hI in continuousOn_schwarzReflection_of_eq_zero; hI, hIc in isConnected_im_ne_zero_union_image_ofReal (cleanup later). +- 2026-11-07: PositiveEnergyHolomorphic.lean: 5 of 6 proved (spectral-support interval and full, polarization, both Fourier–Laplace). Remaining: IsPositiveEnergy.exists_holomorphic_extension (prover cut off by the session limit; no partial edits left). +- 2026-11-07: PositiveEnergyHolomorphic.lean fully proved (6 lemmas); module builds with no warnings from this file. Analytic preliminaries complete (12 of 12 incl. removability). Next: Translations.lean (6). +- 2026-11-07: Translations.lean: 4 more proved (diamond-translate, neighbourhood-partial-sums, future-timelike-basis, timelike-spreading-direction). Module builds; remaining sorries: exists_diamond_translate_subset, inner_translation_eq_zero. +- 2026-11-07: Translations.lean fully proved (6). CyclicSubspace: apply_eq_of_mem_cyclicSubspace proved (one line, ContinuousLinearMap.eqOn_closure_span). 19 of 41 proved. +- 2026-11-07: proved translations_cyclicSubspace_invariant, translations_intertwine_cyclicSubspace, translations_add_cyclicSubspace, action_translationSub_image_range_ι. Correlations builds. 23 of 41 proved; remaining: covariant_translations_cyclicSubspace (bundle), 5 in Correlations, 9 in Additivity. +- 2026-11-08: proved covariant_translations_cyclicSubspace, translated_products_apply, inner_translated_products_update_eq_inner. CyclicSubspace.lean complete. 26 of 41 proved. +- 2026-11-08: proved inner_translated_products_eq_zero_of_mem, IsWeaklyAdditive.isWeaklyAdditiveVonNeumann, apply_mem_closure_translationGeneratedAlgebra. 29 of 41 proved. +- 2026-11-08: proved inner_translated_products_eq_zero (vanishing induction). 30 of 41 proved. +- 2026-11-08: proved inner_monomial_eq_zero (Correlations.lean complete) and inner_adjoin_translates_eq_zero. 32 of 41 proved; remaining: reeh_schlieder + 5 corollaries. +- 2026-11-08: proved reeh_schlieder (main theorem) and reeh_schlieder_cyclic. 34 of 41 proved; remaining: the von Neumann, weak-additivity, vacuum and separating corollaries. +- 2026-11-08: proved the four remaining corollaries (von Neumann, separating, weak additivity, vacuum). §10.9 complete: all 41 nodes proved; full lake build of Physicslib4 succeeds with 0 sorry warnings. Remaining cleanup: unused hI/hIc in EdgeVanishing.lean; unused hω/hrep in reeh_schlieder_cyclic_of_vacuum (blueprint rewording would allow dropping them). +- 2026-11-08: crllr:reeh-schlieder-vacuum reworded (implementation and spectrum conditions of a vacuum state); reeh_schlieder_cyclic_of_vacuum drops ω, hω, hrep. Full build: 0 sorry, no warnings in Additivity.lean. diff --git a/notes/agents/review-manual-ch-reeh-schlieder-2026-11-08.md b/notes/agents/review-manual-ch-reeh-schlieder-2026-11-08.md new file mode 100644 index 0000000..fa58d27 --- /dev/null +++ b/notes/agents/review-manual-ch-reeh-schlieder-2026-11-08.md @@ -0,0 +1,106 @@ +# Review: manual chapter "The Reeh–Schlieder theorem" (2026-11-08) + +Scope: `web/Manual/ReehSchlieder.lean`, and the edited passages in `web/Manual/NotProved.lean`, +`web/Manual/HaagKastler.lean`, `web/Manual/Curved.lean` and `web/Manual/Conventions.lean`. +Checked against `blueprint/src/sections/sec10/reeh-schlieder.tex` and the Lean statements and +docstrings in `Physicslib4/AQFT/HaagKastler/ReehSchlieder/*.lean`, +`Physicslib4/AQFT/PositiveEnergyHolomorphic.lean`, `Physicslib4/Analysis/EdgeVanishing.lean`, plus +`PositiveEnergy.lean`, `LocalVonNeumann.lean` and `VacuumState.lean` where the chapter relies on them. + +VERDICT: REVISE (4 blocking findings, all one-sentence wording fixes; the mathematics and the +names are otherwise correct). + +## What was verified (no action needed) + +- Blueprint links: all 16 labels used in the chapter (`sctn:`, `def:`, `lmm:`, `thrm:`, `crllr:`) + exist as `\label{...}` in `reeh-schlieder.tex`. +- Lean names: all 30 distinct `{docstring}` / `{apiDocs}` names exist with the exact fully + qualified name (namespaces checked: `Physicslib4.AQFT.HaagKastler[.HaagKastlerNet]`, + `Physicslib4.AQFT`, `Physicslib4`). None is `private`. `localVonNeumannAlgebra_separating` is in + `HaagKastlerNet` (`HaagKastler/LocalVonNeumann.lean:29,206`). The `#check` outputs come from the + successful build. +- No `sorry` in the six source files, so line 94 ("with no `sorry`") is accurate. +- `reeh_schlieder` hypotheses: π, Ω, U, hU, hpos, hB₁, hB, hB₁B. No additivity and no cyclicity + (lines 68–74, 114–129 are accurate). +- Nonempty diamonds: `IsWeaklyAdditive` and `IsWeaklyAdditiveVonNeumann` quantify over nonempty B; + every cyclicity corollary has `hne : B.Nonempty`; `hcyc` of `reeh_schlieder_cyclic` and + `reeh_schlieder_separating` has `B'.Nonempty`; C may be empty in the separating corollary. + The empty-diamond paragraph (lines 133–141) matches blueprint line 157. +- Chain (lines 160–169): `IsWeaklyAdditive.isWeaklyAdditiveVonNeumann` holds for every π; the + second step needs Ω cyclic for π(𝔘) and uses `apply_mem_closure_translationGeneratedAlgebra`. + Matches blueprint lines 193 and 480. +- Vacuum corollary: hypotheses are hwa, π, Ω, U (indexed by the Poincaré group), hU, hpos, hcyc. + No state, no reproduction condition. Matches the docstring and blueprint line 501. +- Separating corollary uses `IsCompletelySpacelike ... B C`, matching blueprint line 514. +- Proof route: one complex variable, one future-timelike direction at a time, no joint spectral + measure (blueprint line 3). The basis `e₀`, `e₀ + ½eᵢ` matches `futureTimelike_basis`. The group + law only at φ (`hmul`) matches `inner_translation_eq_zero_add_smul`. `IsPositiveEnergy` allows an + unbounded positive generator (`PositiveEnergy.lean:16–17,74`), so line 181 is accurate. +- Curved spacetime: NotProved.lean and Curved.lean say correctly that Reeh–Schlieder is proved + only for Minkowski; the curved axioms carry no spectrum condition (`Curved.lean:511`). + Conventions.lean: "the intersection property for general spacetimes" is a real appendix entry + (`NotProved.lean:50`). +- Nothing claims that a vacuum state of a nontrivial net exists (`HaagKastler.lean:607` keeps "It + does not construct a vacuum state of a nontrivial net"). +- Style: `python3 scripts/check_temporal_wording.py` reports "OK: no temporal wording or stray + version strings." No absolute paths and no version numbers. Every `lean` input code line is at + most 60 columns. The long lines are in `leanOutput` blocks, which are verbatim Lean output and + are also long in `Stone.lean` and `HaagKastler.lean`. + +## Blocking findings + +1. **`web/Manual/ReehSchlieder.lean:56-57`: "unconditionally" overclaims.** Cyclicity for local + algebras needs an additivity hypothesis and Ω cyclic for π(𝔘) (see the chapter's own + lines 116–118). Replace + "Its cyclicity hypothesis is exactly what the Reeh–Schlieder theorem supplies, + so for the vacuum the property holds unconditionally." + with + "Its cyclicity hypothesis is exactly what the Reeh–Schlieder theorem supplies, + so for the vacuum of a weakly additive net the property needs no separate cyclicity + hypothesis." + +2. **`web/Manual/ReehSchlieder.lean:61-64`: the modular-theory bullet is not marked as + unformalized.** Append to the end of the bullet (after "restricted to a wedge."): + " None of these is formalized in the library; they are mentioned as context." + +3. **`web/Manual/ReehSchlieder.lean:206-207`: "which is the case for the GNS representation" + claims more than the library proves.** The library's covariant GNS result for a vacuum state + (`IsVacuumState.exists_gns_irreducible_covariant`) assumes purity and, by its docstring + (`VacuumState.lean:159-162`), does not use the spectrum condition. So no Lean result shows + that the GNS data satisfy `hpos`. Replace + "The statement therefore applies to the witnessing data of every vacuum state with $`\Omega` + cyclic, which is the case for the GNS representation." + with + "The statement therefore applies to the witnessing data of every vacuum state for which + $`\Omega` is cyclic for $`\pi(\mathfrak{U})`." + +4. **`web/Manual/HaagKastler.lean:468-470` (edited passage): leaves out the additivity + hypothesis.** The chapter itself says cyclicity cannot hold without one. Replace + "In a vacuum representation the cyclicity is supplied by the + Reeh–Schlieder theorem ({ref "reeh-schlieder"}[The Reeh–Schlieder theorem]), and the corollary + `reeh_schlieder_separating` combines the two; here cyclicity is a hypothesis." + with + "In a vacuum representation of a weakly additive net, with $`\Omega` cyclic for + $`\pi(\mathfrak{U})`, the cyclicity is supplied by the Reeh–Schlieder theorem + ({ref "reeh-schlieder"}[The Reeh–Schlieder theorem]), and the corollary + `reeh_schlieder_separating` combines the two; here cyclicity is a hypothesis." + +## Optional findings + +5. **`web/Manual/ReehSchlieder.lean:41-43`.** The overview states the theorem before mentioning + additivity. Suggested: "For every nonempty diamond $`\mathbf{B}`, however small, and under a + mild additivity assumption on the net discussed below, $`\Omega` is already cyclic for the + local algebra $`\pi(\mathfrak{U}(\mathbf{B}))`: ..." + +6. **`web/Manual/HaagKastler.lean:609-611`.** "The consequences that do use the spectrum + condition, the Reeh–Schlieder theorem and its corollaries, are in ..." reads as an exhaustive + list. Suggested: "The Reeh–Schlieder theorem and its corollaries, which use the spectrum + condition, are in {ref "reeh-schlieder"}[The Reeh–Schlieder theorem]." + +7. **`web/Manual/ReehSchlieder.lean:133`.** For precision, replace "for $`q` not in the future of + $`p`" with "for $`q` not in the chronological future $`I^+(p)` of $`p`". + +8. **`web/Manual/Conventions.lean:108-111`.** The source lines are ragged ("are marked where / + they arise and collected / in the"). This is cosmetic only, since the rendering is unaffected. + Reflow to: "existence of pure states and the intersection property for general spacetimes, are + marked where they arise and collected in the {ref "not-proved"}[appendix]. Where ..." diff --git a/web/Manual.lean b/web/Manual.lean index ed41d95..796ca67 100644 --- a/web/Manual.lean +++ b/web/Manual.lean @@ -6,6 +6,7 @@ import Manual.Stone import Manual.Spacetime import Manual.HaagKastler import Manual.Curved +import Manual.ReehSchlieder import Manual.Conventions import Manual.NotProved import Manual.FeatureTests @@ -37,6 +38,8 @@ are listed in the {ref "not-proved"}[appendix]. {include 1 Manual.Curved} +{include 1 Manual.ReehSchlieder} + {include 1 Manual.Conventions} {include 1 Manual.NotProved} diff --git a/web/Manual/Conventions.lean b/web/Manual/Conventions.lean index 54d818c..ee16247 100644 --- a/web/Manual/Conventions.lean +++ b/web/Manual/Conventions.lean @@ -106,7 +106,8 @@ the present tense. Its history is kept in one place, `CHANGELOG.md` at the root repository. _Where the library stops._ The standard facts that the library does not prove, such as the -Reeh–Schlieder theorem and the existence of pure states, are marked where they arise and collected +existence of pure states and the intersection property for general spacetimes, are marked where +they arise and collected in the {ref "not-proved"}[appendix]. Where a theorem depends on one of them, it is a hypothesis of that theorem. diff --git a/web/Manual/Curved.lean b/web/Manual/Curved.lean index 10b14d3..87afdd6 100644 --- a/web/Manual/Curved.lean +++ b/web/Manual/Curved.lean @@ -445,7 +445,8 @@ Schlieder property, {apiDocs Physicslib4.AQFT.HaagKastlerCurved.HaagKastlerNet.localVonNeumannAlgebra_separating}[`localVonNeumannAlgebra_separating`], says that if $`\mathbf{B}_1` and $`\mathbf{B}_2` are completely spacelike and $`\Omega` is cyclic for the local operators of $`\mathbf{B}_1`, then $`\Omega` is separating for $`R(\mathbf{B}_2)`. -The library has no Reeh–Schlieder theorem, so cyclicity is a hypothesis. The +The library's Reeh–Schlieder theorem ({ref "reeh-schlieder"}[The Reeh–Schlieder theorem]) is for +Minkowski spacetime, so here cyclicity is a hypothesis. The relative commutant $`R(\mathbf{B}_1)' \cap R(\mathbf{B}_2)` is {apiDocs Physicslib4.AQFT.HaagKastlerCurved.HaagKastlerNet.relativeCommutant}[`relativeCommutant`]; the inclusion of $`R(\mathbf{B}')` in itself is irreducible exactly when $`R(\mathbf{B}')` is a diff --git a/web/Manual/HaagKastler.lean b/web/Manual/HaagKastler.lean index 9c5cc00..502c6a7 100644 --- a/web/Manual/HaagKastler.lean +++ b/web/Manual/HaagKastler.lean @@ -465,8 +465,10 @@ Physicslib4.AQFT.HaagKastler.HaagKastlerNet.localVonNeumannAlgebra_le_commutant. Statistical independence (the Schlieder property): if $`\mathbf{B}_1` and $`\mathbf{B}_2` are completely spacelike and a vector $`\Omega` is cyclic for the local operators of $`\mathbf{B}_1`, then $`\Omega` is separating for $`R(\mathbf{B}_2)`, so an element of $`R(\mathbf{B}_2)` that -annihilates $`\Omega` is zero. In a vacuum representation the cyclicity is the content of the -Reeh–Schlieder theorem, which the library does not prove; it is a hypothesis here. +annihilates $`\Omega` is zero. In a vacuum representation of a weakly additive net, with +$`\Omega` cyclic for $`\pi(\mathfrak{U})`, the cyclicity is supplied by the +Reeh–Schlieder theorem ({ref "reeh-schlieder"}[The Reeh–Schlieder theorem]), and the corollary +`reeh_schlieder_separating` combines the two; here cyclicity is a hypothesis. ```lean (name := checkSeparating) open Physicslib4 AQFT HaagKastler in @@ -604,8 +606,9 @@ The library proves the consequences of a vacuum state that do not use the spectr invariant (`HaagKastlerNet.IsVacuumState.invariant`), and if it is pure its GNS representation is covariant and irreducible ({apiDocs Physicslib4.AQFT.HaagKastler.HaagKastlerNet.IsVacuumState.exists_gns_irreducible_covariant}[`IsVacuumState.exists_gns_irreducible_covariant`]). -It does not construct a vacuum state of a nontrivial net, and it does not prove the Reeh–Schlieder -theorem. +It does not construct a vacuum state of a nontrivial net. The consequences that do use the spectrum +condition, the Reeh–Schlieder theorem and its corollaries, are in +{ref "reeh-schlieder"}[The Reeh–Schlieder theorem]. Thermal equilibrium is described by KMS states. In Minkowski spacetime every Poincaré transformation acts on the one algebra $`\mathfrak{U}`, so a one-parameter subgroup $`t \mapsto diff --git a/web/Manual/NotProved.lean b/web/Manual/NotProved.lean index dd6edd8..4b17b0c 100644 --- a/web/Manual/NotProved.lean +++ b/web/Manual/NotProved.lean @@ -78,10 +78,11 @@ tag := "not-proved-minkowski" C\*-algebras are isometric; the library constructs one and states its results for every quasilocal algebra, but does not prove uniqueness ([Haag–Kastler chapter](Haag-Kastler-axioms-in-Minkowski-spacetime/#physicslib4-reference-manual--The-Haag___Kastler-axioms-in-Minkowski-spacetime--Design--The-quasilocal-algebra-is-constructed)). -* _The Reeh–Schlieder theorem._ In a vacuum representation the vacuum is cyclic for the algebra - of every nonempty diamond. The library does not prove it, so the Schlieder property takes - cyclicity as a hypothesis, in Minkowski and in curved spacetime - ([Haag–Kastler chapter](Haag-Kastler-axioms-in-Minkowski-spacetime/#physicslib4-reference-manual--The-Haag___Kastler-axioms-in-Minkowski-spacetime--Main-definitions-and-theorems--Representations-and-local-von-Neumann-algebras)). +* _The Reeh–Schlieder theorem in curved spacetime._ The library proves the Reeh–Schlieder theorem + in Minkowski spacetime ({ref "reeh-schlieder"}[The Reeh–Schlieder theorem]). In curved spacetime, + where the axioms carry no spectrum condition, it does not, so the curved Schlieder property takes + cyclicity as a hypothesis + ([curved chapter](The-axioms-in-curved-spacetime-and-general-covariance/)). * _The spectrum condition in its joint-spectrum form._ The library states the spectrum condition as positive energy along every future-timelike translation. Its equivalence with the textbook form, that the joint spectrum of the energy-momentum operators lies in the closed forward cone, diff --git a/web/Manual/ReehSchlieder.lean b/web/Manual/ReehSchlieder.lean new file mode 100644 index 0000000..4c11595 --- /dev/null +++ b/web/Manual/ReehSchlieder.lean @@ -0,0 +1,551 @@ +import VersoManual +import Book.Meta +import Physicslib4.AQFT.PositiveEnergyHolomorphic +import Physicslib4.Analysis.EdgeVanishing +import Physicslib4.AQFT.HaagKastler.ReehSchlieder.Translations +import Physicslib4.AQFT.HaagKastler.ReehSchlieder.CyclicSubspace +import Physicslib4.AQFT.HaagKastler.ReehSchlieder.Correlations +import Physicslib4.AQFT.HaagKastler.ReehSchlieder.Additivity + +open Verso.Genre Manual +open Verso.Genre.Manual.InlineLean +open Book +-- Docstring code spans are elaborated in this scope; these namespaces let the names they mention, +-- written relative to the library's namespaces, resolve and link. +open Physicslib4 Physicslib4.AQFT Physicslib4.AQFT.HaagKastler +open Physicslib4.AQFT.HaagKastler.HaagKastlerNet + +#doc (Manual) "The Reeh–Schlieder theorem" => + +%%% +tag := "reeh-schlieder" +file := "The-Reeh-Schlieder-theorem" +%%% + +This chapter describes how the library states and proves the Reeh–Schlieder theorem for a +Haag–Kastler net in Minkowski spacetime. It corresponds to +[Section 10.9](https://physicslib.github.io/physicslib4/blueprint/chptr-haag-kastler-axioms-blueprint.html#sctn:reeh-schlieder) +of the blueprint. It builds on the {ref "haag-kastler"}[Minkowski chapter], which supplies the net, +its quasilocal algebra $`\mathfrak{U}`, the covariance action $`L \mapsto \beta_L` and the local von +Neumann algebras, and on the {ref "stone"}[chapter on Stone's theorem], which supplies positive +energy, the form in which the library states the spectrum condition. + +# Overview +%%% +tag := "reeh-schlieder-overview" +%%% + +As you will recall, the vacuum vector $`\Omega` of a quantum field theory is _cyclic_ for the +algebra of all observables: the vectors $`A\Omega`, with $`A` ranging over the quasilocal algebra, +are dense in the Hilbert space. Physically, every state of the theory can be approximated by acting +on the vacuum with observables. The Reeh–Schlieder theorem says something much stronger. For every +nonempty diamond $`\mathbf{B}`, however small, $`\Omega` is already cyclic for the local algebra +$`\pi(\mathfrak{U}(\mathbf{B}))`: operations confined to an arbitrarily small region of spacetime +approximate, to arbitrary accuracy, every state of the theory, including states localised far away +in spacelike separation. + +The theorem looks paradoxical and is not. It does not allow signalling, because the operators that +do the approximating are not unitary and their effect is not a physical operation that one observer +can perform with certainty. What it does show is that the vacuum is highly entangled across every +spacelike boundary. It has three consequences that the rest of algebraic quantum field theory uses +constantly: + +* _Statistical independence._ The Schlieder property, which the Minkowski chapter calls + statistical independence, says: if $`\mathbf{B}_1` and $`\mathbf{B}_2` are completely spacelike + and $`\Omega` is cyclic for $`\pi(\mathfrak{U}(\mathbf{B}_1))`, then $`\Omega` is separating for + $`R(\mathbf{B}_2)`. Its cyclicity hypothesis is exactly what the Reeh–Schlieder theorem supplies, + so for the vacuum of a weakly additive net the property needs no separate cyclicity hypothesis. +* _The vacuum is separating._ Combining the two, no nonzero local observable of a region with + spacelike room around it annihilates the vacuum: a local detector placed in the vacuum has a + nonzero probability of clicking. +* _Modular theory._ A vector that is both cyclic and separating for a von Neumann algebra is + exactly the input of Tomita–Takesaki theory. The Reeh–Schlieder theorem therefore starts the + modular theory of local algebras, and through it the Bisognano–Wichmann theorem and the KMS + property of the vacuum restricted to a wedge. None of these is formalized in the library; they + are mentioned as context. + +The library proves the theorem in two stages, following the blueprint. + +The main theorem, `reeh_schlieder`, assumes no additivity property of the net. Its hypotheses are +a \*-representation $`\pi` of $`\mathfrak{U}` on a Hilbert space $`H`, a vector $`\Omega`, and +unitaries $`U(x)`, $`x \in \mathbb{R}^4`, that implement the translations on the vectors +$`\pi(a)\Omega` and have positive energy along every future-timelike direction. If a diamond +$`\mathbf{B}` contains every small translate of a diamond $`\mathbf{B}_1`, it concludes that the +vectors $`\pi(A)\Omega`, with $`A` in the algebra $`\mathfrak{A}_{\mathbf{B}_1}` generated by all +translates of $`\mathfrak{U}(\mathbf{B}_1)`, lie in the closure of $`\pi(\mathfrak{U}(\mathbf{B}))\Omega`. +In words: whatever you can reach from the vacuum with operators localised anywhere in spacetime, +built from translates of a small region, you can already reach with operators localised in a +slightly larger region. + +Corollaries turn this into cyclicity, under three hypotheses of increasing strength: + +* `reeh_schlieder_cyclic`: $`\Omega` is cyclic for every translation-generated algebra + $`\pi(\mathfrak{A}_{\mathbf{B}'})`; +* `reeh_schlieder_cyclic_of_vonNeumann`: $`\Omega` is cyclic for $`\pi(\mathfrak{U})` and $`\pi` + satisfies the von Neumann form of weak additivity; +* `reeh_schlieder_cyclic_of_weaklyAdditive`: $`\Omega` is cyclic for $`\pi(\mathfrak{U})` and the + net is weakly additive. + +Each concludes that $`\Omega` is cyclic for $`\pi(\mathfrak{U}(\mathbf{B}))` for every nonempty +diamond $`\mathbf{B}`. The vacuum form, `reeh_schlieder_cyclic_of_vacuum`, states the last of these +for the implementation and spectrum data of a vacuum state. The separating form, +`reeh_schlieder_separating`, concludes that $`\Omega` is separating for the local von Neumann +algebra of every diamond completely spacelike to a nonempty diamond. + +Every statement of Section 10.9 is proved in Lean, with no `sorry`. The theorem and its +corollaries are in the namespace `Physicslib4.AQFT.HaagKastler`, the holomorphic extension under +positive energy is in `Physicslib4.AQFT`, and the complex-analysis lemma on vanishing on an edge is +in `Physicslib4`. + +# Design +%%% +tag := "reeh-schlieder-design" +%%% + +The conventions of the {ref "haag-kastler-design"}[Minkowski chapter] carry over. A diamond is an +Alexandrov basis set $`I^+(p) \cap I^-(q)`, the predicate `IsAlexandrovBasisSet`; the local algebra +of $`\mathbf{B}` inside $`\mathfrak{U}` is the range of the embedding $`\iota_{\mathbf{B}}`; the +translate of a diamond is $`\mathbf{B} + x = \mathrm{translationSub}(x) \cdot \mathbf{B}`, again a +diamond; and $`\beta_x` is the action of $`\mathrm{translationSub}(x)` on $`\mathfrak{U}`. A +\*-representation is a \*-algebra homomorphism `N.quasilocal.carrier →⋆ₐ[ℂ] (H →L[ℂ] H)`, and a +unitary is a linear isometry equivalence `H ≃ₗᵢ[ℂ] H`. A vector is cyclic for a set of operators +when its orbit is dense, and the library states each cyclicity conclusion directly as `Dense` of +that orbit. + +## The main theorem assumes no additivity + +The cyclicity of $`\Omega` for a local algebra cannot hold without some hypothesis linking the +local algebras to the whole of $`\mathfrak{U}`: a net could assign to every diamond the algebra +$`\mathbb{C}\mathbf{1}`, and then nothing local reaches beyond $`\Omega` itself. In the literature +the link is an additivity property of the net. The library separates the analytic content of the +theorem from this link. The main theorem, `reeh_schlieder`, assumes no additivity at all; it +compares two sets of vectors that the net defines in any case, $`\pi(\mathfrak{A}_{\mathbf{B}_1})\Omega` +and the closure of $`\pi(\mathfrak{U}(\mathbf{B}))\Omega`. Additivity enters only in the +corollaries, and only to identify the closure of $`\pi(\mathfrak{A}_{\mathbf{B}'})\Omega` with all +of $`H`. A reader with a different additivity assumption can derive cyclicity from the main +theorem directly. + +The main theorem also assumes nothing about $`\Omega` beyond the implementation condition. It +does not assume $`\Omega` cyclic for $`\pi(\mathfrak{U})`, nor a unit vector, nor invariant; +invariance under the $`U(x)` follows from the implementation condition with $`a = 1`. + +## The corollaries quantify over nonempty diamonds + +The empty set is a diamond, $`I^+(p) \cap I^-(q)` for $`q` not in the future of $`p`, and Axiom 1 +assigns it the trivial algebra $`\mathfrak{U}(\emptyset) = \mathbb{C}\mathbf{1}`. Every translate of +the empty set is empty, so $`\mathfrak{A}_\emptyset = \mathbb{C}\mathbf{1}` too. Weak additivity as +"$`\mathfrak{A}_{\mathbf{B}} = \mathfrak{U}` for every diamond" would therefore force +$`\mathfrak{U} = \mathbb{C}\mathbf{1}`, and cyclicity of $`\Omega` for $`\mathfrak{U}(\emptyset)` +would force $`H` to be at most one-dimensional. The additivity conditions, the cyclicity hypothesis +of `reeh_schlieder_cyclic` and every cyclicity conclusion are therefore stated for nonempty +diamonds, through a hypothesis `B.Nonempty`. The main theorem needs no such hypothesis, since for +empty $`\mathbf{B}_1` it states only that $`\Omega` lies in the closure of $`\mathbb{C}\Omega`. + +## Weak additivity is a hypothesis, in three forms + +Weak additivity is not one of the Haag–Kastler axioms of the library, and it is not added to +`HaagKastlerNet`: it is a predicate on a net, assumed by the results that need it. The library has +three forms of it, from the weakest assumption to the strongest: + +* _Cyclicity for the translation-generated algebras_: $`\Omega` is cyclic for + $`\pi(\mathfrak{A}_{\mathbf{B}})` for every nonempty diamond $`\mathbf{B}`. This is the hypothesis + of `reeh_schlieder_cyclic`. It is not given a name, because it concerns one vector and one + representation and is used only there. +* _The von Neumann form_, `HaagKastlerNet.IsWeaklyAdditiveVonNeumann`: for one representation + $`\pi`, $`\pi(\mathfrak{U}) \subseteq \pi(\mathfrak{A}_{\mathbf{B}})''` for every nonempty + diamond. It allows $`\mathfrak{A}_{\mathbf{B}}` to be smaller than $`\mathfrak{U}` provided it + generates the same von Neumann algebra in the representation. +* _Weak additivity_, `HaagKastlerNet.IsWeaklyAdditive`: $`\mathfrak{A}_{\mathbf{B}} = \mathfrak{U}` + for every nonempty diamond. It concerns the net alone. + +They are related by + +$$`\text{weak additivity} \;\Longrightarrow\; \text{von Neumann form for every } \pi \;\Longrightarrow\; \Omega \text{ cyclic for every } \pi(\mathfrak{A}_{\mathbf{B}}),` + +the second implication under the assumption that $`\Omega` is cyclic for $`\pi(\mathfrak{U})`. +The first is `HaagKastlerNet.IsWeaklyAdditive.isWeaklyAdditiveVonNeumann`, since every set lies in +its bicommutant. The second uses that the closure of $`\pi(\mathfrak{A}_{\mathbf{B}})\Omega` +contains $`\pi(\mathfrak{A}_{\mathbf{B}})''\Omega`, a consequence of von Neumann's bicommutant +theorem for a single vector, and hence the dense set $`\pi(\mathfrak{U})\Omega`. The three cyclicity +corollaries follow the same chain: each is the previous one composed with one implication. + +## Positive energy one direction at a time + +The textbook proof uses the spectrum condition in its joint form: the energy–momentum operators +$`P^\mu` have a joint spectral measure supported in the closed forward cone, so +$`x \mapsto U(x)\varphi` extends holomorphically to the forward tube +$`\mathbb{R}^4 + iV_+`. The library has no joint spectral measure for commuting unbounded operators, +and the proof does not need one. It continues analytically in one complex variable at a time, along +one future-timelike direction at a time. + +For a future-pointing timelike $`n`, the one-parameter group $`t \mapsto U(tn)` has positive +energy, that is, $`U(tn) = e^{itA}` with $`A` positive and self-adjoint. Every matrix coefficient +$`t \mapsto \langle \chi, U(tn)\varphi \rangle` is then the boundary value of a function +holomorphic on the upper half-plane and bounded and continuous on its closure. If the matrix +coefficient vanishes on an open interval of $`t`, Schwarz reflection and the identity theorem make it +vanish for all $`t`. So a function $`x \mapsto \langle \chi, U(x)\varphi \rangle` that vanishes on +an open set $`W` vanishes on $`W + \mathbb{R}n`. Applying this to the four future-timelike vectors +$`e_0` and $`e_0 + \tfrac{1}{2}e_i`, which form a basis of $`\mathbb{R}^4`, spreads the vanishing +from any nonempty open set to all of $`\mathbb{R}^4`. The spectrum condition is used only in the +per-direction form that the library states, `IsPositiveEnergy` of each future-timelike translation +subgroup, so the proof needs no structure beyond it. + +The group law of $`U` is needed in the spreading step, and the hypotheses do not include it: the +unitaries are only assumed to implement the translations on the vectors $`\pi(a)\Omega`. The library +proves that on the cyclic subspace $`K_0`, the closure of $`\pi(\mathfrak{U})\Omega`, the +$`U(x)` satisfy $`U(x + y) = U(x)U(y)` and intertwine $`\pi` with $`\beta`, and runs the argument +inside $`K_0`. Cyclicity of $`\Omega` is not assumed, so $`K_0` may be a proper subspace of $`H`. + +## The vacuum corollary needs only implementation and spectrum + +A vacuum state in the library (`HaagKastlerNet.IsVacuumState`) is a state $`\omega` together with +the existence of a representation $`(K, \pi, \Omega)` and unitaries $`U(L)` that reproduce +$`\omega`, implement the Poincaré action and satisfy the spectrum condition. The corollary +`reeh_schlieder_cyclic_of_vacuum` takes the representation and the unitaries as data and assumes +only the implementation and spectrum conditions, plus cyclicity of $`\Omega` for +$`\pi(\mathfrak{U})` and weak additivity. The state itself, and the condition that the +representation reproduces it, play no role. The statement therefore applies to the witnessing data +of every vacuum state for which $`\Omega` is cyclic for $`\pi(\mathfrak{U})`. From the +Poincaré unitaries it uses only the translations $`U(\mathrm{translationSub}(x))` and the +positive energy of the subgroups $`t \mapsto U(\mathrm{translationFlow}(n)(t)) = U(tn)`. + +# Main definitions and theorems +%%% +tag := "reeh-schlieder-main" +%%% + +## Translation-generated algebras and weak additivity + +The algebra $`\mathfrak{A}_{\mathbf{B}}` is the C\*-subalgebra of $`\mathfrak{U}` generated by all +translates of the local algebra of $`\mathbf{B}` +([def:translation-generated-algebra](https://physicslib.github.io/physicslib4/blueprint/chptr-haag-kastler-axioms-blueprint.html#def:translation-generated-algebra)). +In Lean it is the topological closure of `StarAlgebra.adjoin` of the union of the ranges of the +embeddings $`\iota_{\mathbf{B} + x}`: + +{docstring Physicslib4.AQFT.HaagKastler.HaagKastlerNet.translationGeneratedAlgebra} + +Weak additivity +([def:weak-additivity](https://physicslib.github.io/physicslib4/blueprint/chptr-haag-kastler-axioms-blueprint.html#def:weak-additivity)) +says it is all of $`\mathfrak{U}`, written as equality with `⊤` in the lattice of star subalgebras: + +{docstring Physicslib4.AQFT.HaagKastler.HaagKastlerNet.IsWeaklyAdditive} + +The von Neumann form +([def:weak-additivity-von-neumann](https://physicslib.github.io/physicslib4/blueprint/chptr-haag-kastler-axioms-blueprint.html#def:weak-additivity-von-neumann)) +takes the commutant in the bounded operators on $`H` as Mathlib's `Set.centralizer`, as the local +von Neumann algebras do: + +{docstring Physicslib4.AQFT.HaagKastler.HaagKastlerNet.IsWeaklyAdditiveVonNeumann} + +The first implication between them +([lmm:weak-additivity-von-neumann](https://physicslib.github.io/physicslib4/blueprint/chptr-haag-kastler-axioms-blueprint.html#lmm:weak-additivity-von-neumann)) +holds for every representation: + +```lean (name := checkWAVN) +open Physicslib4 AQFT HaagKastler in +#check + HaagKastlerNet.IsWeaklyAdditive.isWeaklyAdditiveVonNeumann +``` + +```leanOutput checkWAVN +Physicslib4.AQFT.HaagKastler.HaagKastlerNet.IsWeaklyAdditive.isWeaklyAdditiveVonNeumann.{u_1, u_2} {H : Type u_1} + [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {N : HaagKastlerNet} (hN : N.IsWeaklyAdditive) + (π : N.quasilocal.carrier →⋆ₐ[ℂ] H →L[ℂ] H) : N.IsWeaklyAdditiveVonNeumann π +``` + +## The theorem + +The main theorem +([thrm:reeh-schlieder](https://physicslib.github.io/physicslib4/blueprint/chptr-haag-kastler-axioms-blueprint.html#thrm:reeh-schlieder)) +has four groups of hypotheses. The covariant setting is `π`, `Ω`, `U` and `hU`, the implementation +condition $`U(x)\pi(a)\Omega = \pi(\beta_x a)\Omega`. Positive energy is `hpos`: for every $`n` in +the open forward cone, `IsPositiveEnergy fun t => U (t • n)`. The geometry is `hB₁B`: eventually +in the neighbourhood filter of $`0`, that is, for every $`x` in some neighbourhood of $`0`, +$`\mathbf{B}_1 + x \subseteq \mathbf{B}`. The conclusion is pointwise: for every +$`A \in \mathfrak{A}_{\mathbf{B}_1}`, $`\pi(A)\Omega` lies in the closure of the orbit of +$`\Omega` under the local algebra of $`\mathbf{B}`. + +```lean (name := checkRS) +open Physicslib4 AQFT HaagKastler in +#check reeh_schlieder +``` + +```leanOutput checkRS +Physicslib4.AQFT.HaagKastler.reeh_schlieder.{u_1, u_2} {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] + [CompleteSpace H] {N : HaagKastlerNet} (π : N.quasilocal.carrier →⋆ₐ[ℂ] H →L[ℂ] H) (Ω : H) + (U : StandardMinkowskiSpacetime.Carrier → H ≃ₗᵢ[ℂ] H) + (hU : + ∀ (x : StandardMinkowskiSpacetime.Carrier) (a : N.quasilocal.carrier), + (U x) ((π a) Ω) = (π ((N.action (translationSub x)) a)) Ω) + (hpos : ∀ n ∈ minkowskiForwardCone 0, IsPositiveEnergy fun t => U (t • n)) + {B₁ B : Set StandardMinkowskiSpacetime.Carrier} (hB₁ : IsAlexandrovBasisSet B₁) (hB : IsAlexandrovBasisSet B) + (hB₁B : ∀ᶠ (x : StandardMinkowskiSpacetime.Carrier) in nhds 0, translationSub x • B₁ ⊆ B) (A : N.quasilocal.carrier) : + A ∈ N.translationGeneratedAlgebra hB₁ → (π A) Ω ∈ closure (Set.range fun b => (π ((N.quasilocal.ι hB) b)) Ω) +``` + +## The cyclicity corollaries + +The first corollary +([crllr:reeh-schlieder-cyclic](https://physicslib.github.io/physicslib4/blueprint/chptr-haag-kastler-axioms-blueprint.html#crllr:reeh-schlieder-cyclic)) +assumes `hcyc`, cyclicity of $`\Omega` for $`\pi(\mathfrak{A}_{\mathbf{B}'})` for every nonempty +diamond $`\mathbf{B}'`. Given a nonempty diamond $`\mathbf{B}`, it picks a smaller nonempty +diamond $`\mathbf{B}_1` all of whose small translates stay in $`\mathbf{B}`, and applies the main +theorem. The conclusion uses `HaagKastlerNet.localOperators`, the set of operators +$`\pi(\iota_{\mathbf{B}}(b))`. + +```lean (name := checkRSCyclic) +open Physicslib4 AQFT HaagKastler in +#check reeh_schlieder_cyclic +``` + +```leanOutput checkRSCyclic +Physicslib4.AQFT.HaagKastler.reeh_schlieder_cyclic.{u_1, u_2} {H : Type u_1} [NormedAddCommGroup H] + [InnerProductSpace ℂ H] [CompleteSpace H] {N : HaagKastlerNet} (π : N.quasilocal.carrier →⋆ₐ[ℂ] H →L[ℂ] H) (Ω : H) + (U : StandardMinkowskiSpacetime.Carrier → H ≃ₗᵢ[ℂ] H) + (hU : + ∀ (x : StandardMinkowskiSpacetime.Carrier) (a : N.quasilocal.carrier), + (U x) ((π a) Ω) = (π ((N.action (translationSub x)) a)) Ω) + (hpos : ∀ n ∈ minkowskiForwardCone 0, IsPositiveEnergy fun t => U (t • n)) + (hcyc : + ∀ ⦃B' : Set StandardMinkowskiSpacetime.Carrier⦄ (hB' : IsAlexandrovBasisSet B'), + B'.Nonempty → Dense (Set.range fun a => (π ↑a) Ω)) + {B : Set StandardMinkowskiSpacetime.Carrier} (hB : IsAlexandrovBasisSet B) (hne : B.Nonempty) : + Dense ((fun T => T Ω) '' N.localOperators π hB) +``` + +Under the von Neumann form of weak additivity +([crllr:reeh-schlieder-von-neumann](https://physicslib.github.io/physicslib4/blueprint/chptr-haag-kastler-axioms-blueprint.html#crllr:reeh-schlieder-von-neumann)), +cyclicity for $`\pi(\mathfrak{U})` is `GNS.IsCyclicVector π Ω`, the predicate of the GNS chapter: + +```lean (name := checkRSvN) +open Physicslib4 AQFT HaagKastler in +#check reeh_schlieder_cyclic_of_vonNeumann +``` + +```leanOutput checkRSvN +Physicslib4.AQFT.HaagKastler.reeh_schlieder_cyclic_of_vonNeumann.{u_1, u_2} {H : Type u_1} [NormedAddCommGroup H] + [InnerProductSpace ℂ H] [CompleteSpace H] {N : HaagKastlerNet} (π : N.quasilocal.carrier →⋆ₐ[ℂ] H →L[ℂ] H) (Ω : H) + (U : StandardMinkowskiSpacetime.Carrier → H ≃ₗᵢ[ℂ] H) + (hU : + ∀ (x : StandardMinkowskiSpacetime.Carrier) (a : N.quasilocal.carrier), + (U x) ((π a) Ω) = (π ((N.action (translationSub x)) a)) Ω) + (hpos : ∀ n ∈ minkowskiForwardCone 0, IsPositiveEnergy fun t => U (t • n)) (hwa : N.IsWeaklyAdditiveVonNeumann π) + (hcyc : GNS.IsCyclicVector π Ω) {B : Set StandardMinkowskiSpacetime.Carrier} (hB : IsAlexandrovBasisSet B) + (hne : B.Nonempty) : Dense ((fun T => T Ω) '' N.localOperators π hB) +``` + +Under weak additivity +([crllr:reeh-schlieder-weak-additivity](https://physicslib.github.io/physicslib4/blueprint/chptr-haag-kastler-axioms-blueprint.html#crllr:reeh-schlieder-weak-additivity)): + +```lean (name := checkRSwa) +open Physicslib4 AQFT HaagKastler in +#check reeh_schlieder_cyclic_of_weaklyAdditive +``` + +```leanOutput checkRSwa +Physicslib4.AQFT.HaagKastler.reeh_schlieder_cyclic_of_weaklyAdditive.{u_1, u_2} {H : Type u_1} [NormedAddCommGroup H] + [InnerProductSpace ℂ H] [CompleteSpace H] {N : HaagKastlerNet} (π : N.quasilocal.carrier →⋆ₐ[ℂ] H →L[ℂ] H) (Ω : H) + (U : StandardMinkowskiSpacetime.Carrier → H ≃ₗᵢ[ℂ] H) + (hU : + ∀ (x : StandardMinkowskiSpacetime.Carrier) (a : N.quasilocal.carrier), + (U x) ((π a) Ω) = (π ((N.action (translationSub x)) a)) Ω) + (hpos : ∀ n ∈ minkowskiForwardCone 0, IsPositiveEnergy fun t => U (t • n)) (hwa : N.IsWeaklyAdditive) + (hcyc : GNS.IsCyclicVector π Ω) {B : Set StandardMinkowskiSpacetime.Carrier} (hB : IsAlexandrovBasisSet B) + (hne : B.Nonempty) : Dense ((fun T => T Ω) '' N.localOperators π hB) +``` + +The vacuum form +([crllr:reeh-schlieder-vacuum](https://physicslib.github.io/physicslib4/blueprint/chptr-haag-kastler-axioms-blueprint.html#crllr:reeh-schlieder-vacuum)) +indexes the unitaries by the whole Poincaré group, as a vacuum state does. Its hypotheses `hU` and +`hpos` are the implementation and spectrum conjuncts of +{apiDocs Physicslib4.AQFT.HaagKastler.HaagKastlerNet.IsVacuumStateConcrete}[`IsVacuumStateConcrete`], +with the spectrum condition quantified over future-timelike translation subgroups $`\gamma`: + +```lean (name := checkRSvac) +open Physicslib4 AQFT HaagKastler in +#check reeh_schlieder_cyclic_of_vacuum +``` + +```leanOutput checkRSvac +Physicslib4.AQFT.HaagKastler.reeh_schlieder_cyclic_of_vacuum.{u_1, u_2} {H : Type u_1} [NormedAddCommGroup H] + [InnerProductSpace ℂ H] [CompleteSpace H] {N : HaagKastlerNet} (hwa : N.IsWeaklyAdditive) + (π : N.quasilocal.carrier →⋆ₐ[ℂ] H →L[ℂ] H) (Ω : H) (U : InhomogeneousLorentzGroup → H ≃ₗᵢ[ℂ] H) + (hU : ∀ (L : InhomogeneousLorentzGroup) (a : N.quasilocal.carrier), (U L) ((π a) Ω) = (π ((N.action L) a)) Ω) + (hpos : + ∀ (γ : ℝ → InhomogeneousLorentzGroup), + IsOneParameterSubgroup γ → IsFutureTimelikeTranslation γ → IsPositiveEnergy fun t => U (γ t)) + (hcyc : GNS.IsCyclicVector π Ω) {B : Set StandardMinkowskiSpacetime.Carrier} (hB : IsAlexandrovBasisSet B) + (hne : B.Nonempty) : Dense ((fun T => T Ω) '' N.localOperators π hB) +``` + +## The separating form + +The separating form +([crllr:reeh-schlieder-separating](https://physicslib.github.io/physicslib4/blueprint/chptr-haag-kastler-axioms-blueprint.html#crllr:reeh-schlieder-separating)) +combines `reeh_schlieder_cyclic` with +{apiDocs Physicslib4.AQFT.HaagKastler.HaagKastlerNet.localVonNeumannAlgebra_separating}[`localVonNeumannAlgebra_separating`] +of the Minkowski chapter: a vector cyclic for $`\pi(\mathfrak{U}(\mathbf{B}))` is separating for +$`R(\mathbf{C})` when $`\mathbf{C}` is completely spacelike to $`\mathbf{B}`. The diamond +$`\mathbf{C}` may be empty; $`\mathbf{B}` may not. + +```lean (name := checkRSsep) +open Physicslib4 AQFT HaagKastler in +#check reeh_schlieder_separating +``` + +```leanOutput checkRSsep +Physicslib4.AQFT.HaagKastler.reeh_schlieder_separating.{u_1, u_2} {H : Type u_1} [NormedAddCommGroup H] + [InnerProductSpace ℂ H] [CompleteSpace H] {N : HaagKastlerNet} (π : N.quasilocal.carrier →⋆ₐ[ℂ] H →L[ℂ] H) (Ω : H) + (U : StandardMinkowskiSpacetime.Carrier → H ≃ₗᵢ[ℂ] H) + (hU : + ∀ (x : StandardMinkowskiSpacetime.Carrier) (a : N.quasilocal.carrier), + (U x) ((π a) Ω) = (π ((N.action (translationSub x)) a)) Ω) + (hpos : ∀ n ∈ minkowskiForwardCone 0, IsPositiveEnergy fun t => U (t • n)) + (hcyc : + ∀ ⦃B' : Set StandardMinkowskiSpacetime.Carrier⦄ (hB' : IsAlexandrovBasisSet B'), + B'.Nonempty → Dense (Set.range fun a => (π ↑a) Ω)) + {B C : Set StandardMinkowskiSpacetime.Carrier} (hB : IsAlexandrovBasisSet B) (hne : B.Nonempty) + (hC : IsAlexandrovBasisSet C) + (hs : StandardMinkowskiSpacetime.IsCompletelySpacelike standardMinkowskiTimeOrientation B C) {R : H →L[ℂ] H} + (hR : R ∈ N.localVonNeumannAlgebra π hC) (hRΩ : R Ω = 0) : R = 0 +``` + +## A tour of the proof + +The supporting lemmas fall into five groups, in the order the proof uses them. + +_Holomorphic extension under positive energy._ The spectrum condition enters through one lemma +([lmm:positive-energy-holomorphic](https://physicslib.github.io/physicslib4/blueprint/chptr-haag-kastler-axioms-blueprint.html#lmm:positive-energy-holomorphic)): +a matrix coefficient of a positive-energy group extends holomorphically to the upper half-plane, +bounded and continuous up to the real axis. + +```lean (name := checkHolo) +open Physicslib4 AQFT in +#check IsPositiveEnergy.exists_holomorphic_extension +``` + +```leanOutput checkHolo +Physicslib4.AQFT.IsPositiveEnergy.exists_holomorphic_extension.{u_1} {H : Type u_1} [NormedAddCommGroup H] + [InnerProductSpace ℂ H] [CompleteSpace H] {V : ℝ → H ≃ₗᵢ[ℂ] H} (hV : IsPositiveEnergy V) (χ φ : H) : + ∃ F, + DifferentiableOn ℂ F {z | 0 < z.im} ∧ + ContinuousOn F {z | 0 ≤ z.im} ∧ (∃ C, ∀ (z : ℂ), 0 ≤ z.im → ‖F z‖ ≤ C) ∧ ∀ (t : ℝ), F ↑t = inner ℂ χ ((V t) φ) +``` + +Its proof writes $`V(t) = e^{itA}` by Stone's theorem and goes through the spectral measure of +$`A`: it vanishes on $`(-\infty, 0)` +({apiDocs Physicslib4.AQFT.spectralMeasure_Iio_zero_eq_zero}[`spectralMeasure_Iio_zero_eq_zero`]); +polarization writes each matrix coefficient as a combination of Fourier transforms of finite +measures ({apiDocs Physicslib4.AQFT.exists_inner_expUnitary_eq_sum}[`exists_inner_expUnitary_eq_sum`]); +and the Fourier–Laplace transform $`z \mapsto \int e^{iz\lambda}\,d\nu(\lambda)` of a finite measure +carried by $`[0, \infty)` is bounded and continuous on the closed upper half-plane +({apiDocs Physicslib4.AQFT.fourierLaplace_bounded_continuousOn}[`fourierLaplace_bounded_continuousOn`]) +and holomorphic on the open one +({apiDocs Physicslib4.AQFT.differentiableOn_fourierLaplace}[`differentiableOn_fourierLaplace`]). + +_Vanishing on an edge._ The uniqueness step +([lmm:edge-vanishing](https://physicslib.github.io/physicslib4/blueprint/chptr-haag-kastler-axioms-blueprint.html#lmm:edge-vanishing)) +is pure complex analysis, with no operators: + +```lean (name := checkEdge) +#check Physicslib4.eq_zero_of_eq_zero_on_Ioo +``` + +```leanOutput checkEdge +Physicslib4.eq_zero_of_eq_zero_on_Ioo {f : ℂ → ℂ} {a b : ℝ} (hab : a < b) (hf : ContinuousOn f {z | 0 ≤ z.im}) + (hf' : DifferentiableOn ℂ f {z | 0 < z.im}) (hzero : ∀ x ∈ Set.Ioo a b, f ↑x = 0) (z : ℂ) : 0 ≤ z.im → f z = 0 +``` + +The proof reflects $`f` across the interval $`I`: the function equal to $`f(z)` for +$`\operatorname{Im} z \ge 0` and to $`\overline{f(\bar z)}` below is holomorphic on +$`\{\operatorname{Im} z \neq 0\} \cup I` +({apiDocs Physicslib4.differentiableOn_schwarzReflection_of_eq_zero}[`differentiableOn_schwarzReflection_of_eq_zero`], +via Morera's theorem across the real axis), a set that is open and connected +({apiDocs Physicslib4.isConnected_im_ne_zero_union_image_ofReal}[`isConnected_im_ne_zero_union_image_ofReal`]), +so the identity theorem applies. + +_Timelike spreading._ Combining the two: +{apiDocs Physicslib4.AQFT.HaagKastler.inner_translation_eq_zero_add_smul}[`inner_translation_eq_zero_add_smul`] +spreads the vanishing of $`x \mapsto \langle \chi, U(x)\varphi \rangle` from an open set $`W` to +$`W + \mathbb{R}n`, and +{apiDocs Physicslib4.AQFT.HaagKastler.inner_translation_eq_zero}[`inner_translation_eq_zero`] +iterates over the basis +{apiDocs Physicslib4.AQFT.HaagKastler.futureTimelike_basis}[`futureTimelike_basis`] to reach all of +$`\mathbb{R}^4` +([lmm:timelike-spreading](https://physicslib.github.io/physicslib4/blueprint/chptr-haag-kastler-axioms-blueprint.html#lmm:timelike-spreading)). +The group law is assumed only at the one vector $`\varphi`, hypothesis `hmul`, which is what the +cyclic subspace supplies. The geometric lemmas of the same file give the translate of a diamond +({apiDocs Physicslib4.AQFT.HaagKastler.translationSub_smul_diamond}[`translationSub_smul_diamond`]), +the smaller diamond with all small translates inside a given one +({apiDocs Physicslib4.AQFT.HaagKastler.exists_diamond_translate_subset}[`exists_diamond_translate_subset`]), +and small partial sums +({apiDocs Physicslib4.AQFT.HaagKastler.exists_isOpen_sum_mem_of_mem_nhds}[`exists_isOpen_sum_mem_of_mem_nhds`]). + +_The cyclic subspace._ On $`K_0`, the closure of $`\pi(\mathfrak{U})\Omega`, the unitaries fix +$`\Omega`, leave $`K_0` invariant together with every $`\pi(a)`, intertwine $`\pi` with $`\beta`, +and satisfy the group law; the conjunction is +{apiDocs Physicslib4.AQFT.HaagKastler.covariant_translations_cyclicSubspace}[`covariant_translations_cyclicSubspace`] +([lmm:covariant-translations-cyclic-subspace](https://physicslib.github.io/physicslib4/blueprint/chptr-haag-kastler-axioms-blueprint.html#lmm:covariant-translations-cyclic-subspace)). +Each part reduces, through +{apiDocs Physicslib4.AQFT.HaagKastler.apply_eq_of_mem_cyclicSubspace}[`apply_eq_of_mem_cyclicSubspace`], +to an identity on the vectors $`\pi(a)\Omega`. + +_The correlation-function induction._ For $`\psi` orthogonal to $`\pi(\mathfrak{U}(\mathbf{B}))\Omega` +and $`a_1, \dots, a_n` in the local algebra of $`\mathbf{B}_1`, consider + +$$`F(\xi_1, \dots, \xi_n) = \langle \psi, U(\xi_1)\pi(a_1)U(\xi_2)\pi(a_2) \cdots U(\xi_n)\pi(a_n)\Omega \rangle.` + +By {apiDocs Physicslib4.AQFT.HaagKastler.translated_products_apply}[`translated_products_apply`] +the vector is $`\pi(\beta_{x_1}a_1 \cdots \beta_{x_n}a_n)\Omega` with partial sums +$`x_k = \xi_1 + \dots + \xi_k`, so $`F` vanishes when all $`\xi_k` are small +({apiDocs Physicslib4.AQFT.HaagKastler.inner_translated_products_eq_zero_of_mem}[`inner_translated_products_eq_zero_of_mem`]). +As a function of one $`\xi_k` with the others fixed, $`F` is a matrix coefficient +$`\langle \chi, U(\xi_k)\varphi \rangle` with $`\varphi \in K_0` +({apiDocs Physicslib4.AQFT.HaagKastler.inner_translated_products_update_eq_inner}[`inner_translated_products_update_eq_inner`]), +so timelike spreading frees the variables one at a time, from $`\xi_1` to $`\xi_n`, and $`F` +vanishes identically +({apiDocs Physicslib4.AQFT.HaagKastler.inner_translated_products_eq_zero}[`inner_translated_products_eq_zero`], +[lmm:reeh-schlieder-correlations-vanish](https://physicslib.github.io/physicslib4/blueprint/chptr-haag-kastler-axioms-blueprint.html#lmm:reeh-schlieder-correlations-vanish)). +Changing variables back gives orthogonality to every monomial in translated local elements +({apiDocs Physicslib4.AQFT.HaagKastler.inner_monomial_eq_zero}[`inner_monomial_eq_zero`]), linearity +to the \*-algebra they generate +({apiDocs Physicslib4.AQFT.HaagKastler.inner_adjoin_translates_eq_zero}[`inner_adjoin_translates_eq_zero`]), +and continuity to its norm closure $`\mathfrak{A}_{\mathbf{B}_1}`, which is the main theorem. The +corollaries add the bicommutant step +{apiDocs Physicslib4.AQFT.HaagKastler.apply_mem_closure_translationGeneratedAlgebra}[`apply_mem_closure_translationGeneratedAlgebra`]. + +# Where to look +%%% +tag := "reeh-schlieder-files" +%%% + +The Reeh–Schlieder theorem is in `Physicslib4/AQFT/HaagKastler/ReehSchlieder/`, in four files +listed in dependency order, and rests on two files outside it. Each entry links to the API +documentation of a representative declaration. + +* `Translations.lean`: translates of diamonds, the future-timelike basis and timelike spreading, + {apiDocs Physicslib4.AQFT.HaagKastler.inner_translation_eq_zero}[`inner_translation_eq_zero`]. +* `CyclicSubspace.lean`: the unitaries on the cyclic subspace, + {apiDocs Physicslib4.AQFT.HaagKastler.covariant_translations_cyclicSubspace}[`covariant_translations_cyclicSubspace`]. +* `Correlations.lean`: the correlation functions and their vanishing, + {apiDocs Physicslib4.AQFT.HaagKastler.inner_translated_products_eq_zero}[`inner_translated_products_eq_zero`]. +* `Additivity.lean`: the translation-generated algebras, the forms of weak additivity, the theorem + and its corollaries, + {apiDocs Physicslib4.AQFT.HaagKastler.reeh_schlieder}[`reeh_schlieder`]. + +The analytic preliminaries: + +* `Physicslib4/AQFT/PositiveEnergyHolomorphic.lean`: the holomorphic extension under positive + energy, + {apiDocs Physicslib4.AQFT.IsPositiveEnergy.exists_holomorphic_extension}[`IsPositiveEnergy.exists_holomorphic_extension`]; + positive energy itself is in `Physicslib4/AQFT/PositiveEnergy.lean`. +* `Physicslib4/Analysis/EdgeVanishing.lean`: Schwarz reflection and vanishing on an edge, + {apiDocs Physicslib4.eq_zero_of_eq_zero_on_Ioo}[`eq_zero_of_eq_zero_on_Ioo`]. + +The separating step uses `Physicslib4/AQFT/HaagKastler/LocalVonNeumann.lean`, and the bicommutant +step for a single vector is in `Physicslib4/Operators/DensityTheorem.lean`, +{apiDocs Physicslib4.apply_mem_closure_of_mem_bicommutant}[`apply_mem_closure_of_mem_bicommutant`]. + +The blueprint section is +[Section 10.9](https://physicslib.github.io/physicslib4/blueprint/chptr-haag-kastler-axioms-blueprint.html#sctn:reeh-schlieder), +and each entry there links to the Lean declarations that formalise it. diff --git a/web/README.md b/web/README.md index 36e071d..fe1f838 100644 --- a/web/README.md +++ b/web/README.md @@ -60,6 +60,7 @@ examples on the page are elaborated against the library itself. Section 10.6). - `Manual/Curved.lean`: "The axioms in curved spacetime and general covariance" (blueprint Sections 10.7–10.8). +- `Manual/ReehSchlieder.lean`: "The Reeh–Schlieder theorem" (blueprint Section 10.9). - `Manual/Conventions.lean`: "Conventions and design decisions", the library's conventions and design decisions, each stated once with links to where it matters. - `Manual/NotProved.lean`: "Appendix: what the library does not prove", the standard facts the