diff --git a/Physicslib4.lean b/Physicslib4.lean index 879964b..90eb335 100644 --- a/Physicslib4.lean +++ b/Physicslib4.lean @@ -54,6 +54,7 @@ import Physicslib4.GNS.UnitaryRepresentation import Physicslib4.Operators.Conjugation import Physicslib4.Operators.LpDiagonal import Physicslib4.Spacetime.Basic +import Physicslib4.Spacetime.CausalComplement import Physicslib4.Spacetime.CausalStructure import Physicslib4.Spacetime.Causality import Physicslib4.Spacetime.Curves diff --git a/Physicslib4/AQFT/HaagKastler/LocalVonNeumann.lean b/Physicslib4/AQFT/HaagKastler/LocalVonNeumann.lean index 9728d29..9fa3111 100644 --- a/Physicslib4/AQFT/HaagKastler/LocalVonNeumann.lean +++ b/Physicslib4/AQFT/HaagKastler/LocalVonNeumann.lean @@ -5,6 +5,7 @@ Authors: Lean Community -/ import Physicslib4.AQFT.HaagKastler.EinsteinCausality import Physicslib4.GNS.Irreducibility +import Physicslib4.Spacetime.CausalComplement /-! # Local von Neumann algebras and spacelike commutation @@ -89,12 +90,12 @@ theorem eq_zero_of_commute_of_cyclic {S : Set (H →L[ℂ] H)} {Ω : H} have hzero : Set.EqOn (⇑R) (fun _ => (0 : H)) ((fun T => T Ω) '' S) := by rintro _ ⟨T, hT, rfl⟩ change R (T Ω) = 0 - rw [← ContinuousLinearMap.mul_apply, hcomm T hT, ContinuousLinearMap.mul_apply, hRΩ, + rw [← mul_apply_eq_comp, hcomm T hT, mul_apply_eq_comp, hRΩ, map_zero] have hRx : (⇑R) = fun _ => (0 : H) := Continuous.ext_on hcyc R.continuous continuous_const hzero exact ContinuousLinearMap.ext fun x => - (congrFun hRx x).trans (ContinuousLinearMap.zero_apply x).symm + (congrFun hRx x).trans (zero_apply x).symm /-- **Statistical independence (Schlieder property), Minkowski spacetime.** If `Ω` is cyclic for the local observables of `B₁` - in Minkowski spacetime this @@ -150,6 +151,21 @@ theorem localVonNeumannAlgebra_le_commutant simp only [coe_localVonNeumannAlgebra, VonNeumannAlgebra.coe_commutant] exact N.localVonNeumann_subset_centralizer π hB₁ hB₂ hs +/-- **Additive-free locality (Minkowski).** A bounded region lying in the spacelike +complement of `B` has its local algebra inside the commutant of `R(B)`: for basis +sets `B' ⊆ B^⊥`, `R(B') ≤ R(B)'`. This repackages microcausality through the +spacelike complement, keeping strictly to bounded (diamond) regions — no algebra is +attached to the unbounded complement. -/ +theorem localVonNeumannAlgebra_le_commutant_of_subset_spacelikeComplement + (π : N.commAlgebra.carrier →⋆ₐ[ℂ] (H →L[ℂ] H)) + ⦃B B' : Set StandardMinkowskiSpacetime.Carrier⦄ + (hB : IsAlexandrovBasisSet B) (hB' : IsAlexandrovBasisSet B') + (hsub : B' ⊆ Spacetime.spacelikeComplement StandardMinkowskiSpacetime + standardMinkowskiTimeOrientation B) : + N.localVonNeumannAlgebra π B' ≤ (N.localVonNeumannAlgebra π B).commutant := + N.localVonNeumannAlgebra_le_commutant π hB' hB + ((Spacetime.subset_spacelikeComplement_iff _ _).mp hsub) + /-- **Isotony, bundled (Minkowski).** `B₁ ⊆ B₂ ⟹ R(B₁) ≤ R(B₂)` as von Neumann algebras. -/ theorem localVonNeumannAlgebra_mono diff --git a/Physicslib4/AQFT/HaagKastler/Net.lean b/Physicslib4/AQFT/HaagKastler/Net.lean index 26f9158..272050f 100644 --- a/Physicslib4/AQFT/HaagKastler/Net.lean +++ b/Physicslib4/AQFT/HaagKastler/Net.lean @@ -269,7 +269,7 @@ the empty-region normalisation being the identity isomorphism. -/ noncomputable def trivialLocalNet : LocalNet where algebra := fun _ => ℂ instCStarAlgebra := fun _ => inferInstance - emptyEquivComplex := StarAlgEquiv.refl + emptyEquivComplex := StarAlgEquiv.refl ℂ ℂ /-- A concrete Alexandrov-basis set of standard Minkowski spacetime (`I⁺(0) ∩ I⁻(0)`), used as a witness that basis sets exist. -/ @@ -310,7 +310,7 @@ theorem trivialLocalNet_quasilocalCompleteness : theorem trivialLocalNet_lorentzCovariance : LorentzCovariance trivialLocalNet := by - refine ⟨fun _ _ => StarAlgEquiv.refl, fun _ _ _ _ _ => StarAlgHom.id ℂ ℂ, + refine ⟨fun _ _ => StarAlgEquiv.refl ℂ ℂ, fun _ _ _ _ _ => StarAlgHom.id ℂ ℂ, ?_, ?_, ?_, ?_⟩ · intro B₁ B₂ hB₁ hB₂ h a b hh; exact hh · intro _ _; rfl diff --git a/Physicslib4/AQFT/HaagKastler/QuasilocalAction.lean b/Physicslib4/AQFT/HaagKastler/QuasilocalAction.lean index 8fd1177..a376739 100644 --- a/Physicslib4/AQFT/HaagKastler/QuasilocalAction.lean +++ b/Physicslib4/AQFT/HaagKastler/QuasilocalAction.lean @@ -84,7 +84,6 @@ theorem QuasilocalLift.unique {Q : QuasilocalAlgebra N.U} intro x hx simp only [Set.mem_iUnion, Set.mem_range] at hx obtain ⟨B, hB, a, rfl⟩ := hx - change l₁.β (Q.ι B a) = l₂.β (Q.ι B a) rw [l₁.intertwines hB a, l₂.intertwines hB a] /-- The type of lifts of a fixed `L` is a subsingleton: a lift is determined by diff --git a/Physicslib4/AQFT/HaagKastler/QuasilocalIntertwiner.lean b/Physicslib4/AQFT/HaagKastler/QuasilocalIntertwiner.lean index fd04ee0..9b62e1b 100644 --- a/Physicslib4/AQFT/HaagKastler/QuasilocalIntertwiner.lean +++ b/Physicslib4/AQFT/HaagKastler/QuasilocalIntertwiner.lean @@ -402,8 +402,8 @@ inhabiting `QuasilocalLift`. -/ noncomputable def quasilocalLift (hcov : IsCovariant N Q) (L : InhomogeneousLorentzGroup) : N.QuasilocalLift Q L where β := StarAlgEquiv.ofStarAlgHom (extendHom hcov L) (extendHom hcov L⁻¹) - (fun x => DFunLike.congr_fun (extendHom_inv_comp hcov L) x) - (fun x => DFunLike.congr_fun (extendHom_comp_inv hcov L) x) + (extendHom_inv_comp hcov L) + (extendHom_comp_inv hcov L) intertwines := by intro B hB a rw [StarAlgEquiv.ofStarAlgHom_apply] @@ -476,7 +476,8 @@ theorem action_ι (C : CovariantQuasilocalAlgebra) (L : InhomogeneousLorentzGrou theorem action_apply (C : CovariantQuasilocalAlgebra) (L : InhomogeneousLorentzGroup) (x : C.quasilocal.carrier) : C.action L x = extendHom C.covariant L x := - StarAlgEquiv.ofStarAlgHom_apply _ _ _ _ x + StarAlgEquiv.ofStarAlgHom_apply (extendHom C.covariant L) (extendHom C.covariant L⁻¹) + (extendHom_inv_comp C.covariant L) (extendHom_comp_inv C.covariant L) x /-- **The action is trivial at the identity:** `β_1 = id`. -/ theorem action_one_apply (C : CovariantQuasilocalAlgebra) @@ -495,7 +496,7 @@ theorem action_mul_apply (C : CovariantQuasilocalAlgebra) /-- The covariance action sends the identity to the identity automorphism. -/ theorem action_one (C : CovariantQuasilocalAlgebra) : - C.action 1 = StarAlgEquiv.refl := by + C.action 1 = StarAlgEquiv.refl ℂ C.quasilocal.carrier := by ext x; rw [action_one_apply]; rfl /-- The covariance action is multiplicative: `β_{L'·L} = β_L` followed by diff --git a/Physicslib4/AQFT/HaagKastlerCurved/Concrete.lean b/Physicslib4/AQFT/HaagKastlerCurved/Concrete.lean index fc638a6..79fd6b8 100644 --- a/Physicslib4/AQFT/HaagKastlerCurved/Concrete.lean +++ b/Physicslib4/AQFT/HaagKastlerCurved/Concrete.lean @@ -5,8 +5,10 @@ Authors: Lean Community -/ import Physicslib4.AQFT.HaagKastlerCurved.Spacetime import Physicslib4.AQFT.HaagKastlerCurved.Net +import Physicslib4.AQFT.HaagKastlerCurved.LocalVonNeumann import Physicslib4.Spacetime.LorentzianSpacetime import Physicslib4.Spacetime.Isometry +import Physicslib4.Spacetime.CausalComplement /-! # Bridging a concrete spacetime to the abstract Haag-Kastler interface @@ -35,9 +37,16 @@ spacetime: * `Isom` is `Physicslib4.Spacetime.Isometry` of the underlying spacetime, with its `Group` and `MulAction` instances. -The same deferred refinements noted on `Spacetime.Isometry` apply here: -the isometry group is the full metric-preserving group (its -identity-component restriction is not yet captured) and its bundled +This bridge instantiates `Isom` with the *full* metric-preserving +isometry group. The identity-component restriction of Axiom 5 +("isometries connected to the identity") is captured by the sibling +bridge `toAbstractIdentityComponent` +(`Physicslib4/AQFT/HaagKastlerCurved/IdentityComponent.lean`), which uses +`Spacetime.Isometry.orientedIdentityComponent` (the topological +`connectedComponentOfOne` intersected with future-orientation +preservation); this full-group bridge is retained for the axioms that +hold under the whole isometry group (e.g. microcausality). One deferred +refinement noted on `Spacetime.Isometry` still applies: the bundled differential is not yet tied to the manifold derivative. -/ @@ -96,6 +105,26 @@ theorem commute_of_spacelike_mono_geometric (fun _ _ _ _ hh₁ hh₂ hh => L.isCompletelySpacelike_mono hh₁ hh₂ hh) hB₁' hB₂' hB hs hsub₁ hsub₂ h₁ h₂ a b +/-- **Additive-free locality over a concrete spacetime.** The geometric +specialisation of the curved additive-free locality: for a Haag-Kastler net over a +concrete Lorentzian spacetime `L`, a bounded region `B₁` lying in the spacelike +complement of `B₂` (both inside a common containing basis set `B`) has its local von +Neumann algebra inside the commutant of `R(B₂)`. The Galois bridge +`subset_spacelikeComplement_iff` discharges the spacelike hypothesis; no algebra is +attached to the unbounded complement. -/ +theorem localVonNeumannAlgebra_le_commutant_of_subset_spacelikeComplement_geometric + {L : Spacetime.LorentzianSpacetime} (N : HaagKastlerNet L.toAbstract) + {H : Type*} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] + {B : Set L.toAbstract.Carrier} (hB : L.toAbstract.IsBasisSet B) + (π : N.algebra B →⋆ₐ[ℂ] (H →L[ℂ] H)) + ⦃B₁ B₂ : Set L.toAbstract.Carrier⦄ + (hB₁ : L.toAbstract.IsBasisSet B₁) (hB₂ : L.toAbstract.IsBasisSet B₂) + (hsub : B₁ ⊆ L.spacelikeComplement B₂) (h₁ : B₁ ⊆ B) (h₂ : B₂ ⊆ B) : + N.localVonNeumannAlgebra π hB₁ hB h₁ + ≤ (N.localVonNeumannAlgebra π hB₂ hB h₂).commutant := + N.localVonNeumannAlgebra_le_commutant hB π hB₁ hB₂ + (L.subset_spacelikeComplement_iff.mp hsub) h₁ h₂ + end AQFT.HaagKastlerCurved.HaagKastlerNet end Physicslib4 diff --git a/Physicslib4/AQFT/HaagKastlerCurved/LocalVonNeumann.lean b/Physicslib4/AQFT/HaagKastlerCurved/LocalVonNeumann.lean index d51755e..6ef9a05 100644 --- a/Physicslib4/AQFT/HaagKastlerCurved/LocalVonNeumann.lean +++ b/Physicslib4/AQFT/HaagKastlerCurved/LocalVonNeumann.lean @@ -107,12 +107,12 @@ theorem eq_zero_of_commute_of_cyclic {S : Set (H →L[ℂ] H)} {Ω : H} have hzero : Set.EqOn (⇑R) (fun _ => (0 : H)) ((fun T => T Ω) '' S) := by rintro _ ⟨T, hT, rfl⟩ change R (T Ω) = 0 - rw [← ContinuousLinearMap.mul_apply, hcomm T hT, ContinuousLinearMap.mul_apply, hRΩ, + rw [← mul_apply_eq_comp, hcomm T hT, mul_apply_eq_comp, hRΩ, map_zero] have hRx : (⇑R) = fun _ => (0 : H) := Continuous.ext_on hcyc R.continuous continuous_const hzero exact ContinuousLinearMap.ext fun x => - (congrFun hRx x).trans (ContinuousLinearMap.zero_apply x).symm + (congrFun hRx x).trans (zero_apply x).symm /-- **Statistical independence (Schlieder property) for spacelike curved regions.** If `Ω` is cyclic for the local observables of `B₁` - the role supplied in diff --git a/Physicslib4/AQFT/HaagKastlerCurved/Net.lean b/Physicslib4/AQFT/HaagKastlerCurved/Net.lean index 26db700..87943ac 100644 --- a/Physicslib4/AQFT/HaagKastlerCurved/Net.lean +++ b/Physicslib4/AQFT/HaagKastlerCurved/Net.lean @@ -276,7 +276,7 @@ identity isomorphism. -/ noncomputable def trivialLocalNet (M : LorentzianSpacetime) : LocalNet M where algebra := fun _ => ℂ instCStarAlgebra := fun _ => inferInstance - emptyEquivComplex := StarAlgEquiv.refl + emptyEquivComplex := StarAlgEquiv.refl ℂ ℂ theorem trivialLocalNet_isotony (M : LorentzianSpacetime) : Isotony (trivialLocalNet M) := @@ -295,7 +295,7 @@ theorem trivialLocalNet_localAlgebra (M : LorentzianSpacetime) : theorem trivialLocalNet_isometricCovariance (M : LorentzianSpacetime) : IsometricCovariance (trivialLocalNet M) := by - refine ⟨fun _ _ => StarAlgEquiv.refl, fun _ _ _ _ _ => StarAlgHom.id ℂ ℂ, + refine ⟨fun _ _ => StarAlgEquiv.refl ℂ ℂ, fun _ _ _ _ _ => StarAlgHom.id ℂ ℂ, ?_, ?_, ?_, ?_⟩ · intro _ _ _ _ h _ _ hh; exact hh · intro _ _; rfl diff --git a/Physicslib4/AQFT/HaagKastlerCurved/StabilizerAction.lean b/Physicslib4/AQFT/HaagKastlerCurved/StabilizerAction.lean index 4cc9ea5..abb3c52 100644 --- a/Physicslib4/AQFT/HaagKastlerCurved/StabilizerAction.lean +++ b/Physicslib4/AQFT/HaagKastlerCurved/StabilizerAction.lean @@ -59,11 +59,11 @@ variable {M : LorentzianSpacetime} (N : HaagKastlerNet M) /-- Transport a local algebra along an equality of regions. -/ noncomputable def algCongr {B₁ B₂ : Set M.Carrier} (h : B₁ = B₂) : N.algebra B₁ ≃⋆ₐ[ℂ] N.algebra B₂ := by - subst h; exact StarAlgEquiv.refl + subst h; exact StarAlgEquiv.refl ℂ (N.algebra B₁) theorem algCongr_apply {B₁ B₂ : Set M.Carrier} (h : B₁ = B₂) (a : N.algebra B₁) : N.algCongr h a = cast (congrArg N.algebra h) a := by - subst h; rfl + subst h; simp [algCongr] /-- **Stabilizer automorphism.** For an isometry `φ` fixing the region `B` (`φ·B = B`), the covariance equivalence `covEquiv φ B` lands back in `𝔘(B)` and diff --git a/Physicslib4/Analysis/HorizontalLineRemovable.lean b/Physicslib4/Analysis/HorizontalLineRemovable.lean index c64c8f6..f0cd007 100644 --- a/Physicslib4/Analysis/HorizontalLineRemovable.lean +++ b/Physicslib4/Analysis/HorizontalLineRemovable.lean @@ -156,7 +156,7 @@ theorem rectIntegralReal_eq_zero_of_continuousOn_off_horizontal_line (f : ℂ intro z hz rw [Complex.mem_reProdIm] at hz obtain ⟨hre, him⟩ := hz - refine Set.mem_diff_of_mem (Complex.mem_reProdIm.mpr ⟨Set.Ioo_subset_Icc_self hre, ?_⟩) ?_ + refine Set.mem_sdiff_of_mem (Complex.mem_reProdIm.mpr ⟨Set.Ioo_subset_Icc_self hre, ?_⟩) ?_ · exact Set.mem_Icc.mpr ⟨him.1.le, him.2.le.trans hℓd⟩ · simp only [Set.mem_setOf_eq]; exact ne_of_lt him.2 -- The upper piece `[a,b] × [ℓ,d]`: holomorphic interior has `im > ℓ`. @@ -167,7 +167,7 @@ theorem rectIntegralReal_eq_zero_of_continuousOn_off_horizontal_line (f : ℂ intro z hz rw [Complex.mem_reProdIm] at hz obtain ⟨hre, him⟩ := hz - refine Set.mem_diff_of_mem (Complex.mem_reProdIm.mpr ⟨Set.Ioo_subset_Icc_self hre, ?_⟩) ?_ + refine Set.mem_sdiff_of_mem (Complex.mem_reProdIm.mpr ⟨Set.Ioo_subset_Icc_self hre, ?_⟩) ?_ · exact Set.mem_Icc.mpr ⟨hcℓ.trans him.1.le, him.2.le⟩ · simp only [Set.mem_setOf_eq]; exact (ne_of_lt him.1).symm rw [hlow, hupp, add_zero] @@ -225,7 +225,7 @@ theorem rectIntegralReal_eq_zero_of_subset {U : Set ℂ} (ℓ : ℝ) · -- `c ≤ ℓ ≤ d`: straddling vanishing refine rectIntegralReal_eq_zero_of_continuousOn_off_horizontal_line f a b c d ℓ hab hcℓ hℓd hcont (hd.mono (fun z hz => ?_)) - refine Set.mem_diff_of_mem (hsub ?_) hz.2 + refine Set.mem_sdiff_of_mem (hsub ?_) hz.2 rw [Complex.mem_reProdIm, Set.uIcc_of_le hab, Set.uIcc_of_le hcd] exact Complex.mem_reProdIm.mp hz.1 · -- `d < ℓ`: line above the rectangle, plain Cauchy-Goursat @@ -234,14 +234,14 @@ theorem rectIntegralReal_eq_zero_of_subset {U : Set ℂ} (ℓ : ℝ) rw [min_eq_left hab, max_eq_right hab, min_eq_left hcd, max_eq_right hcd] intro z hz rw [Complex.mem_reProdIm] at hz - exact Set.mem_diff_of_mem (hsub (hmem_open z hz.1 hz.2)) (ne_of_lt (hz.2.2.trans_le hdℓ)) + exact Set.mem_sdiff_of_mem (hsub (hmem_open z hz.1 hz.2)) (ne_of_lt (hz.2.2.trans_le hdℓ)) · -- `ℓ < c`: line below the rectangle, plain Cauchy-Goursat refine rectIntegralReal_eq_zero_of_continuousOn_of_differentiableOn f a b c d hcont (hd.mono ?_) rw [min_eq_left hab, max_eq_right hab, min_eq_left hcd, max_eq_right hcd] intro z hz rw [Complex.mem_reProdIm] at hz - exact Set.mem_diff_of_mem (hsub (hmem_open z hz.1 hz.2)) + exact Set.mem_sdiff_of_mem (hsub (hmem_open z hz.1 hz.2)) (ne_of_lt (lt_of_le_of_lt hℓc hz.2.1)).symm rcases le_total a b with hab | hab <;> rcases le_total c d with hcd | hcd · exact ordered a b c d hab hcd hsub @@ -316,7 +316,7 @@ theorem frontier_setOf_im_lt (c : ℝ) : = closure {z : ℂ | z.im < c} \ interior {z : ℂ | z.im < c} from rfl, closure_setOf_im_lt, (isOpen_setOf_im_lt c).interior_eq] ext z - simp only [Set.mem_diff, Set.mem_setOf_eq, not_lt] + simp only [Set.mem_sdiff, Set.mem_setOf_eq, not_lt] exact ⟨fun ⟨h1, h2⟩ => le_antisymm h1 h2, fun h => ⟨h.le, h.ge⟩⟩ /-- **Holomorphic gluing across a horizontal line (Schwarz-reflection form).** diff --git a/Physicslib4/GNS/Amplification.lean b/Physicslib4/GNS/Amplification.lean index 40606b4..26a8cc4 100644 --- a/Physicslib4/GNS/Amplification.lean +++ b/Physicslib4/GNS/Amplification.lean @@ -60,10 +60,10 @@ theorem not_isIrreducible_directSum {j k : ι} (hjk : j ≠ k) exact norm_ne_zero_iff.mpr hw have e1 := DFunLike.congr_fun hc (lp.single 2 j v) have e2 := DFunLike.congr_fun hc (lp.single 2 k w) - simp only [summandProj_apply, ContinuousLinearMap.smul_apply, ContinuousLinearMap.one_apply, + simp only [summandProj_apply, smul_apply, one_apply_eq_self, lp.single_apply_self] at e1 simp only [summandProj_apply, lp.single_apply_ne 2 k w hjk, lp.single_zero, - ContinuousLinearMap.smul_apply, ContinuousLinearMap.one_apply] at e2 + smul_apply, one_apply_eq_self] at e2 have hc1 : c = 1 := by have h0 : (1 - c) • lp.single 2 j v = 0 := by rw [sub_smul, one_smul, ← e1, sub_self] rcases smul_eq_zero.mp h0 with h | h diff --git a/Physicslib4/GNS/Basic.lean b/Physicslib4/GNS/Basic.lean index 467d381..e6293cd 100644 --- a/Physicslib4/GNS/Basic.lean +++ b/Physicslib4/GNS/Basic.lean @@ -66,7 +66,7 @@ variable {A} noncomputable instance : FunLike (State A) A ℂ where coe ω := ω.toContinuousLinearMap - coe_injective' := by + coe_injective := by intro ω₁ ω₂ h cases ω₁ cases ω₂ diff --git a/Physicslib4/GNS/Construction.lean b/Physicslib4/GNS/Construction.lean index 14ca896..8c432e5 100644 --- a/Physicslib4/GNS/Construction.lean +++ b/Physicslib4/GNS/Construction.lean @@ -195,12 +195,12 @@ theorem gns_unique {A : Type*} [CStarAlgebra A] (ω : State A) U Ω₁ = Ω₂ ∧ ∀ (a : A) (x : H₁), U (π₁ a x) = π₂ a (U x) := by let e₁ : A →ₗ[ℂ] H₁ := { toFun := fun a => π₁ a Ω₁ - map_add' := fun a b => by simp [map_add, ContinuousLinearMap.add_apply] - map_smul' := fun c a => by simp [map_smul, ContinuousLinearMap.smul_apply] } + map_add' := fun a b => by simp [map_add, add_apply] + map_smul' := fun c a => by simp [map_smul, smul_apply] } let e₂ : A →ₗ[ℂ] H₂ := { toFun := fun a => π₂ a Ω₂ - map_add' := fun a b => by simp [map_add, ContinuousLinearMap.add_apply] - map_smul' := fun c a => by simp [map_smul, ContinuousLinearMap.smul_apply] } + map_add' := fun a b => by simp [map_add, add_apply] + map_smul' := fun c a => by simp [map_smul, smul_apply] } have hdense₁ : DenseRange e₁ := hcyc₁ have hdense₂ : DenseRange e₂ := hcyc₂ have hinner_eq : ∀ a b : A, ⟪e₁ a, e₁ b⟫_ℂ = ⟪e₂ a, e₂ b⟫_ℂ := by @@ -209,11 +209,11 @@ theorem gns_unique {A : Type*} [CStarAlgebra A] (ω : State A) have h1 : ⟪π₁ a Ω₁, π₁ b Ω₁⟫_ℂ = ⟪Ω₁, π₁ (star a * b) Ω₁⟫_ℂ := by rw [← ContinuousLinearMap.adjoint_inner_right, ← ContinuousLinearMap.star_eq_adjoint, ← map_star] - rw [map_mul, ContinuousLinearMap.mul_apply] + rw [map_mul, mul_apply_eq_comp] have h2 : ⟪π₂ a Ω₂, π₂ b Ω₂⟫_ℂ = ⟪Ω₂, π₂ (star a * b) Ω₂⟫_ℂ := by rw [← ContinuousLinearMap.adjoint_inner_right, ← ContinuousLinearMap.star_eq_adjoint, ← map_star] - rw [map_mul, ContinuousLinearMap.mul_apply] + rw [map_mul, mul_apply_eq_comp] rw [h1, h2, ← hrep₁, ← hrep₂] have hnorm : ∀ a : A, ‖e₂ a‖ = ‖e₁ a‖ := by intro a diff --git a/Physicslib4/GNS/DirectSum.lean b/Physicslib4/GNS/DirectSum.lean index 259f4d8..13da254 100644 --- a/Physicslib4/GNS/DirectSum.lean +++ b/Physicslib4/GNS/DirectSum.lean @@ -64,7 +64,7 @@ noncomputable def directSum : A →⋆ₐ[ℂ] (lp H 2 →L[ℂ] lp H 2) where toFun := directSumFun π map_one' := by refine lpDiag_ext fun x i => ?_; simp [map_one] map_mul' a b := by - refine lpDiag_ext fun x i => ?_; simp [map_mul, ContinuousLinearMap.mul_apply] + refine lpDiag_ext fun x i => ?_; simp [map_mul, mul_apply_eq_comp] map_zero' := by refine lpDiag_ext fun x i => ?_ change π i 0 (x i) = (0 : lp H 2) i @@ -75,8 +75,8 @@ noncomputable def directSum : A →⋆ₐ[ℂ] (lp H 2 →L[ℂ] lp H 2) where rw [map_add (π i) a b]; rfl commutes' r := by refine lpDiag_ext fun x i => ?_ - simp [Algebra.algebraMap_eq_smul_one, ContinuousLinearMap.smul_apply, - ContinuousLinearMap.one_apply, lp.coeFn_smul] + simp [Algebra.algebraMap_eq_smul_one, smul_apply, + one_apply_eq_self, lp.coeFn_smul] map_star' a := by simp only [directSumFun] rw [lpDiag_star] @@ -118,7 +118,7 @@ theorem summandProj_mem_commutant (j : ι) : rw [Set.mem_centralizer_iff] rintro _ ⟨a, rfl⟩ refine lpDiag_ext fun x i => ?_ - simp only [ContinuousLinearMap.mul_apply, directSum_apply, directSumFun_apply_coe, + simp only [mul_apply_eq_comp, directSum_apply, directSumFun_apply_coe, summandProj_apply, lp.single_apply] rcases eq_or_ne i j with h | h · subst h; simp diff --git a/Physicslib4/GNS/ExtremeState.lean b/Physicslib4/GNS/ExtremeState.lean index d7f1bf4..9ec036d 100644 --- a/Physicslib4/GNS/ExtremeState.lean +++ b/Physicslib4/GNS/ExtremeState.lean @@ -58,7 +58,7 @@ private lemma nontrivial_of_state (ω : State A) : Nontrivial A := by · exfalso have h0 : ω.toContinuousLinearMap = 0 := by ext a - rw [Subsingleton.elim a 0, map_zero, ContinuousLinearMap.zero_apply] + rw [Subsingleton.elim a 0, map_zero, zero_apply] have hnorm := ω.isNormalized rw [h0, norm_zero] at hnorm exact one_ne_zero hnorm.symm @@ -155,7 +155,7 @@ theorem isExtremePoint_of_isPure (ω : State A) (hpure : IsPure ω) : have hψapp : ∀ a, ψ a = (t : ℂ) * ω₁ a := by intro a; rw [hψ_def] show ((t : ℂ) • ω₁.toContinuousLinearMap) a = (t : ℂ) * ω₁ a - rw [ContinuousLinearMap.smul_apply]; rfl + rw [smul_apply]; rfl have htne : (t : ℂ) ≠ 0 := by rw [Ne, Complex.ofReal_eq_zero]; exact ht0.ne' have h1tne : (1 - (t : ℂ)) ≠ 0 := by have he : (1 - (t : ℂ)) = ((1 - t : ℝ) : ℂ) := by push_cast; ring @@ -229,9 +229,9 @@ theorem isPure_of_isExtremePoint (ω : State A) (hext : ω.IsExtremePoint) : · -- `λ = 1` : `ψ = ω` refine ⟨1, fun a => ?_⟩ have hpossub : ∀ c, 0 ≤ (ω.toContinuousLinearMap - ψ) (star c * c) := by - intro c; rw [ContinuousLinearMap.sub_apply]; exact sub_nonneg.mpr (hψdom c) + intro c; rw [sub_apply]; exact sub_nonneg.mpr (hψdom c) have hval : ((ω.toContinuousLinearMap - ψ) 1).re = 0 := by - rw [ContinuousLinearMap.sub_apply, Complex.sub_re] + rw [sub_apply, Complex.sub_re] change (ω 1).re - (ψ 1).re = 0 rw [hω1, Complex.one_re, ← hlam_def, hlam1]; ring have hnormsub := norm_eq_re_apply_one_of_positive hpossub @@ -249,20 +249,20 @@ theorem isPure_of_isExtremePoint (ω : State A) (hext : ω.IsExtremePoint) : rw [Ne, Complex.ofReal_eq_zero]; exact h1lampos.ne' -- the two rescaled states have hpos1 : ∀ a, 0 ≤ (((lam : ℂ))⁻¹ • ψ) (star a * a) := by - intro a; rw [ContinuousLinearMap.smul_apply] + intro a; rw [smul_apply] exact mul_nonneg (complex_inv_ofReal_nonneg hlampos.le) (hψpos a) have hnorm1 : ‖((lam : ℂ))⁻¹ • ψ‖ = 1 := by rw [norm_smul, norm_inv_ofReal_pos hlampos, hψnorm, inv_mul_cancel₀ hlampos.ne'] have hpossub : ∀ c, 0 ≤ (ω.toContinuousLinearMap - ψ) (star c * c) := by - intro c; rw [ContinuousLinearMap.sub_apply]; exact sub_nonneg.mpr (hψdom c) + intro c; rw [sub_apply]; exact sub_nonneg.mpr (hψdom c) have hnormsub : ‖ω.toContinuousLinearMap - ψ‖ = 1 - lam := by - rw [norm_eq_re_apply_one_of_positive hpossub, ContinuousLinearMap.sub_apply, + rw [norm_eq_re_apply_one_of_positive hpossub, sub_apply, Complex.sub_re] change (ω 1).re - (ψ 1).re = 1 - lam rw [hω1, Complex.one_re, ← hlam_def] have hpos2 : ∀ a, 0 ≤ ((((1 - lam : ℝ) : ℂ))⁻¹ • (ω.toContinuousLinearMap - ψ)) (star a * a) := by - intro a; rw [ContinuousLinearMap.smul_apply] + intro a; rw [smul_apply] exact mul_nonneg (complex_inv_ofReal_nonneg h1lampos.le) (hpossub a) have hnorm2 : ‖(((1 - lam : ℝ) : ℂ))⁻¹ • (ω.toContinuousLinearMap - ψ)‖ = 1 := by rw [norm_smul, norm_inv_ofReal_pos h1lampos, hnormsub, inv_mul_cancel₀ h1lampos.ne'] @@ -273,12 +273,12 @@ theorem isPure_of_isExtremePoint (ω : State A) (hext : ω.IsExtremePoint) : have hs1a : ∀ a, s1 a = ((lam : ℂ))⁻¹ * ψ a := by intro a; rw [hs1] change (((lam : ℂ))⁻¹ • ψ) a = ((lam : ℂ))⁻¹ * ψ a - rw [ContinuousLinearMap.smul_apply]; rfl + rw [smul_apply]; rfl have hs2a : ∀ a, s2 a = (((1 - lam : ℝ) : ℂ))⁻¹ * (ω a - ψ a) := by intro a; rw [hs2] change ((((1 - lam : ℝ) : ℂ))⁻¹ • (ω.toContinuousLinearMap - ψ)) a = (((1 - lam : ℝ) : ℂ))⁻¹ * (ω a - ψ a) - rw [ContinuousLinearMap.smul_apply, ContinuousLinearMap.sub_apply]; rfl + rw [smul_apply, sub_apply]; rfl have hcancel : (lam : ℂ) * ((lam : ℂ))⁻¹ = 1 := mul_inv_cancel₀ hlamne have hcancel2 : (1 - (lam : ℂ)) * (((1 - lam : ℝ) : ℂ))⁻¹ = 1 := by rw [show (1 - (lam : ℂ)) = (((1 - lam : ℝ) : ℂ)) from by push_cast; ring] @@ -376,7 +376,7 @@ noncomputable def State.convexCombo (ω₁ ω₂ : State A) (s : ℝ) (hs0 : 0 toContinuousLinearMap := (s : ℂ) • ω₁.toContinuousLinearMap + ((1 - s : ℝ) : ℂ) • ω₂.toContinuousLinearMap isPositive := fun a => by - simp only [ContinuousLinearMap.add_apply, ContinuousLinearMap.smul_apply, smul_eq_mul] + simp only [add_apply, smul_apply, smul_eq_mul] exact add_nonneg (mul_nonneg (complex_ofReal_nonneg hs0) (ω₁.isPositive a)) (mul_nonneg (complex_ofReal_nonneg (by linarith)) (ω₂.isPositive a)) isNormalized := by @@ -384,11 +384,11 @@ noncomputable def State.convexCombo (ω₁ ω₂ : State A) (s : ℝ) (hs0 : 0 have hpos : ∀ a, 0 ≤ ((s : ℂ) • ω₁.toContinuousLinearMap + ((1 - s : ℝ) : ℂ) • ω₂.toContinuousLinearMap) (star a * a) := by intro a - simp only [ContinuousLinearMap.add_apply, ContinuousLinearMap.smul_apply, smul_eq_mul] + simp only [add_apply, smul_apply, smul_eq_mul] exact add_nonneg (mul_nonneg (complex_ofReal_nonneg hs0) (ω₁.isPositive a)) (mul_nonneg (complex_ofReal_nonneg (by linarith)) (ω₂.isPositive a)) rw [norm_eq_re_apply_one_of_positive hpos] - simp only [ContinuousLinearMap.add_apply, ContinuousLinearMap.smul_apply, smul_eq_mul] + simp only [add_apply, smul_apply, smul_eq_mul] rw [show ω₁.toContinuousLinearMap 1 = ω₁ 1 from rfl, show ω₂.toContinuousLinearMap 1 = ω₂ 1 from rfl, ω₁.apply_one, ω₂.apply_one] rw [show (s : ℂ) * 1 + ((1 - s : ℝ) : ℂ) * 1 = 1 from by push_cast; ring, Complex.one_re] @@ -398,7 +398,7 @@ noncomputable def State.convexCombo (ω₁ ω₂ : State A) (s : ℝ) (hs0 : 0 (ω₁.convexCombo ω₂ s hs0 hs1) a = (s : ℂ) * ω₁ a + ((1 - s : ℝ) : ℂ) * ω₂ a := by change ((s : ℂ) • ω₁.toContinuousLinearMap + ((1 - s : ℝ) : ℂ) • ω₂.toContinuousLinearMap) a = (s : ℂ) * ω₁ a + ((1 - s : ℝ) : ℂ) * ω₂ a - simp only [ContinuousLinearMap.add_apply, ContinuousLinearMap.smul_apply, smul_eq_mul] + simp only [add_apply, smul_apply, smul_eq_mul] rfl /-- **Purity is invariant under a `*`-automorphism**: `ω ∘ Φ` is pure iff `ω` is. @@ -434,7 +434,7 @@ theorem convex_stateSpace : Convex ℝ (stateSpace A) := by refine ⟨ω₁.convexCombo ω₂ a ha (by linarith), ?_⟩ have hb' : b = 1 - a := by linarith refine ContinuousLinearMap.ext fun c => ?_ - simp only [ContinuousLinearMap.add_apply, ContinuousLinearMap.smul_apply, + simp only [add_apply, smul_apply, Complex.real_smul, State.coe_toContinuousLinearMap, State.convexCombo_apply, hb'] /-- **Bridge to Mathlib's convex-geometry API.** A state `ω`, viewed in the @@ -450,7 +450,7 @@ theorem mem_extremePoints_iff_isExtremePoint (ω : State A) : refine ⟨t, 1 - t, ht0, by linarith, by ring, ?_⟩ refine ContinuousLinearMap.ext fun c => ?_ have hc := hdec c - simp only [ContinuousLinearMap.add_apply, ContinuousLinearMap.smul_apply, + simp only [add_apply, smul_apply, Complex.real_smul, State.coe_toContinuousLinearMap] rw [hc] push_cast @@ -464,7 +464,7 @@ theorem mem_extremePoints_iff_isExtremePoint (ω : State A) : have hdec : ∀ c, (ω c : ℂ) = (a : ℂ) * ω₁ c + (1 - a : ℂ) * ω₂ c := by intro c have hc := congrArg (fun φ : A →L[ℂ] ℂ => φ c) heq - simp only [ContinuousLinearMap.add_apply, ContinuousLinearMap.smul_apply, + simp only [add_apply, smul_apply, Complex.real_smul, State.coe_toContinuousLinearMap] at hc rw [← hc] have hb' : b = 1 - a := by linarith @@ -474,8 +474,8 @@ theorem mem_extremePoints_iff_isExtremePoint (ω : State A) : have hcombo : ω₁.toContinuousLinearMap = ω.toContinuousLinearMap := by rw [← heq] refine ContinuousLinearMap.ext fun c => ?_ - rw [ContinuousLinearMap.add_apply, ContinuousLinearMap.smul_apply, - ContinuousLinearMap.smul_apply, Complex.real_smul, Complex.real_smul, + rw [add_apply, smul_apply, + smul_apply, Complex.real_smul, Complex.real_smul, ← add_mul, ← Complex.ofReal_add, hab, Complex.ofReal_one, one_mul] exact ⟨hcombo, hcombo⟩ diff --git a/Physicslib4/GNS/Irreducibility.lean b/Physicslib4/GNS/Irreducibility.lean index 0708744..a97798c 100644 --- a/Physicslib4/GNS/Irreducibility.lean +++ b/Physicslib4/GNS/Irreducibility.lean @@ -72,16 +72,16 @@ theorem eq_smul_one_of_commute_of_cyclic congr 1 have h1 : (π (star b)) (T (π a Ω)) = T ((π (star b)) (π a Ω)) := calc (π (star b)) (T (π a Ω)) - = (π (star b) * T) (π a Ω) := by rw [ContinuousLinearMap.mul_apply] + = (π (star b) * T) (π a Ω) := by rw [mul_apply_eq_comp] _ = (T * π (star b)) (π a Ω) := by rw [hT (star b)] - _ = T ((π (star b)) (π a Ω)) := by rw [ContinuousLinearMap.mul_apply] + _ = T ((π (star b)) (π a Ω)) := by rw [mul_apply_eq_comp] rw [h1] congr 1 - rw [← ContinuousLinearMap.mul_apply, ← map_mul] + rw [← mul_apply_eq_comp, ← map_mul] have e2 : ⟪(π b) Ω, π a Ω⟫_ℂ = ⟪Ω, π (star b * a) Ω⟫_ℂ := by rw [hadj b (π a Ω)] congr 1 - rw [← ContinuousLinearMap.mul_apply, ← map_mul] + rw [← mul_apply_eq_comp, ← map_mul] rw [e1, e2, hprop (star b * a)] ring have hw0 : T (π a Ω) - c • (π a Ω) = 0 := by @@ -101,7 +101,7 @@ theorem eq_smul_one_of_commute_of_cyclic (by rintro _ ⟨a, rfl⟩; exact hkey a) apply ContinuousLinearMap.ext intro x - rw [ContinuousLinearMap.smul_apply, ContinuousLinearMap.one_apply] + rw [smul_apply, one_apply_eq_self] exact congrFun hall x /-- **A commutant operator is a scalar iff its GNS coefficient is proportional to @@ -118,7 +118,7 @@ theorem isScalar_iff_coeff_proportional constructor · rintro ⟨c, rfl⟩ refine ⟨c, fun a => ?_⟩ - rw [ContinuousLinearMap.smul_apply, ContinuousLinearMap.one_apply, inner_smul_right, + rw [smul_apply, one_apply_eq_self, inner_smul_right, ← hrep a] · rintro ⟨t, ht⟩ refine ⟨t, ?_⟩ @@ -142,9 +142,9 @@ noncomputable def coeffFunctional (π : A →⋆ₐ[ℂ] (H →L[ℂ] H)) (Ω : LinearMap.mkContinuous { toFun := fun a => ⟪Ω, T (π a Ω)⟫_ℂ map_add' := fun a b => by - simp [map_add, ContinuousLinearMap.add_apply, inner_add_right] + simp [map_add, add_apply, inner_add_right] map_smul' := fun c a => by - simp [map_smul, ContinuousLinearMap.smul_apply, inner_smul_right] } + simp [map_smul, smul_apply, inner_smul_right] } (‖Ω‖ * ‖T‖ * ‖Ω‖) (fun a => by have hT' : ‖T (π a Ω)‖ ≤ ‖T‖ * (‖a‖ * ‖Ω‖) := @@ -167,10 +167,10 @@ theorem coeffFunctional_star_mul {π : A →⋆ₐ[ℂ] (H →L[ℂ] H)} {Ω : H coeffFunctional π Ω T (star a * a) = ⟪π a Ω, T (π a Ω)⟫_ℂ := by rw [coeffFunctional_apply] have hsplit : π (star a * a) Ω = π (star a) (π a Ω) := by - rw [map_mul, ContinuousLinearMap.mul_apply] + rw [map_mul, mul_apply_eq_comp] rw [hsplit] have hcomm : T (π (star a) (π a Ω)) = π (star a) (T (π a Ω)) := by - rw [← ContinuousLinearMap.mul_apply, ← hT (star a), ContinuousLinearMap.mul_apply] + rw [← mul_apply_eq_comp, ← hT (star a), mul_apply_eq_comp] rw [hcomm] have hadjeq : ContinuousLinearMap.adjoint (π a) = π (star a) := by rw [← ContinuousLinearMap.star_eq_adjoint, map_star] @@ -221,7 +221,7 @@ theorem scalar_of_isSelfAdjoint_of_isPure Complex.re ⟪T v, v⟫_ℂ = r * Complex.re ⟪S v, v⟫_ℂ + 2⁻¹ * ‖v‖ ^ 2 := by intro v have hTv : T v = (r : ℂ) • S v + (2⁻¹ : ℂ) • v := by - simp [hT_def, ContinuousLinearMap.add_apply, ContinuousLinearMap.smul_apply] + simp [hT_def, add_apply, smul_apply] rw [hTv, inner_add_left, inner_smul_left, inner_smul_left, Complex.add_re, Complex.conj_ofReal, Complex.re_ofReal_mul] have h2 : (starRingEnd ℂ) (2⁻¹ : ℂ) = (2⁻¹ : ℂ) := by @@ -253,7 +253,7 @@ theorem scalar_of_isSelfAdjoint_of_isPure rw [ContinuousLinearMap.reApplyInnerSelf_apply] change (0 : ℝ) ≤ Complex.re ⟪(1 - T) v, v⟫_ℂ have hsub : ((1 : H →L[ℂ] H) - T) v = v - T v := by - simp [ContinuousLinearMap.sub_apply] + simp [sub_apply] have hvv : Complex.re ⟪v, v⟫_ℂ = ‖v‖ ^ 2 := by simpa using inner_self_eq_norm_sq (𝕜 := ℂ) v rw [hsub, inner_sub_left, Complex.sub_re, hTexp v, hvv] @@ -274,7 +274,7 @@ theorem scalar_of_isSelfAdjoint_of_isPure intro a rw [coeffFunctional_star_mul hTcomm a, hrep (star a * a)] have hsplit : π (star a * a) Ω = π (star a) (π a Ω) := by - rw [map_mul, ContinuousLinearMap.mul_apply] + rw [map_mul, mul_apply_eq_comp] have hadjeq : ContinuousLinearMap.adjoint (π a) = π (star a) := by rw [← ContinuousLinearMap.star_eq_adjoint, map_star] have hω : ⟪Ω, π (star a * a) Ω⟫_ℂ = ⟪π a Ω, π a Ω⟫_ℂ := by @@ -282,7 +282,7 @@ theorem scalar_of_isSelfAdjoint_of_isPure rw [hω] have hpd := isPositive_inner_nonneg hTle (π a Ω) have hsub : ((1 : H →L[ℂ] H) - T) (π a Ω) = π a Ω - T (π a Ω) := by - simp [ContinuousLinearMap.sub_apply] + simp [sub_apply] rw [hsub, inner_sub_right] at hpd exact sub_nonneg.mp hpd -- purity forces `T` to be a scalar diff --git a/Physicslib4/GNS/RadonNikodym.lean b/Physicslib4/GNS/RadonNikodym.lean index a983175..6029816 100644 --- a/Physicslib4/GNS/RadonNikodym.lean +++ b/Physicslib4/GNS/RadonNikodym.lean @@ -42,7 +42,7 @@ theorem reproducing_norm_sq {ω : State A} {π : A →⋆ₐ[ℂ] (H →L[ℂ] H (ω (star x * x)).re = ‖π x Ω‖ ^ 2 := by have heq : (ω (star x * x) : ℂ) = ⟪π x Ω, π x Ω⟫_ℂ := by have hsplit : π (star x * x) Ω = π (star x) (π x Ω) := by - rw [map_mul, ContinuousLinearMap.mul_apply] + rw [map_mul, mul_apply_eq_comp] have hadjeq : ContinuousLinearMap.adjoint (π x) = π (star x) := by rw [← ContinuousLinearMap.star_eq_adjoint, map_star] rw [hrep, hsplit, ← hadjeq, ContinuousLinearMap.adjoint_inner_right] @@ -93,7 +93,7 @@ theorem gns_form_well_defined {ω : State A} {π : A →⋆ₐ[ℂ] (H →L[ℂ] (hψdom : ∀ a : A, ψ (star a * a) ≤ ω (star a * a)) {a a' : A} (haa : π a Ω = π a' Ω) (b : A) : ψ (star a * b) = ψ (star a' * b) := by - have hzero : π (a - a') Ω = 0 := by rw [map_sub, ContinuousLinearMap.sub_apply, haa, sub_self] + have hzero : π (a - a') Ω = 0 := by rw [map_sub, sub_apply, haa, sub_self] have hb := gns_form_norm_le hrep hψpos hψdom (a - a') b rw [hzero, norm_zero, zero_mul] at hb have hψz : ψ (star (a - a') * b) = 0 := norm_le_zero_iff.mp hb @@ -109,8 +109,8 @@ open InnerProductSpace /-- The cyclic map `a ↦ π a Ω` as a `ℂ`-linear map `A →ₗ[ℂ] H`. -/ noncomputable def cycLM (π : A →⋆ₐ[ℂ] (H →L[ℂ] H)) (Ω : H) : A →ₗ[ℂ] H where toFun a := π a Ω - map_add' x y := by simp [map_add, ContinuousLinearMap.add_apply] - map_smul' c x := by simp [map_smul, ContinuousLinearMap.smul_apply] + map_add' x y := by simp [map_add, add_apply] + map_smul' c x := by simp [map_smul, smul_apply] @[simp] theorem cycLM_apply (π : A →⋆ₐ[ℂ] (H →L[ℂ] H)) (Ω : H) (a : A) : cycLM π Ω a = π a Ω := rfl @@ -233,11 +233,11 @@ theorem rnOp_commute {ω : State A} {π : A →⋆ₐ[ℂ] (H →L[ℂ] H)} {Ω refine eq_of_dense_inner_right (cycLM_denseRange hcyc) (fun a => ?_) simp only [cycLM_apply] have hRHS : T ((π c) (π b Ω)) = T (π (c * b) Ω) := by - congr 1; rw [← ContinuousLinearMap.mul_apply, ← map_mul] + congr 1; rw [← mul_apply_eq_comp, ← map_mul] rw [hRHS, rnOp_inner hcyc hrep hψpos hψdom a (c * b), ← ContinuousLinearMap.adjoint_inner_left, hadjeq, show (π (star c)) (π a Ω) = π (star c * a) Ω from by - rw [← ContinuousLinearMap.mul_apply, ← map_mul], + rw [← mul_apply_eq_comp, ← map_mul], rnOp_inner hcyc hrep hψpos hψdom (star c * a) b] congr 1 rw [star_mul, star_star, mul_assoc] @@ -248,7 +248,7 @@ theorem rnOp_commute {ω : State A} {π : A →⋆ₐ[ℂ] (H →L[ℂ] H)} {Ω simpa using key b apply ContinuousLinearMap.ext intro y - rw [ContinuousLinearMap.mul_apply, ContinuousLinearMap.mul_apply] + rw [mul_apply_eq_comp, mul_apply_eq_comp] exact congrFun hfun y /-- **The reproducing identity for the state.** `ψ(a) = ⟪Ω, T (π a Ω)⟫`. -/ @@ -258,7 +258,7 @@ theorem rnOp_reproducing {ω : State A} {π : A →⋆ₐ[ℂ] (H →L[ℂ] H)} (hψdom : ∀ a : A, ψ (star a * a) ≤ ω (star a * a)) (a : A) : (ψ a : ℂ) = ⟪Ω, rnOp hcyc hrep hψpos hψdom (π a Ω)⟫_ℂ := by have h := rnOp_inner hcyc hrep hψpos hψdom 1 a - rw [map_one, ContinuousLinearMap.one_apply, star_one, one_mul] at h + rw [map_one, one_apply_eq_self, star_one, one_mul] at h exact h.symm /-- **Irreducible ⟹ pure.** If the GNS representation of `ω` is irreducible, then @@ -273,7 +273,7 @@ theorem isPure_of_isIrreducible {ω : State A} {π : A →⋆ₐ[ℂ] (H →L[ (fun a => rnOp_commute hcyc hrep hψpos hψdom a) refine ⟨c, fun a => ?_⟩ rw [rnOp_reproducing hcyc hrep hψpos hψdom a, hc, - ContinuousLinearMap.smul_apply, ContinuousLinearMap.one_apply, inner_smul_right, ← hrep a] + smul_apply, one_apply_eq_self, inner_smul_right, ← hrep a] /-- **The full GNS purity ⟺ irreducibility equivalence.** A state `ω` is pure if and only if its cyclic GNS representation is irreducible. -/ diff --git a/Physicslib4/GNS/Separating.lean b/Physicslib4/GNS/Separating.lean index 408d3af..ec459f2 100644 --- a/Physicslib4/GNS/Separating.lean +++ b/Physicslib4/GNS/Separating.lean @@ -43,7 +43,7 @@ theorem separating_of_faithful {ω : State A} (hω : ω.IsFaithful) have hpos : 0 < ω (star a * a) := hω a hne have hzero : ω (star a * a) = 0 := by rw [hrep (star a * a), map_mul, map_star] - simp [ContinuousLinearMap.mul_apply, ha] + simp [mul_apply_eq_comp, ha] rw [hzero] at hpos exact lt_irrefl 0 hpos diff --git a/Physicslib4/GNS/Superselection.lean b/Physicslib4/GNS/Superselection.lean index 22e3b63..5d9ae61 100644 --- a/Physicslib4/GNS/Superselection.lean +++ b/Physicslib4/GNS/Superselection.lean @@ -49,11 +49,11 @@ theorem intertwines_zero : Intertwines π₁ π₂ (0 : H₁ →L[ℂ] H₂) := theorem Intertwines.add {S T : H₁ →L[ℂ] H₂} (hS : Intertwines π₁ π₂ S) (hT : Intertwines π₁ π₂ T) : Intertwines π₁ π₂ (S + T) := fun a x => by - simp only [ContinuousLinearMap.add_apply, hS a x, hT a x, map_add] + simp only [add_apply, hS a x, hT a x, map_add] theorem Intertwines.smul {T : H₁ →L[ℂ] H₂} (c : ℂ) (hT : Intertwines π₁ π₂ T) : Intertwines π₁ π₂ (c • T) := fun a x => by - simp only [ContinuousLinearMap.smul_apply, hT a x, map_smul] + simp only [smul_apply, hT a x, map_smul] /-- The composition of intertwiners is an intertwiner. -/ theorem Intertwines.comp {S : H₂ →L[ℂ] H₃} {T : H₁ →L[ℂ] H₂} @@ -122,7 +122,7 @@ theorem UnitaryEquiv.not_areDisjoint [Nontrivial H₁] (h : UnitaryEquiv π₁ have := ContinuousLinearMap.ext_iff.mp h0 v simpa only [ContinuousLinearEquiv.coe_coe, LinearIsometryEquiv.coe_toContinuousLinearEquiv, - ContinuousLinearMap.zero_apply] using this + zero_apply] using this exact hv (U.injective (hUv.trans (map_zero U).symm)) /-! ### Schur's lemma and the irreducible dichotomy -/ @@ -277,7 +277,7 @@ theorem eq_smul_of_intertwines_of_isIrreducible = (S.comp (ContinuousLinearMap.adjoint S)) v := by rw [ContinuousLinearMap.comp_apply, ContinuousLinearMap.comp_apply, huv] rw [hc] at happ - simp only [ContinuousLinearMap.smul_apply, ContinuousLinearMap.one_apply] at happ + simp only [smul_apply, one_apply_eq_self] at happ have hcuv : c • (u - v) = 0 := by rw [smul_sub, happ, sub_self] rcases smul_eq_zero.mp hcuv with h | h · exact absurd h hc0 @@ -291,7 +291,7 @@ theorem eq_smul_of_intertwines_of_isIrreducible have hSx : (ContinuousLinearMap.adjoint S) (S x) = a • x := by have := DFunLike.congr_fun ha x simpa using this - rw [ContinuousLinearMap.sub_apply, ContinuousLinearMap.smul_apply, map_sub, map_smul, + rw [sub_apply, smul_apply, map_sub, map_smul, hTx, hSx, smul_smul, div_mul_cancel₀ b ha0, sub_self] have hzero : T - (b / a) • S = 0 := by ext x @@ -309,9 +309,9 @@ theorem intertwines_self_iff_mem_centralizer {π : A →⋆ₐ[ℂ] (H₁ →L[ constructor · rintro h _ ⟨a, rfl⟩ ext x - simpa only [ContinuousLinearMap.mul_apply] using (h a x).symm + simpa only [mul_apply_eq_comp] using (h a x).symm · intro h a x - simpa only [ContinuousLinearMap.mul_apply] using + simpa only [mul_apply_eq_comp] using (DFunLike.congr_fun (h (π a) ⟨a, rfl⟩) x).symm /-- **The endomorphism algebra of an irreducible representation is `ℂ · 1`.** Every @@ -323,6 +323,79 @@ theorem intertwines_self_iff_isScalar {π : A →⋆ₐ[ℂ] (H₁ →L[ℂ] H rw [intertwines_self_iff_mem_centralizer, isIrreducible_iff_centralizer.mp h] exact Iff.rfl +/-! ### The commutant (self-intertwiner) von Neumann algebra -/ + +/-- **The commutant `π(A)'` as a von Neumann algebra**: the algebra of +self-intertwiners of `π` — its "gauge"/intertwiner algebra. The centralizer of +`π(A)` is self-adjoint, and a commutant is always a von Neumann algebra +(`S''' = S'`). -/ +noncomputable def commutantVonNeumann (π : A →⋆ₐ[ℂ] (H₁ →L[ℂ] H₁)) : + VonNeumannAlgebra H₁ := + vonNeumannOfSelfAdjoint (Set.centralizer (Set.range π)) + (fun _ hx => star_mem_setCentralizer (range_selfAdjoint π) hx) + +@[simp] theorem coe_commutantVonNeumann (π : A →⋆ₐ[ℂ] (H₁ →L[ℂ] H₁)) : + (commutantVonNeumann π : Set (H₁ →L[ℂ] H₁)) = Set.centralizer (Set.range π) := by + unfold commutantVonNeumann + rw [coe_vonNeumannOfSelfAdjoint, Set.centralizer_centralizer_centralizer] + +/-- Membership in the commutant von Neumann algebra is exactly being a +self-intertwiner of `π`. -/ +theorem mem_commutantVonNeumann_iff_intertwines + {π : A →⋆ₐ[ℂ] (H₁ →L[ℂ] H₁)} {T : H₁ →L[ℂ] H₁} : + T ∈ commutantVonNeumann π ↔ Intertwines π π T := by + rw [intertwines_self_iff_mem_centralizer, ← coe_commutantVonNeumann, SetLike.mem_coe] + +/-- **A representation is irreducible iff its commutant von Neumann algebra is +trivial**, `π(A)' = ℂ · 1`. This is the von Neumann form of Schur's lemma: the +gauge/intertwiner algebra collapses to the scalars exactly for irreducibles. -/ +theorem isIrreducible_iff_commutantVonNeumann_eq_scalars + {π : A →⋆ₐ[ℂ] (H₁ →L[ℂ] H₁)} : + IsIrreducible π ↔ + (commutantVonNeumann π : Set (H₁ →L[ℂ] H₁)) = scalarOperators H₁ := by + rw [coe_commutantVonNeumann] + exact isIrreducible_iff_centralizer + +/-! ### Double-commutant duality -/ + +/-- **Double-commutant duality (I).** The commutant of the generated von Neumann +algebra `π(A)''` is the commutant von Neumann algebra `π(A)'`. This is the +triple-commutant collapse `S''' = S'` applied to the self-adjoint image `π(A)`. -/ +theorem commutant_gnsVonNeumannAlgebra (π : A →⋆ₐ[ℂ] (H₁ →L[ℂ] H₁)) : + (gnsVonNeumannAlgebra π).commutant = commutantVonNeumann π := + SetLike.coe_injective (by + simp [gnsVonNeumann]) + +/-- **Double-commutant duality (II).** The commutant of the commutant von Neumann +algebra `π(A)'` is the generated von Neumann algebra `π(A)''` — this is exactly the +definition of the bicommutant. So `π(A)''` and `π(A)'` are each other's commutants. -/ +theorem commutant_commutantVonNeumann (π : A →⋆ₐ[ℂ] (H₁ →L[ℂ] H₁)) : + (commutantVonNeumann π).commutant = gnsVonNeumannAlgebra π := + SetLike.coe_injective (by + simp [gnsVonNeumann]) + +/-- **A factor and its commutant.** A von Neumann algebra and its commutant share the +same center (their intersection is symmetric), so the generated algebra `π(A)''` is a +factor if and only if its commutant `π(A)'` is a factor. -/ +theorem isFactor_gnsVonNeumann_iff_isFactor_commutant (π : A →⋆ₐ[ℂ] (H₁ →L[ℂ] H₁)) : + IsFactor (gnsVonNeumann π) ↔ + IsFactor (commutantVonNeumann π : Set (H₁ →L[ℂ] H₁)) := by + unfold IsFactor + simp only [coe_commutantVonNeumann] + unfold gnsVonNeumann + simp only [Set.centralizer_centralizer_centralizer] + constructor <;> intro h <;> rw [Set.inter_comm] at h <;> exact h + +/-- **Triviality duality.** The commutant collapses to the scalars `π(A)' = ℂ · 1` if +and only if the generated algebra is everything `π(A)'' = B(H)`. This is the commutant +form of the equivalence "irreducible ⟺ generates `B(H)`". -/ +theorem commutantVonNeumann_eq_scalars_iff_gnsVonNeumann_eq_univ + (π : A →⋆ₐ[ℂ] (H₁ →L[ℂ] H₁)) : + (commutantVonNeumann π : Set (H₁ →L[ℂ] H₁)) = scalarOperators H₁ ↔ + gnsVonNeumann π = Set.univ := by + rw [← isIrreducible_iff_commutantVonNeumann_eq_scalars] + exact isIrreducible_iff_gnsVonNeumann_eq_univ + /-! ### The pure-state dichotomy -/ /-- **The pure-state dichotomy.** The GNS representations of two pure states are @@ -356,7 +429,7 @@ omit [CompleteSpace H₁] [CompleteSpace H₂] in theorem conjCLM_mul (U : H₁ ≃ₗᵢ[ℂ] H₂) (S T : H₁ →L[ℂ] H₁) : conjCLM U (S * T) = conjCLM U S * conjCLM U T := by ext x - simp only [conjCLM_apply, ContinuousLinearMap.mul_apply, + simp only [conjCLM_apply, mul_apply_eq_comp, LinearIsometryEquiv.symm_apply_apply] omit [CompleteSpace H₁] [CompleteSpace H₂] in @@ -444,7 +517,7 @@ def QuasiEquiv (π₁ : A →⋆ₐ[ℂ] (H₁ →L[ℂ] H₁)) (π₂ : A → /-- Quasi-equivalence is reflexive. -/ theorem QuasiEquiv.refl (π : A →⋆ₐ[ℂ] (H₁ →L[ℂ] H₁)) : QuasiEquiv π π := - ⟨StarAlgEquiv.refl, fun _ => rfl⟩ + ⟨StarAlgEquiv.refl ℂ (gnsVonNeumannAlgebra π).toStarSubalgebra, fun _ => rfl⟩ /-- Quasi-equivalence is symmetric. -/ theorem QuasiEquiv.symm (h : QuasiEquiv π₁ π₂) : QuasiEquiv π₂ π₁ := by diff --git a/Physicslib4/GNS/UnitaryEquiv.lean b/Physicslib4/GNS/UnitaryEquiv.lean index 6647b11..7376936 100644 --- a/Physicslib4/GNS/UnitaryEquiv.lean +++ b/Physicslib4/GNS/UnitaryEquiv.lean @@ -84,7 +84,7 @@ noncomputable def conjMulEquiv (U : H₁ ≃ₗᵢ[ℂ] H₂) : left_inv T := by ext x; simp right_inv S := by ext x; simp map_mul' S T := by - ext x; simp [ContinuousLinearMap.mul_apply] + ext x; simp [mul_apply_eq_comp] omit [CompleteSpace H₁] [CompleteSpace H₂] in @[simp] theorem conjMulEquiv_apply (U : H₁ ≃ₗᵢ[ℂ] H₂) (T : H₁ →L[ℂ] H₁) : diff --git a/Physicslib4/GNS/UnitaryRepresentation.lean b/Physicslib4/GNS/UnitaryRepresentation.lean index 376851a..8fec234 100644 --- a/Physicslib4/GNS/UnitaryRepresentation.lean +++ b/Physicslib4/GNS/UnitaryRepresentation.lean @@ -64,9 +64,9 @@ theorem gns_operator_covariance {A : Type*} [CStarAlgebra A] {G : Type*} rintro _ ⟨b, rfl⟩ change U g (π a (π b Ω)) = π (γ g a) (U g (π b Ω)) have e1 : (π a) (π b Ω) = π (a * b) Ω := by - rw [← ContinuousLinearMap.mul_apply, ← map_mul] + rw [← mul_apply_eq_comp, ← map_mul] have e2 : (π (γ g a)) (π (γ g b) Ω) = π (γ g a * γ g b) Ω := by - rw [← ContinuousLinearMap.mul_apply, ← map_mul] + rw [← mul_apply_eq_comp, ← map_mul] rw [e1, himpl g (a * b), map_mul (γ g), himpl g b, e2] rw [show U g (π a ((U g).symm x)) = π (γ g a) (U g ((U g).symm x)) from congrFun hint ((U g).symm x), (U g).apply_symm_apply] @@ -98,12 +98,12 @@ theorem exists_gns_unitary_of_invariant.{u} {A : Type u} [CStarAlgebra A] obtain ⟨H, _, _, _, π, Ω, hcyc, hrepro, _⟩ := gns_construction ω let cyc : A →ₗ[ℂ] H := { toFun := fun a => π a Ω - map_add' := fun a b => by rw [map_add, ContinuousLinearMap.add_apply] - map_smul' := fun c a => by rw [map_smul, ContinuousLinearMap.smul_apply]; rfl } + map_add' := fun a b => by rw [map_add, add_apply] + map_smul' := fun c a => by rw [map_smul, smul_apply]; rfl } have hcycdense : DenseRange (cyc : A → H) := hcyc have q : ∀ x, (ω (star x * x) : ℂ) = ⟪π x Ω, π x Ω⟫_ℂ := by intro x - rw [hrepro (star x * x), map_mul, map_star, ContinuousLinearMap.mul_apply, + rw [hrepro (star x * x), map_mul, map_star, mul_apply_eq_comp, ContinuousLinearMap.star_eq_adjoint, ContinuousLinearMap.adjoint_inner_right] have hinner : ∀ (g : G) (a b : A), ω (star (γ g a) * γ g b) = ω (star a * b) := by intro g a b @@ -131,12 +131,12 @@ theorem exists_gns_unitary_of_invariant.{u} {A : Type u} [CStarAlgebra A] · intro g have hΩ : cyc (1 : A) = Ω := by change π 1 Ω = Ω - rw [map_one, ContinuousLinearMap.one_apply] + rw [map_one, one_apply_eq_self] have hone' : cyc ((γ g).toAlgEquiv.toLinearEquiv (1 : A)) = Ω := by change π (γ g 1) Ω = Ω rw [map_one (γ g)] change π 1 Ω = Ω - rw [map_one, ContinuousLinearMap.one_apply] + rw [map_one, one_apply_eq_self] calc U g Ω = U g (cyc 1) := by rw [hΩ] _ = cyc ((γ g).toAlgEquiv.toLinearEquiv 1) := (γ g).toAlgEquiv.toLinearEquiv.extendOfIsometry_eq cyc cyc hcycdense hcycdense @@ -225,12 +225,12 @@ theorem exists_gns_unitary_of_invariant_strongContinuous.{u} {A : Type u} obtain ⟨H, _, _, _, π, Ω, hcyc, hrepro, _⟩ := gns_construction ω let cyc : A →ₗ[ℂ] H := { toFun := fun a => π a Ω - map_add' := fun a b => by rw [map_add, ContinuousLinearMap.add_apply] - map_smul' := fun c a => by rw [map_smul, ContinuousLinearMap.smul_apply]; rfl } + map_add' := fun a b => by rw [map_add, add_apply] + map_smul' := fun c a => by rw [map_smul, smul_apply]; rfl } have hcycdense : DenseRange (cyc : A → H) := hcyc have qq : ∀ a c : A, (ω (star a * c) : ℂ) = ⟪π a Ω, π c Ω⟫_ℂ := by intro a c - rw [hrepro (star a * c), map_mul, map_star, ContinuousLinearMap.mul_apply, + rw [hrepro (star a * c), map_mul, map_star, mul_apply_eq_comp, ContinuousLinearMap.star_eq_adjoint, ContinuousLinearMap.adjoint_inner_right] have hinner : ∀ (g : G) (a b : A), ω (star (γ g a) * γ g b) = ω (star a * b) := by intro g a b @@ -259,12 +259,12 @@ theorem exists_gns_unitary_of_invariant_strongContinuous.{u} {A : Type u} · intro g have hΩ : cyc (1 : A) = Ω := by change π 1 Ω = Ω - rw [map_one, ContinuousLinearMap.one_apply] + rw [map_one, one_apply_eq_self] have hone' : cyc ((γ g).toAlgEquiv.toLinearEquiv (1 : A)) = Ω := by change π (γ g 1) Ω = Ω rw [map_one (γ g)] change π 1 Ω = Ω - rw [map_one, ContinuousLinearMap.one_apply] + rw [map_one, one_apply_eq_self] calc U g Ω = U g (cyc 1) := by rw [hΩ] _ = cyc ((γ g).toAlgEquiv.toLinearEquiv 1) := (γ g).toAlgEquiv.toLinearEquiv.extendOfIsometry_eq cyc cyc hcycdense hcycdense diff --git a/Physicslib4/Operators/Conjugation.lean b/Physicslib4/Operators/Conjugation.lean index 9ea7050..fa31b94 100644 --- a/Physicslib4/Operators/Conjugation.lean +++ b/Physicslib4/Operators/Conjugation.lean @@ -102,7 +102,7 @@ omit [CompleteSpace H] in lieConj Uop T x = Uop (T (Uop.symm x)) := by change ((Uop.toContinuousLinearEquiv : H →L[ℂ] H) * T * (Uop.toContinuousLinearEquiv.symm : H →L[ℂ] H)) x = Uop (T (Uop.symm x)) - simp only [ContinuousLinearMap.mul_apply, ContinuousLinearEquiv.coe_coe, + simp only [mul_apply_eq_comp, ContinuousLinearEquiv.coe_coe, LinearIsometryEquiv.coe_toContinuousLinearEquiv] rfl diff --git a/Physicslib4/Operators/LpDiagonal.lean b/Physicslib4/Operators/LpDiagonal.lean index af2420d..3388536 100644 --- a/Physicslib4/Operators/LpDiagonal.lean +++ b/Physicslib4/Operators/LpDiagonal.lean @@ -107,7 +107,7 @@ theorem lpDiag_add (S T : ∀ i, E i →L[𝕜] E i) {KS KT KST : ℝ} lpDiag (fun i => S i + T i) hKST hSTK = lpDiag S hKS hSK + lpDiag T hKT hTK := by refine lpDiag_ext fun x i => ?_ change (S i + T i) (x i) = S i (x i) + T i (x i) - exact ContinuousLinearMap.add_apply (S i) (T i) (x i) + exact add_apply (S i) (T i) (x i) /-- The diagonal operator is `𝕜`-linear in the family. -/ theorem lpDiag_smul (c : 𝕜) (T : ∀ i, E i →L[𝕜] E i) {K KcT : ℝ} diff --git a/Physicslib4/Spacetime/CausalComplement.lean b/Physicslib4/Spacetime/CausalComplement.lean new file mode 100644 index 0000000..3162826 --- /dev/null +++ b/Physicslib4/Spacetime/CausalComplement.lean @@ -0,0 +1,423 @@ +/- +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.Spacetime.LorentzianSpacetime +import Mathlib.Order.Closure + +/-! +# The causal (spacelike) complement of a region + +The **spacelike complement** `B^⊥` of a region `B` in a Lorentzian spacetime is the +set of points completely spacelike-separated from all of `B`: +`B^⊥ = { x | {x} is completely spacelike to B }`. + +This is the geometric substrate of locality and Haag duality in algebraic quantum +field theory. We record its order structure: + +* `spacelikeComplement_antitone` — `B₁ ⊆ B₂ ⇒ B₂^⊥ ⊆ B₁^⊥`; +* `subset_spacelikeComplement_spacelikeComplement` — `B ⊆ B^⊥⊥`; +* `spacelikeComplement_spacelikeComplement_spacelikeComplement` — `B^⊥⊥⊥ = B^⊥`; +* `subset_spacelikeComplement_iff` — the Galois-type bridge + `B₁ ⊆ B₂^⊥ ↔ B₁, B₂ completely spacelike`. +-/ + +namespace Physicslib4 +namespace Spacetime + +section SpacetimeLevel +variable (M : Spacetime) (t : M.TimeOrientation) + +/-- The **spacelike complement** `B^⊥` of a region `B`, with respect to a time +orientation `t`: the points completely spacelike-separated from all of `B`. -/ +def spacelikeComplement (B : Set M.Carrier) : Set M.Carrier := + {x | Spacetime.IsCompletelySpacelike M t {x} B} + +@[simp] theorem mem_spacelikeComplement {B : Set M.Carrier} {x : M.Carrier} : + x ∈ Spacetime.spacelikeComplement M t B ↔ Spacetime.IsCompletelySpacelike M t {x} B := + Iff.rfl + +/-- **Galois bridge.** A region lies in the complement of another exactly when the +two are completely spacelike-separated. -/ +theorem subset_spacelikeComplement_iff {B₁ B₂ : Set M.Carrier} : + B₁ ⊆ Spacetime.spacelikeComplement M t B₂ ↔ Spacetime.IsCompletelySpacelike M t B₁ B₂ := by + constructor + · intro h p hp q hq + exact (h hp) p rfl q hq + · intro h x hx + rw [mem_spacelikeComplement] + intro p hp q hq + rw [Set.mem_singleton_iff] at hp + subst hp + exact h p hx q hq + +end SpacetimeLevel + +namespace LorentzianSpacetime + +variable (M : LorentzianSpacetime) + +/-- The **spacelike complement** `B^⊥` of a region `B`: the points completely +spacelike-separated from all of `B`. -/ +def spacelikeComplement (B : Set M.Carrier) : Set M.Carrier := + {x | M.IsCompletelySpacelike {x} B} + +@[simp] theorem mem_spacelikeComplement {B : Set M.Carrier} {x : M.Carrier} : + x ∈ M.spacelikeComplement B ↔ M.IsCompletelySpacelike {x} B := + Iff.rfl + +/-- Complete spacelike separation of a singleton from a region is pointwise. -/ +theorem isCompletelySpacelike_singleton_left_iff {x : M.Carrier} {O : Set M.Carrier} : + M.IsCompletelySpacelike {x} O ↔ ∀ y ∈ O, M.IsCompletelySpacelike {x} {y} := by + refine ⟨fun h y hy => + M.isCompletelySpacelike_mono (subset_refl _) (Set.singleton_subset_iff.mpr hy) h, fun h => ?_⟩ + intro p hp q hq + exact h q hq p hp q rfl + +/-- The spacelike complement is **antitone**: enlarging a region shrinks its +complement. -/ +theorem spacelikeComplement_antitone {B₁ B₂ : Set M.Carrier} (h : B₁ ⊆ B₂) : + M.spacelikeComplement B₂ ⊆ M.spacelikeComplement B₁ := by + intro x hx + rw [mem_spacelikeComplement] at hx ⊢ + exact M.isCompletelySpacelike_mono (subset_refl _) h hx + +/-- A region is contained in its **double complement**: `B ⊆ B^⊥⊥`. -/ +theorem subset_spacelikeComplement_spacelikeComplement (B : Set M.Carrier) : + B ⊆ M.spacelikeComplement (M.spacelikeComplement B) := by + intro y hy + rw [mem_spacelikeComplement, isCompletelySpacelike_singleton_left_iff] + intro x hx + rw [mem_spacelikeComplement] at hx + rw [M.isCompletelySpacelike_comm] + exact M.isCompletelySpacelike_mono (subset_refl _) (Set.singleton_subset_iff.mpr hy) hx + +/-- The **triple complement equals the complement**: `B^⊥⊥⊥ = B^⊥`. -/ +theorem spacelikeComplement_spacelikeComplement_spacelikeComplement (B : Set M.Carrier) : + M.spacelikeComplement (M.spacelikeComplement (M.spacelikeComplement B)) + = M.spacelikeComplement B := + Set.Subset.antisymm + (M.spacelikeComplement_antitone (M.subset_spacelikeComplement_spacelikeComplement B)) + (M.subset_spacelikeComplement_spacelikeComplement (M.spacelikeComplement B)) + +/-- The complement of the empty region is everything. -/ +@[simp] theorem spacelikeComplement_empty : + M.spacelikeComplement (∅ : Set M.Carrier) = Set.univ := by + ext x + simp + +/-- **Galois bridge.** A region lies in the complement of another exactly when the +two are completely spacelike-separated. -/ +theorem subset_spacelikeComplement_iff {B₁ B₂ : Set M.Carrier} : + B₁ ⊆ M.spacelikeComplement B₂ ↔ M.IsCompletelySpacelike B₁ B₂ := by + constructor + · intro h p hp q hq + exact (h hp) p rfl q hq + · intro h x hx + rw [mem_spacelikeComplement] + intro p hp q hq + rw [Set.mem_singleton_iff] at hp + subst hp + exact h p hx q hq + +/-! ### Causally complete regions and the causal closure operator + +The double complement `B ↦ B^⊥⊥` is a **closure operator** on the regions of a +Lorentzian spacetime. Its fixed points — the **causally complete** regions — are +the natural regions of algebraic QFT, and they form a complete lattice on which +the spacelike complement `^⊥` acts as an order-reversing involution. + +A caveat on orthocomplementation: the spacelike-separation relation used here is +*irreflexive-causality* based (a point is spacelike to itself, since there is no +degenerate closed causal trip), so `B ∩ B^⊥` need not be empty and the full +orthocomplement law `B ⊓ B^⊥ = ⊥` does **not** hold at this generality. What does +hold is the complete lattice with an order-reversing involution (a De Morgan +structure). -/ + +/-- The **causal closure operator** `B ↦ B^⊥⊥` on the regions of `M`: monotone, +extensive (`B ⊆ B^⊥⊥`), and idempotent (`B^⊥⊥⊥⊥ = B^⊥⊥`). -/ +noncomputable def causalClosure : ClosureOperator (Set M.Carrier) := + ClosureOperator.mk' + (fun B => M.spacelikeComplement (M.spacelikeComplement B)) + (fun _ _ h => M.spacelikeComplement_antitone (M.spacelikeComplement_antitone h)) + (fun B => M.subset_spacelikeComplement_spacelikeComplement B) + (fun B => (M.spacelikeComplement_spacelikeComplement_spacelikeComplement + (M.spacelikeComplement B)).le) + +@[simp] theorem causalClosure_apply (B : Set M.Carrier) : + M.causalClosure B = M.spacelikeComplement (M.spacelikeComplement B) := rfl + +/-- A region is **causally complete** if it equals its own double complement, +`B^⊥⊥ = B` (equivalently, it is a closed element of `causalClosure`). -/ +def IsCausallyComplete (B : Set M.Carrier) : Prop := + M.spacelikeComplement (M.spacelikeComplement B) = B + +theorem isCausallyComplete_iff_isClosed {B : Set M.Carrier} : + M.IsCausallyComplete B ↔ M.causalClosure.IsClosed B := by + rw [ClosureOperator.isClosed_iff] + rfl + +/-- The **spacelike complement of any region is causally complete**: `B^⊥⊥⊥ = B^⊥`. -/ +theorem isCausallyComplete_spacelikeComplement (B : Set M.Carrier) : + M.IsCausallyComplete (M.spacelikeComplement B) := + M.spacelikeComplement_spacelikeComplement_spacelikeComplement B + +/-- The causal closure `B^⊥⊥` of any region is causally complete. -/ +theorem isCausallyComplete_causalClosure (B : Set M.Carrier) : + M.IsCausallyComplete (M.causalClosure B) := + M.isCausallyComplete_spacelikeComplement (M.spacelikeComplement B) + +/-- On causally complete regions the spacelike complement is an **involution**: +`B^⊥⊥ = B`. -/ +theorem spacelikeComplement_spacelikeComplement_of_isCausallyComplete + {B : Set M.Carrier} (h : M.IsCausallyComplete B) : + M.spacelikeComplement (M.spacelikeComplement B) = B := h + +/-- **The causally complete regions are closed under intersection** (the lattice +meet): `B₁^⊥⊥ = B₁` and `B₂^⊥⊥ = B₂` imply `(B₁ ∩ B₂)^⊥⊥ = B₁ ∩ B₂`. -/ +theorem isCausallyComplete_inter {B₁ B₂ : Set M.Carrier} + (h₁ : M.IsCausallyComplete B₁) (h₂ : M.IsCausallyComplete B₂) : + M.IsCausallyComplete (B₁ ∩ B₂) := by + have key : ∀ {A C : Set M.Carrier}, A ⊆ C → M.IsCausallyComplete C → + M.spacelikeComplement (M.spacelikeComplement A) ⊆ C := by + intro A C hAC hC + calc M.spacelikeComplement (M.spacelikeComplement A) + ⊆ M.spacelikeComplement (M.spacelikeComplement C) := + M.spacelikeComplement_antitone (M.spacelikeComplement_antitone hAC) + _ = C := hC + exact Set.Subset.antisymm + (Set.subset_inter (key Set.inter_subset_left h₁) (key Set.inter_subset_right h₂)) + (M.subset_spacelikeComplement_spacelikeComplement _) + +/-- Arbitrary intersections of causally complete sets are causally complete. -/ +theorem isCausallyComplete_iInter {ι : Sort*} (B : ι → Set M.Carrier) + (h : ∀ i, M.IsCausallyComplete (B i)) : M.IsCausallyComplete (⋂ i, B i) := by + apply Set.Subset.antisymm + · intro x hx + rw [Set.mem_iInter] + intro i + have hxi : x ∈ M.spacelikeComplement (M.spacelikeComplement (⋂ i, B i)) := hx + have h_sub : ⋂ i, B i ⊆ B i := Set.iInter_subset B i + have h_comp : M.spacelikeComplement (B i) ⊆ M.spacelikeComplement (⋂ i, B i) := + M.spacelikeComplement_antitone h_sub + have h_double_comp : M.spacelikeComplement (M.spacelikeComplement (⋂ i, B i)) + ⊆ M.spacelikeComplement (M.spacelikeComplement (B i)) := + M.spacelikeComplement_antitone h_comp + have hxBi : x ∈ M.spacelikeComplement (M.spacelikeComplement (B i)) := h_double_comp hxi + rw [h i] at hxBi + exact hxBi + · exact M.subset_spacelikeComplement_spacelikeComplement (⋂ i, B i) + +/-- The **causally complete regions**, i.e. the closed elements of the causal +closure operator (`B^⊥⊥ = B`). Ordered by inclusion. -/ +abbrev CausallyCompleteRegion : Type _ := M.causalClosure.Closeds + +/-- The causally complete regions form a **complete lattice** (meets are +intersections; joins are causal closures of unions), transported from the causal +closure operator via its Galois insertion. -/ +noncomputable instance : CompleteLattice M.CausallyCompleteRegion := + M.causalClosure.gi.liftCompleteLattice + +/-- The spacelike complement as an **order-reversing involution** on the complete +lattice of causally complete regions (the causal complement). -/ +def causalComplement (B : M.CausallyCompleteRegion) : M.CausallyCompleteRegion := + ⟨M.spacelikeComplement B.1, + M.isCausallyComplete_iff_isClosed.mp (M.isCausallyComplete_spacelikeComplement B.1)⟩ + +@[simp] theorem causalComplement_coe (B : M.CausallyCompleteRegion) : + (M.causalComplement B).1 = M.spacelikeComplement B.1 := rfl + +/-- Causal complementation is an **involution**: `B^⊥⊥ = B` on causally complete +regions. -/ +theorem causalComplement_causalComplement (B : M.CausallyCompleteRegion) : + M.causalComplement (M.causalComplement B) = B := by + apply Subtype.ext + exact M.isCausallyComplete_iff_isClosed.mpr B.2 + +/-! ### De Morgan laws for the spacelike complement -/ + +/-- **Binary De Morgan (set level).** The spacelike complement turns a union into +an intersection: `(B₁ ∪ B₂)^⊥ = B₁^⊥ ∩ B₂^⊥`. -/ +theorem spacelikeComplement_union (B₁ B₂ : Set M.Carrier) : + M.spacelikeComplement (B₁ ∪ B₂) + = M.spacelikeComplement B₁ ∩ M.spacelikeComplement B₂ := by + ext x + simp_rw [mem_spacelikeComplement, Set.mem_inter_iff] + exact M.isCompletelySpacelike_union_right {x} B₁ B₂ + +/-- **Infinitary De Morgan (set level).** The spacelike complement turns an +indexed union into an intersection: `(⋃ i, B i)^⊥ = ⋂ i, (B i)^⊥`. -/ +theorem spacelikeComplement_iUnion {ι : Sort*} (B : ι → Set M.Carrier) : + M.spacelikeComplement (⋃ i, B i) = ⋂ i, M.spacelikeComplement (B i) := by + ext x + simp_rw [mem_spacelikeComplement, Set.mem_iInter] + constructor + · intro h i + exact M.isCompletelySpacelike_mono (subset_refl _) (Set.subset_iUnion B i) h + · intro h + rw [isCompletelySpacelike_singleton_left_iff] + intro y hy + rcases Set.mem_iUnion.1 hy with ⟨i, hy⟩ + have hxBi : M.IsCompletelySpacelike {x} (B i) := h i + rw [isCompletelySpacelike_singleton_left_iff] at hxBi + exact hxBi y hy + +/-! ### De Morgan laws for the causal complement + +On the complete lattice of causally complete regions the causal complement is an +order-reversing involution, hence satisfies the full De Morgan laws. The lattice +is not linearly ordered, so the equalities below rely on the involution +(`causalComplement_causalComplement`), not on antitonicity alone. -/ + +/-- The causal complement is **antitone** (order-reversing) on the lattice of +causally complete regions. -/ +private theorem coe_inf (B₁ B₂ : M.CausallyCompleteRegion) : (B₁ ⊓ B₂).1 = B₁.1 ∩ B₂.1 := by + rfl + +private theorem coe_sup (B₁ B₂ : M.CausallyCompleteRegion) : + (B₁ ⊔ B₂).1 = M.causalClosure (B₁.1 ∪ B₂.1) := by + rfl + +private theorem coe_top : (⊤ : M.CausallyCompleteRegion).1 = (Set.univ : Set M.Carrier) := by + rfl + +private theorem coe_bot : + (⊥ : M.CausallyCompleteRegion).1 = M.causalClosure (∅ : Set M.Carrier) := by + rfl + +private theorem coe_iSup {ι : Sort*} (B : ι → M.CausallyCompleteRegion) : + (⨆ i, B i).1 = M.causalClosure (⋃ i, (B i).1) := by + have h := (GaloisInsertion.l_iSup_u M.causalClosure.gi B) + have h' := congrArg Subtype.val h.symm + have h'' : (M.causalClosure.toCloseds (⨆ i, (B i).1)).1 = M.causalClosure (⨆ i, (B i).1) := rfl + rw [h''] at h' + rw [Set.iSup_eq_iUnion] at h' + exact h' + +private theorem coe_iInf {ι : Sort*} (B : ι → M.CausallyCompleteRegion) : + (⨅ i, B i).1 = M.causalClosure (⋂ i, (B i).1) := by + have h := (GaloisInsertion.l_iInf_u M.causalClosure.gi B) + have h' := congrArg Subtype.val h.symm + have h'' : (M.causalClosure.toCloseds (⨅ i, (B i).1)).1 = M.causalClosure (⨅ i, (B i).1) := rfl + rw [h''] at h' + rw [Set.iInf_eq_iInter] at h' + exact h' + +theorem causalComplement_antitone : Antitone M.causalComplement := by + intro B₁ B₂ h + rw [← Subtype.coe_le_coe] + have h' : B₁.1 ⊆ B₂.1 := h + rw [causalComplement_coe, causalComplement_coe] + exact M.spacelikeComplement_antitone h' + +/-- `⊥^⊥ = ⊤`: the complement of the least region is the greatest. -/ +theorem causalComplement_bot : + M.causalComplement (⊥ : M.CausallyCompleteRegion) = ⊤ := by + apply Subtype.ext + calc + (M.causalComplement (⊥ : M.CausallyCompleteRegion)).1 + = M.spacelikeComplement (⊥ : M.CausallyCompleteRegion).1 := rfl + _ = M.spacelikeComplement (M.causalClosure (∅ : Set M.Carrier)) := by rw [coe_bot] + _ = M.spacelikeComplement + (M.spacelikeComplement (M.spacelikeComplement (∅ : Set M.Carrier))) := rfl + _ = M.spacelikeComplement (∅ : Set M.Carrier) := by + rw [M.spacelikeComplement_spacelikeComplement_spacelikeComplement] + _ = Set.univ := by rw [M.spacelikeComplement_empty] + _ = (⊤ : M.CausallyCompleteRegion).1 := by rw [coe_top] + +/-- `⊤^⊥ = ⊥`: the complement of the greatest region is the least. -/ +theorem causalComplement_top : + M.causalComplement (⊤ : M.CausallyCompleteRegion) = ⊥ := by + apply Subtype.ext + calc + (M.causalComplement (⊤ : M.CausallyCompleteRegion)).1 + = M.spacelikeComplement (⊤ : M.CausallyCompleteRegion).1 := rfl + _ = M.spacelikeComplement (Set.univ : Set M.Carrier) := by rw [coe_top] + _ = M.spacelikeComplement (M.spacelikeComplement (∅ : Set M.Carrier)) := by + rw [M.spacelikeComplement_empty] + _ = M.causalClosure (∅ : Set M.Carrier) := rfl + _ = (⊥ : M.CausallyCompleteRegion).1 := by rw [coe_bot] + +/-- **Binary De Morgan (join).** `(B₁ ⊔ B₂)^⊥ = B₁^⊥ ⊓ B₂^⊥`. -/ +theorem causalComplement_sup (B₁ B₂ : M.CausallyCompleteRegion) : + M.causalComplement (B₁ ⊔ B₂) = M.causalComplement B₁ ⊓ M.causalComplement B₂ := by + apply Subtype.ext + calc + (M.causalComplement (B₁ ⊔ B₂)).1 = M.spacelikeComplement ((B₁ ⊔ B₂).1) := rfl + _ = M.spacelikeComplement (M.causalClosure (B₁.1 ∪ B₂.1)) := by rw [coe_sup] + _ = M.spacelikeComplement (M.spacelikeComplement (M.spacelikeComplement (B₁.1 ∪ B₂.1))) := rfl + _ = M.spacelikeComplement (B₁.1 ∪ B₂.1) := by + rw [M.spacelikeComplement_spacelikeComplement_spacelikeComplement] + _ = M.spacelikeComplement B₁.1 ∩ M.spacelikeComplement B₂.1 := by + rw [M.spacelikeComplement_union] + _ = (M.causalComplement B₁).1 ∩ (M.causalComplement B₂).1 := rfl + _ = ((M.causalComplement B₁) ⊓ (M.causalComplement B₂)).1 := by rw [coe_inf] + +/-- **Binary De Morgan (meet).** `(B₁ ⊓ B₂)^⊥ = B₁^⊥ ⊔ B₂^⊥`. -/ +theorem causalComplement_inf (B₁ B₂ : M.CausallyCompleteRegion) : + M.causalComplement (B₁ ⊓ B₂) = M.causalComplement B₁ ⊔ M.causalComplement B₂ := by + apply Subtype.ext + have h₁ : M.spacelikeComplement (M.spacelikeComplement B₁.1) = B₁.1 := + M.isCausallyComplete_iff_isClosed.mpr B₁.2 + have h₂ : M.spacelikeComplement (M.spacelikeComplement B₂.1) = B₂.1 := + M.isCausallyComplete_iff_isClosed.mpr B₂.2 + calc + (M.causalComplement (B₁ ⊓ B₂)).1 = M.spacelikeComplement ((B₁ ⊓ B₂).1) := rfl + _ = M.spacelikeComplement (B₁.1 ∩ B₂.1) := by rw [coe_inf] + _ = M.spacelikeComplement (M.spacelikeComplement (M.spacelikeComplement B₁.1) + ∩ M.spacelikeComplement (M.spacelikeComplement B₂.1)) := by + rw [h₁, h₂] + _ = M.spacelikeComplement (M.spacelikeComplement (M.spacelikeComplement B₁.1 + ∪ M.spacelikeComplement B₂.1)) := by + rw [M.spacelikeComplement_union] + _ = M.causalClosure (M.spacelikeComplement B₁.1 ∪ M.spacelikeComplement B₂.1) := rfl + _ = ((M.causalComplement B₁) ⊔ (M.causalComplement B₂)).1 := by + rw [coe_sup, causalComplement_coe, causalComplement_coe] + +/-- **Infinitary De Morgan (join).** `(⨆ i, B i)^⊥ = ⨅ i, (B i)^⊥`. -/ +theorem causalComplement_iSup {ι : Sort*} (B : ι → M.CausallyCompleteRegion) : + M.causalComplement (⨆ i, B i) = ⨅ i, M.causalComplement (B i) := by + apply Subtype.ext + calc + (M.causalComplement (⨆ i, B i)).1 = M.spacelikeComplement ((⨆ i, B i).1) := rfl + _ = M.spacelikeComplement (M.causalClosure (⋃ i, (B i).1)) := by rw [coe_iSup] + _ = M.spacelikeComplement (M.spacelikeComplement (M.spacelikeComplement (⋃ i, (B i).1))) := rfl + _ = M.spacelikeComplement (⋃ i, (B i).1) := by + rw [M.spacelikeComplement_spacelikeComplement_spacelikeComplement] + _ = ⋂ i, M.spacelikeComplement ((B i).1) := by rw [M.spacelikeComplement_iUnion] + _ = ⋂ i, (M.causalComplement (B i)).1 := by simp_rw [causalComplement_coe] + _ = M.causalClosure (⋂ i, (M.causalComplement (B i)).1) := by + have hclosed : M.IsCausallyComplete (⋂ i, (M.causalComplement (B i)).1) := + isCausallyComplete_iInter M (fun i => (M.causalComplement (B i)).1) fun i => by + exact (M.causalComplement (B i)).2 + have hclosed' : M.causalClosure (⋂ i, (M.causalComplement (B i)).1) + = ⋂ i, (M.causalComplement (B i)).1 := by + rw [M.causalClosure_apply, hclosed] + rw [hclosed'] + _ = (⨅ i, M.causalComplement (B i)).1 := by rw [coe_iInf] + +/-- **Infinitary De Morgan (meet).** `(⨅ i, B i)^⊥ = ⨆ i, (B i)^⊥`. -/ +theorem causalComplement_iInf {ι : Sort*} (B : ι → M.CausallyCompleteRegion) : + M.causalComplement (⨅ i, B i) = ⨆ i, M.causalComplement (B i) := by + apply Subtype.ext + have hclosed (i : ι) : M.spacelikeComplement (M.spacelikeComplement ((B i).1)) = (B i).1 := + M.isCausallyComplete_iff_isClosed.mpr (B i).2 + calc + (M.causalComplement (⨅ i, B i)).1 = M.spacelikeComplement ((⨅ i, B i).1) := rfl + _ = M.spacelikeComplement (M.causalClosure (⋂ i, (B i).1)) := by rw [coe_iInf] + _ = M.spacelikeComplement (M.spacelikeComplement (M.spacelikeComplement (⋂ i, (B i).1))) := rfl + _ = M.spacelikeComplement (⋂ i, (B i).1) := by + rw [M.spacelikeComplement_spacelikeComplement_spacelikeComplement] + _ = M.spacelikeComplement (⋂ i, M.spacelikeComplement (M.spacelikeComplement ((B i).1))) := by + simp_rw [hclosed] + _ = M.spacelikeComplement (M.spacelikeComplement (⋃ i, M.spacelikeComplement ((B i).1))) := by + rw [M.spacelikeComplement_iUnion] + _ = M.causalClosure (⋃ i, M.spacelikeComplement ((B i).1)) := rfl + _ = M.causalClosure (⋃ i, (M.causalComplement (B i)).1) := by + simp_rw [causalComplement_coe] + _ = (⨆ i, M.causalComplement (B i)).1 := by rw [coe_iSup] + +end LorentzianSpacetime +end Spacetime +end Physicslib4 diff --git a/Physicslib4/Spacetime/CausalStructure.lean b/Physicslib4/Spacetime/CausalStructure.lean index bacce9c..1ae7c00 100644 --- a/Physicslib4/Spacetime/CausalStructure.lean +++ b/Physicslib4/Spacetime/CausalStructure.lean @@ -110,7 +110,7 @@ reparametrisation-invariance of the causal type of a curve. -/ /-- The metric square scales quadratically: `g(c•v, c•v) = c² · g(v,v)`. -/ theorem val_smul_smul {x : M.Carrier} (c : ℝ) (v : TangentSpace M.model x) : M.val x (c • v) (c • v) = c ^ 2 * M.val x v v := by - simp only [map_smul, ContinuousLinearMap.smul_apply, smul_eq_mul] + simp only [map_smul, smul_apply, smul_eq_mul] ring /-- **Scaling invariance of timelikeness.** For `c ≠ 0`, `c • v` is timelike iff diff --git a/Physicslib4/Spacetime/Causality.lean b/Physicslib4/Spacetime/Causality.lean index 0a98864..f76feb7 100644 --- a/Physicslib4/Spacetime/Causality.lean +++ b/Physicslib4/Spacetime/Causality.lean @@ -78,23 +78,21 @@ def IsGeodesic (_μ : M.SmoothPath) : Prop := True /-! ### Trips and chronological precedence -/ /-- -A *trip* from `p` to `q` in a spacetime `M` is a smooth curve `c` together -with a representative smooth path `μ` that +A *trip segment* from `p` to `q` in a spacetime `M` is a smooth curve `c` +together with a representative smooth path `μ` that -* is piecewise future-oriented and timelike; -* is piecewise a geodesic; +* is future-oriented and timelike; +* is a geodesic; * has past endpoint `p` and future endpoint `q`. -The "piecewise" condition is captured by the existence of a finite -ascending list of cut points `s₀ < s₁ < ⋯ < sₖ` in the parameter space -such that on each sub-interval the path restricts to a future-oriented -timelike geodesic. +This is a single geodesic piece; a full (piecewise) trip is a finite chain +of such segments (see `IsTrip`). A `TimeOrientation` argument `t` is required to talk about future-orientation. The endpoints `p, q : M.Carrier` are given as parameters. -/ -def IsTrip (t : M.TimeOrientation) (p q : M.Carrier) +def IsTripSegment (t : M.TimeOrientation) (p q : M.Carrier) (c : SmoothCurve M) : Prop := ∃ rep : M.SmoothPath, c = SmoothCurve.ofPath M rep ∧ @@ -104,10 +102,26 @@ def IsTrip (t : M.TimeOrientation) (p q : M.Carrier) IsPastEndpoint M rep p ∧ IsFutureEndpoint M rep q +/-- *Single-segment chronological precedence*: `p` and `q` are joined by one +future-oriented timelike geodesic segment. -/ +def SegmentPrecedes (t : M.TimeOrientation) (p q : M.Carrier) : Prop := + ∃ c : SmoothCurve M, IsTripSegment M t p q c + +/-- +A *trip* from `p` to `q`: a curve which is *piecewise* a future-oriented +timelike geodesic, i.e. a finite chain of trip segments joined at matching +endpoints. This is encoded as the transitive closure of single-segment +precedence, which is exactly "there is a finite ascending sequence +`p = x₀, x₁, …, xₙ = q` with each consecutive pair joined by a +future-oriented timelike geodesic segment". This genuinely piecewise form +is what makes chronological precedence transitive by concatenation. -/ +def IsTrip (t : M.TimeOrientation) (p q : M.Carrier) : Prop := + Relation.TransGen (SegmentPrecedes M t) p q + /-- *Chronological precedence*: `p ≪ q` iff there exists a trip from `p` to `q`, relative to a fixed time orientation. -/ def ChronologicallyPrecedes (t : M.TimeOrientation) (p q : M.Carrier) : Prop := - ∃ c : SmoothCurve M, IsTrip M t p q c + IsTrip M t p q @[inherit_doc] scoped notation:50 p " ≪[" M ", " t "] " q => ChronologicallyPrecedes M t p q @@ -115,14 +129,14 @@ def ChronologicallyPrecedes (t : M.TimeOrientation) (p q : M.Carrier) : Prop := /-! ### Causal trips and causal precedence -/ /-- -A *causal trip* from `p` to `q` in a spacetime `M` is a smooth curve `c` -together with a representative smooth path `μ` that +A *causal trip segment* from `p` to `q` in a spacetime `M` is a smooth curve +`c` together with a representative smooth path `μ` that -* is piecewise future-oriented and causal; -* is piecewise a (possibly degenerate) geodesic; +* is future-oriented and causal; +* is a (possibly degenerate) geodesic; * has past endpoint `p` and future endpoint `q`. -/ -def IsCausalTrip (t : M.TimeOrientation) (p q : M.Carrier) +def IsCausalTripSegment (t : M.TimeOrientation) (p q : M.Carrier) (c : SmoothCurve M) : Prop := ∃ rep : M.SmoothPath, c = SmoothCurve.ofPath M rep ∧ @@ -132,10 +146,22 @@ def IsCausalTrip (t : M.TimeOrientation) (p q : M.Carrier) IsPastEndpoint M rep p ∧ IsFutureEndpoint M rep q +/-- *Single-segment causal precedence*: `p` and `q` are joined by one +future-oriented causal geodesic segment. -/ +def CausalSegmentPrecedes (t : M.TimeOrientation) (p q : M.Carrier) : Prop := + ∃ c : SmoothCurve M, IsCausalTripSegment M t p q c + +/-- A *causal trip* from `p` to `q`: a curve which is piecewise a +future-oriented causal geodesic, i.e. a finite chain of causal trip +segments. Encoded as the transitive closure of single-segment causal +precedence. -/ +def IsCausalTrip (t : M.TimeOrientation) (p q : M.Carrier) : Prop := + Relation.TransGen (CausalSegmentPrecedes M t) p q + /-- *Causal precedence*: `p ≺ q` iff there exists a causal trip from `p` to `q`, relative to a fixed time orientation. -/ def CausallyPrecedes (t : M.TimeOrientation) (p q : M.Carrier) : Prop := - ∃ c : SmoothCurve M, IsCausalTrip M t p q c + IsCausalTrip M t p q @[inherit_doc] scoped notation:50 p " ≺[" M ", " t "] " q => CausallyPrecedes M t p q @@ -209,18 +235,42 @@ theorem isCausal_of_isTimelike {μ : M.SmoothPath} (h : SmoothPath.IsTimelike M μ) : SmoothPath.IsCausal M μ := fun s hs => Or.inl (h s hs) -/-- Every trip is a causal trip. -/ -theorem isCausalTrip_of_isTrip (t : M.TimeOrientation) {p q : M.Carrier} - {c : SmoothCurve M} (h : M.IsTrip t p q c) : M.IsCausalTrip t p q c := by +/-- Every trip segment is a causal trip segment. -/ +theorem isCausalTripSegment_of_isTripSegment (t : M.TimeOrientation) + {p q : M.Carrier} {c : SmoothCurve M} (h : M.IsTripSegment t p q c) : + M.IsCausalTripSegment t p q c := by obtain ⟨rep, hc, htl, hfo, hg, hpe, hfe⟩ := h exact ⟨rep, hc, M.isCausal_of_isTimelike htl, hfo, hg, hpe, hfe⟩ +/-- Single-segment chronological precedence implies single-segment causal +precedence. -/ +theorem causalSegmentPrecedes_of_segmentPrecedes (t : M.TimeOrientation) + {p q : M.Carrier} (h : M.SegmentPrecedes t p q) : + M.CausalSegmentPrecedes t p q := by + obtain ⟨c, hc⟩ := h + exact ⟨c, M.isCausalTripSegment_of_isTripSegment t hc⟩ + +/-- **Transitivity of chronological precedence.** Two trips joined at a common +point `q` concatenate to a single (piecewise) trip: `p ≪ q` and `q ≪ r` give +`p ≪ r`. This is exactly the transitivity of the transitive closure. -/ +theorem chronologicallyPrecedes_trans (t : M.TimeOrientation) + {p q r : M.Carrier} (h₁ : M.ChronologicallyPrecedes t p q) + (h₂ : M.ChronologicallyPrecedes t q r) : + M.ChronologicallyPrecedes t p r := + Relation.TransGen.trans h₁ h₂ + +/-- **Transitivity of causal precedence.** `p ≺ q` and `q ≺ r` give `p ≺ r`. -/ +theorem causallyPrecedes_trans (t : M.TimeOrientation) + {p q r : M.Carrier} (h₁ : M.CausallyPrecedes t p q) + (h₂ : M.CausallyPrecedes t q r) : + M.CausallyPrecedes t p r := + Relation.TransGen.trans h₁ h₂ + /-- Chronological precedence implies causal precedence. -/ theorem causallyPrecedes_of_chronologicallyPrecedes (t : M.TimeOrientation) {p q : M.Carrier} (h : M.ChronologicallyPrecedes t p q) : - M.CausallyPrecedes t p q := by - obtain ⟨c, hc⟩ := h - exact ⟨c, M.isCausalTrip_of_isTrip t hc⟩ + M.CausallyPrecedes t p q := + Relation.TransGen.mono (fun _ _ => M.causalSegmentPrecedes_of_segmentPrecedes t) _ _ h /-- The chronological future is contained in the causal future. -/ theorem chronologicalFuture_subset_causalFuture (t : M.TimeOrientation) @@ -232,6 +282,41 @@ theorem chronologicalPast_subset_causalPast (t : M.TimeOrientation) (p : M.Carrier) : chronologicalPast M t p ⊆ causalPast M t p := fun _ hq => M.causallyPrecedes_of_chronologicallyPrecedes t hq +/-! ### Causal-order refinements under the causality condition -/ + +/-- **The causality condition (no closed causal curve).** A spacetime satisfies the +causality condition when no point causally precedes itself: a closed causal curve +through `p` is exactly a causal trip `p ≺ p`, so its absence is `¬ (p ≺ p)` for all +`p`. This is strictly weaker than strong causality and strictly stronger than the +chronology condition `¬ (p ≪ p)`. -/ +def NoClosedCausalCurve (t : M.TimeOrientation) : Prop := + ∀ p : M.Carrier, ¬ M.CausallyPrecedes t p p + +/-- Under the causality condition, chronological precedence is **irreflexive**: +`¬ (p ≪ p)`, because `p ≪ p` would give the forbidden `p ≺ p`. -/ +theorem chronologicallyPrecedes_irrefl (t : M.TimeOrientation) + (hc : M.NoClosedCausalCurve t) (p : M.Carrier) : + ¬ M.ChronologicallyPrecedes t p p := by + intro h + exact hc p (M.causallyPrecedes_of_chronologicallyPrecedes t h) + +/-- Under the causality condition, causal precedence is **asymmetric**: +`p ≺ q → ¬ (q ≺ p)`, since transitivity would otherwise give the forbidden `p ≺ p`. -/ +theorem causallyPrecedes_asymm (t : M.TimeOrientation) + (hc : M.NoClosedCausalCurve t) {p q : M.Carrier} + (hpq : M.CausallyPrecedes t p q) : ¬ M.CausallyPrecedes t q p := by + intro hqp + exact hc p (M.causallyPrecedes_trans t hpq hqp) + +/-- Under the causality condition, causal precedence is **antisymmetric**: +`p ≺ q → q ≺ p → p = q` (in fact both cannot hold, since transitivity gives the +forbidden `p ≺ p`). Thus `≺` is a strict partial order. -/ +theorem causallyPrecedes_antisymm (t : M.TimeOrientation) + (hc : M.NoClosedCausalCurve t) {p q : M.Carrier} + (hpq : M.CausallyPrecedes t p q) (hqp : M.CausallyPrecedes t q p) : + p = q := by + exact absurd (M.causallyPrecedes_trans t hpq hqp) (hc p) + /-! ### Symmetry of spacelike relatedness -/ /-- Spacelike relatedness is symmetric. -/ @@ -350,6 +435,107 @@ theorem isOpen_alexandrov_of_mem_basis (t : M.TimeOrientation) @IsOpen M.Carrier (alexandrovTopology M t) B := TopologicalSpace.GenerateOpen.basic B hB +/-- **No-diamond points have only the whole space as neighbourhood.** If `x` lies +in no Alexandrov diamond `I⁺(p) ∩ I⁻(q)`, then every Alexandrov-open set (i.e. every +set generated from the diamond subbasis) containing `x` is the whole space `M`. -/ +theorem alexandrov_nbhd_univ_of_no_diamond (t : M.TimeOrientation) {x : M.Carrier} + (hx : ∀ s ∈ alexandrovBasis M t, x ∉ s) {U : Set M.Carrier} + (hU : TopologicalSpace.GenerateOpen (alexandrovBasis M t) U) (hxU : x ∈ U) : + U = Set.univ := by + induction hU with + | basic s hs => + exact absurd hxU (hx s hs) + | univ => + rfl + | inter s t hs ht ihs iht => + have hxs : x ∈ s := hxU.1 + have hxt : x ∈ t := hxU.2 + rw [ihs hxs, iht hxt, Set.inter_univ] + | sUnion G hG ih => + rcases Set.mem_sUnion.mp hxU with ⟨g, hgG, hxg⟩ + have hg_eq : g = Set.univ := ih g hgG hxg + have h_sub : Set.univ ⊆ ⋃₀ G := by + calc + Set.univ = g := hg_eq.symm + _ ⊆ ⋃₀ G := Set.subset_sUnion_of_mem hgG + exact Set.eq_univ_of_univ_subset h_sub + +/-! ### Openness of chronological futures and pasts -/ + +/-- Every set of the form `I^+(p) ∩ I^-(q)` is open in the Alexandrov topology. +This is the basis lemma restated on chronological futures and pasts. -/ +theorem isOpen_chronologicalFuture_inter_chronologicalPast (t : M.TimeOrientation) + (p q : M.Carrier) : + @IsOpen M.Carrier (alexandrovTopology M t) + (chronologicalFuture M t p ∩ chronologicalPast M t q) := by + exact isOpen_alexandrov_of_mem_basis M t ⟨p, q, rfl⟩ + +/-- If every point of `I^+(p)` has a chronological-future point (for all +`x ∈ I^+(p)` there exists `b` with `x ≪ b`), then the chronological future +`I^+(p)` is open in the Alexandrov topology. -/ +theorem isOpen_chronologicalFuture (t : M.TimeOrientation) (p : M.Carrier) + (h : ∀ x ∈ chronologicalFuture M t p, ∃ b, ChronologicallyPrecedes M t x b) : + @IsOpen M.Carrier (alexandrovTopology M t) (chronologicalFuture M t p) := by + -- Show I⁺(p) = ⋃_{b} (I⁺(p) ∩ I⁻(b)). + have h_eq : chronologicalFuture M t p = + ⋃ (b : M.Carrier), (chronologicalFuture M t p ∩ chronologicalPast M t b) := by + ext x + constructor + · intro hx + -- If x ∈ I⁺(p), then by hypothesis there is b with x ≪ b, i.e. x ∈ I⁻(b); + -- hence x ∈ I⁺(p) ∩ I⁻(b), so x ∈ the union. + obtain ⟨b, hxb⟩ := h x hx + have hx_mem_past : x ∈ chronologicalPast M t b := hxb + have hx_mem_inter : x ∈ chronologicalFuture M t p ∩ chronologicalPast M t b := + ⟨hx, hx_mem_past⟩ + exact Set.mem_iUnion.mpr ⟨b, hx_mem_inter⟩ + · intro hx + -- If x ∈ ⋃_{b} (I⁺(p) ∩ I⁻(b)), then x ∈ I⁺(p) (since each term is a subset of I⁺(p)). + rcases Set.mem_iUnion.mp hx with ⟨b, hx_inter⟩ + exact hx_inter.1 + -- Each (I⁺(p) ∩ I⁻(b)) is open by the basis lemma. + have h_open : ∀ b : M.Carrier, @IsOpen M.Carrier (alexandrovTopology M t) + (chronologicalFuture M t p ∩ chronologicalPast M t b) := by + intro b + exact isOpen_chronologicalFuture_inter_chronologicalPast M t p b + -- An arbitrary union of open sets is open. + rw [h_eq] + exact @isOpen_iUnion M.Carrier (M.Carrier) (alexandrovTopology M t) + (fun b => chronologicalFuture M t p ∩ chronologicalPast M t b) h_open + +/-- Dually, if every point of `I^-(p)` has a chronological-past point (for all +`x ∈ I^-(p)` there exists `a` with `a ≪ x`), then the chronological past +`I^-(p)` is open in the Alexandrov topology. -/ +theorem isOpen_chronologicalPast (t : M.TimeOrientation) (p : M.Carrier) + (h : ∀ x ∈ chronologicalPast M t p, ∃ a, ChronologicallyPrecedes M t a x) : + @IsOpen M.Carrier (alexandrovTopology M t) (chronologicalPast M t p) := by + -- Show I⁻(p) = ⋃_{a} (I⁺(a) ∩ I⁻(p)). + have h_eq : chronologicalPast M t p = + ⋃ (a : M.Carrier), (chronologicalFuture M t a ∩ chronologicalPast M t p) := by + ext x + constructor + · intro hx + -- If x ∈ I⁻(p), then by hypothesis there is a with a ≪ x, i.e. x ∈ I⁺(a); + -- hence x ∈ I⁺(a) ∩ I⁻(p), so x ∈ the union. + obtain ⟨a, hax⟩ := h x hx + have hx_mem_future : x ∈ chronologicalFuture M t a := hax + have hx_mem_inter : x ∈ chronologicalFuture M t a ∩ chronologicalPast M t p := + ⟨hx_mem_future, hx⟩ + exact Set.mem_iUnion.mpr ⟨a, hx_mem_inter⟩ + · intro hx + -- If x ∈ ⋃_{a} (I⁺(a) ∩ I⁻(p)), then x ∈ I⁻(p) (since each term is a subset of I⁻(p)). + rcases Set.mem_iUnion.mp hx with ⟨a, hx_inter⟩ + exact hx_inter.2 + -- Each (I⁺(a) ∩ I⁻(p)) is open by the basis lemma. + have h_open : ∀ a : M.Carrier, @IsOpen M.Carrier (alexandrovTopology M t) + (chronologicalFuture M t a ∩ chronologicalPast M t p) := by + intro a + exact isOpen_chronologicalFuture_inter_chronologicalPast M t a p + -- An arbitrary union of open sets is open. + rw [h_eq] + exact @isOpen_iUnion M.Carrier (M.Carrier) (alexandrovTopology M t) + (fun a => chronologicalFuture M t a ∩ chronologicalPast M t p) h_open + end Spacetime end Physicslib4 diff --git a/Physicslib4/Spacetime/Isometry.lean b/Physicslib4/Spacetime/Isometry.lean index dcedf74..72a6508 100644 --- a/Physicslib4/Spacetime/Isometry.lean +++ b/Physicslib4/Spacetime/Isometry.lean @@ -34,12 +34,17 @@ Composition and inverse preserve the metric via the manifold chain rule `PartialHomeomorph.MDifferentiable.comp_symm_deriv` does. The isometries thus form a group acting on points. -**Deferred refinement.** The blueprint's identity-component -("connected to the identity") restriction is not captured: it requires a -topology on the diffeomorphism group and its identity component, for -which Mathlib has no ready support. The present `Isometry M` is the full -metric-preserving diffeomorphism group; the identity-component subgroup -is a future refinement. +**On the identity-component restriction.** `Isometry M` is the full +metric-preserving diffeomorphism group. The blueprint's identity-component +("connected to the identity") restriction of Axiom 5 is captured downstream: +`Physicslib4/Spacetime/IsometryTopology.lean` topologizes this group as a +topological group and defines the identity-component subgroup +`Isometry.identityComponent := Subgroup.connectedComponentOfOne`, and +`Isometry.orientedIdentityComponent` (`IsometryCausality.lean`) intersects it +with future-orientation preservation. That subgroup is the `M.Isom` supplied to +the curved Haag-Kastler bridge `toAbstractIdentityComponent`. The full group is +retained here as the substrate and for the axioms that hold under all +isometries (e.g. microcausality). -/ namespace Physicslib4 diff --git a/Physicslib4/Spacetime/IsometryCausality.lean b/Physicslib4/Spacetime/IsometryCausality.lean index b41b0c3..1d7de20 100644 --- a/Physicslib4/Spacetime/IsometryCausality.lean +++ b/Physicslib4/Spacetime/IsometryCausality.lean @@ -237,12 +237,12 @@ theorem pushforwardPath_isFutureOriented (g : Isometry M) (μ : M.SmoothPath) simp only [pushforwardPath_tangent g μ hs] exact hg (μ.toFun s) _ (h s hs) -/-- Under future-orientation preservation, an isometry carries chronological -precedence forward: `p ≪ q` implies `g p ≪ g q`. -/ -theorem chronologicallyPrecedes_pushforward (g : Isometry M) (t : M.TimeOrientation) +/-- Under future-orientation preservation, an isometry carries a single +trip segment forward. -/ +theorem segmentPrecedes_pushforward (g : Isometry M) (t : M.TimeOrientation) (hg : g.PreservesFutureOrientation t) {p q : M.Carrier} - (h : ChronologicallyPrecedes M t p q) : - ChronologicallyPrecedes M t (g.toDiffeo p) (g.toDiffeo q) := by + (h : SegmentPrecedes M t p q) : + SegmentPrecedes M t (g.toDiffeo p) (g.toDiffeo q) := by obtain ⟨c, rep, hc, htl, hfo, hgeo, hpe, hfe⟩ := h exact ⟨SmoothCurve.ofPath M (g.pushforwardPath rep), g.pushforwardPath rep, rfl, g.pushforwardPath_isTimelike rep htl, @@ -251,6 +251,20 @@ theorem chronologicallyPrecedes_pushforward (g : Isometry M) (t : M.TimeOrientat g.pushforwardPath_isPastEndpoint rep hpe, g.pushforwardPath_isFutureEndpoint rep hfe⟩ +/-- Under future-orientation preservation, an isometry carries chronological +precedence forward: `p ≪ q` implies `g p ≪ g q`. A trip is a finite chain of +trip segments, so this lifts `segmentPrecedes_pushforward` along the transitive +closure (`Relation.TransGen.lift`). -/ +theorem chronologicallyPrecedes_pushforward (g : Isometry M) (t : M.TimeOrientation) + (hg : g.PreservesFutureOrientation t) {p q : M.Carrier} + (h : ChronologicallyPrecedes M t p q) : + ChronologicallyPrecedes M t (g.toDiffeo p) (g.toDiffeo q) := by + -- `ChronologicallyPrecedes` is `Relation.TransGen` of `SegmentPrecedes`. + -- `TransGen.lift` lifts a relation `r ≤ p ∘ (f, f)` to `TransGen r ≤ TransGen p ∘ (f, f)`. + exact Relation.TransGen.lift (f := g.toDiffeo) + (r := Spacetime.SegmentPrecedes M t) (p := Spacetime.SegmentPrecedes M t) + (fun a b hs => segmentPrecedes_pushforward g t hg hs) _ _ h + /-- Under future-orientation preservation, the image of a chronological future is contained in the chronological future of the image point. -/ theorem chronologicalFuture_image_subset (g : Isometry M) (t : M.TimeOrientation) diff --git a/Physicslib4/Spacetime/LorentzCausality.lean b/Physicslib4/Spacetime/LorentzCausality.lean index e563981..a3eb99e 100644 --- a/Physicslib4/Spacetime/LorentzCausality.lean +++ b/Physicslib4/Spacetime/LorentzCausality.lean @@ -295,12 +295,12 @@ theorem lorentzPath_isFutureEndpoint (g : InhomogeneousLorentzGroup) /-- **A Lorentz transformation maps causal trips to causal trips**, hence preserves causal precedence: if `p ≺ q` then `g • p ≺ g • q`. -/ -theorem causallyPrecedes_smul (g : InhomogeneousLorentzGroup) +theorem causalSegmentPrecedes_smul (g : InhomogeneousLorentzGroup) {p q : StandardMinkowskiSpacetime.Carrier} - (h : CausallyPrecedes StandardMinkowskiSpacetime + (h : CausalSegmentPrecedes StandardMinkowskiSpacetime standardMinkowskiTimeOrientation p q) : - CausallyPrecedes StandardMinkowskiSpacetime standardMinkowskiTimeOrientation - (g • p) (g • q) := by + CausalSegmentPrecedes StandardMinkowskiSpacetime + standardMinkowskiTimeOrientation (g • p) (g • q) := by obtain ⟨c, rep, hc, hcausal, hfut, hgeo, hpast, hfuture⟩ := h exact ⟨SmoothCurve.ofPath StandardMinkowskiSpacetime (lorentzPath g rep), lorentzPath g rep, rfl, @@ -310,6 +310,18 @@ theorem causallyPrecedes_smul (g : InhomogeneousLorentzGroup) lorentzPath_isPastEndpoint g rep hpast, lorentzPath_isFutureEndpoint g rep hfuture⟩ +/-- **A Lorentz transformation maps causal trips to causal trips**, hence +preserves causal precedence: if `p ≺ q` then `g • p ≺ g • q`. Lifts +`causalSegmentPrecedes_smul` along the transitive closure. -/ +theorem causallyPrecedes_smul (g : InhomogeneousLorentzGroup) + {p q : StandardMinkowskiSpacetime.Carrier} + (h : CausallyPrecedes StandardMinkowskiSpacetime + standardMinkowskiTimeOrientation p q) : + CausallyPrecedes StandardMinkowskiSpacetime standardMinkowskiTimeOrientation + (g • p) (g • q) := + Relation.TransGen.lift (fun x => g • x) + (fun _ _ hs => causalSegmentPrecedes_smul g hs) _ _ h + /-- **Causal precedence is Lorentz invariant.** -/ theorem causallyPrecedes_smul_iff (g : InhomogeneousLorentzGroup) (p q : StandardMinkowskiSpacetime.Carrier) : @@ -370,11 +382,11 @@ theorem lorentzPath_isTimelike (g : InhomogeneousLorentzGroup) /-- **A Lorentz transformation maps trips to trips**, hence preserves chronological precedence: if `p ≪ q` then `g • p ≪ g • q`. -/ -theorem chronologicallyPrecedes_smul (g : InhomogeneousLorentzGroup) +theorem segmentPrecedes_smul (g : InhomogeneousLorentzGroup) {p q : StandardMinkowskiSpacetime.Carrier} - (h : ChronologicallyPrecedes StandardMinkowskiSpacetime + (h : SegmentPrecedes StandardMinkowskiSpacetime standardMinkowskiTimeOrientation p q) : - ChronologicallyPrecedes StandardMinkowskiSpacetime + SegmentPrecedes StandardMinkowskiSpacetime standardMinkowskiTimeOrientation (g • p) (g • q) := by obtain ⟨c, rep, hc, htimelike, hfut, hgeo, hpast, hfuture⟩ := h exact ⟨SmoothCurve.ofPath StandardMinkowskiSpacetime (lorentzPath g rep), @@ -385,6 +397,17 @@ theorem chronologicallyPrecedes_smul (g : InhomogeneousLorentzGroup) lorentzPath_isPastEndpoint g rep hpast, lorentzPath_isFutureEndpoint g rep hfuture⟩ +/-- **A Lorentz transformation maps trips to trips**, hence preserves +chronological precedence: if `p ≪ q` then `g • p ≪ g • q`. Lifts +`segmentPrecedes_smul` along the transitive closure. -/ +theorem chronologicallyPrecedes_smul (g : InhomogeneousLorentzGroup) + {p q : StandardMinkowskiSpacetime.Carrier} + (h : ChronologicallyPrecedes StandardMinkowskiSpacetime + standardMinkowskiTimeOrientation p q) : + ChronologicallyPrecedes StandardMinkowskiSpacetime + standardMinkowskiTimeOrientation (g • p) (g • q) := + Relation.TransGen.lift (fun x => g • x) (fun _ _ hs => segmentPrecedes_smul g hs) _ _ h + /-- **Chronological precedence is Lorentz invariant.** -/ theorem chronologicallyPrecedes_smul_iff (g : InhomogeneousLorentzGroup) (p q : StandardMinkowskiSpacetime.Carrier) : diff --git a/Physicslib4/Spacetime/LorentzCone.lean b/Physicslib4/Spacetime/LorentzCone.lean index 9d0ac51..1e705e0 100644 --- a/Physicslib4/Spacetime/LorentzCone.lean +++ b/Physicslib4/Spacetime/LorentzCone.lean @@ -97,7 +97,7 @@ namespace Spacetime private theorem val_add_self (M : Spacetime) (x : M.Carrier) (v w : TangentSpace M.model x) : M.val x (v + w) (v + w) = M.val x v v + 2 * M.val x v w + M.val x w w := by - simp only [map_add, ContinuousLinearMap.add_apply] + simp only [map_add, add_apply] rw [M.symm x w v]; ring /-- **Convexity of the timelike cone** for the metric of a spacetime: the sum of diff --git a/Physicslib4/Spacetime/LorentzOrthogonal.lean b/Physicslib4/Spacetime/LorentzOrthogonal.lean index 46ff607..b46913b 100644 --- a/Physicslib4/Spacetime/LorentzOrthogonal.lean +++ b/Physicslib4/Spacetime/LorentzOrthogonal.lean @@ -372,7 +372,7 @@ theorem isFuturePointing_add_general (M : Spacetime) (x : M.Carrier) · exact le_of_eq h have hvw : M.val x v w ≤ 0 := inner_nonpos_of_future M x τ hfv hfw have hexp : M.val x (v + w) (v + w) = M.val x v v + 2 * (M.val x v w) + M.val x w w := by - simp only [map_add, ContinuousLinearMap.add_apply] + simp only [map_add, add_apply] rw [M.symm x w v]; ring have hcausal : M.val x (v + w) (v + w) ≤ 0 := by rw [hexp]; linarith [hvv, hww, hvw] -- The time-orientation pairing is nonpositive on the sum. @@ -398,7 +398,7 @@ theorem isPastPointing_iff_isFuturePointing_neg (M : Spacetime) (x : M.Carrier) (τ : M.TimeOrientation) {v : TangentSpace M.model x} : M.IsPastPointing τ v ↔ M.IsFuturePointing τ (-v) := by have hquad : ∀ u : TangentSpace M.model x, M.val x (-u) (-u) = M.val x u u := fun u => by - simp only [map_neg, ContinuousLinearMap.neg_apply, neg_neg] + simp only [map_neg, neg_apply, neg_neg] have hlin : ∀ u : TangentSpace M.model x, M.val x (τ.field x) (-u) = -(M.val x (τ.field x) u) := fun u => by rw [map_neg] simp only [IsPastPointing, IsFuturePointing, IsTimelike, IsNull] @@ -429,14 +429,14 @@ theorem inner_neg_of_past_timelike (M : Spacetime) (x : M.Carrier) M.val x v w < 0 := by have hv' : M.IsTimelike (-v) := by change M.val x (-v) (-v) < 0 - simp only [map_neg, ContinuousLinearMap.neg_apply, neg_neg]; exact hv + simp only [map_neg, neg_apply, neg_neg]; exact hv have hw' : M.IsTimelike (-w) := by change M.val x (-w) (-w) < 0 - simp only [map_neg, ContinuousLinearMap.neg_apply, neg_neg]; exact hw + simp only [map_neg, neg_apply, neg_neg]; exact hw have hsv : M.val x (τ.field x) (-v) < 0 := by rw [map_neg]; linarith have hsw : M.val x (τ.field x) (-w) < 0 := by rw [map_neg]; linarith have h := inner_neg_of_future_timelike M x τ hv' hw' hsv hsw - simpa only [map_neg, ContinuousLinearMap.neg_apply, neg_neg] using h + simpa only [map_neg, neg_apply, neg_neg] using h /-- **Convexity of the past cone.** The sum of any two past-pointing tangent vectors (timelike or null) is past-pointing. Obtained from @@ -455,7 +455,7 @@ theorem isFuturePointing_smul_pos (M : Spacetime) (x : M.Carrier) (τ : M.TimeOrientation) {v : TangentSpace M.model x} {c : ℝ} (hc : 0 < c) (hfv : M.IsFuturePointing τ v) : M.IsFuturePointing τ (c • v) := by have hquad : ∀ u : TangentSpace M.model x, M.val x (c • u) (c • u) = c * (c * M.val x u u) := - fun u => by simp only [map_smul, ContinuousLinearMap.smul_apply, smul_eq_mul] + fun u => by simp only [map_smul, smul_apply, smul_eq_mul] have hlin : ∀ u : TangentSpace M.model x, M.val x (τ.field x) (c • u) = c * M.val x (τ.field x) u := fun u => by rw [map_smul, smul_eq_mul] diff --git a/Physicslib4/Spacetime/LorentzianSpacetime.lean b/Physicslib4/Spacetime/LorentzianSpacetime.lean index 4fc6061..93460a2 100644 --- a/Physicslib4/Spacetime/LorentzianSpacetime.lean +++ b/Physicslib4/Spacetime/LorentzianSpacetime.lean @@ -5,6 +5,7 @@ Authors: Lean Community -/ import Physicslib4.Spacetime.Causality import Mathlib.Topology.Separation.Hausdorff +import Mathlib.Topology.Bases /-! # Lorentzian spacetime @@ -151,6 +152,57 @@ theorem isOpen_alexandrov_of_isBasisSet {B : Set M.Carrier} @IsOpen M.Carrier (alexandrovTopology M.toSpacetime M.timeOrientation) B := Spacetime.isOpen_alexandrov_of_mem_basis M.toSpacetime M.timeOrientation hB +/-! ### The Alexandrov diamonds as a genuine topological basis -/ + +/-- **Covering from the Hausdorff assumption.** On a Lorentzian spacetime with at +least two points, the Alexandrov diamonds cover the whole space: every point lies in +some diamond `I⁺(p) ∩ I⁻(q)`. A point in no diamond would have `univ` as its only +Alexandrov-open neighbourhood, contradicting Hausdorffness. -/ +theorem sUnion_alexandrovBasis_eq_univ [Nontrivial M.Carrier] : + ⋃₀ (alexandrovBasis M.toSpacetime M.timeOrientation) = Set.univ := by + rw [Set.eq_univ_iff_forall] + intro x + by_contra hx + -- hx : x ∉ ⋃₀ (alexandrovBasis ...) means every basis set misses x + -- Key: any Alexandrov-open set containing x must be the whole space. + have key : ∀ (U : Set M.Carrier), + TopologicalSpace.GenerateOpen (alexandrovBasis M.toSpacetime M.timeOrientation) U → + x ∈ U → U = Set.univ := by + intro U hU hxU + induction hU with + | basic s hs => exact (hx ⟨s, hs, hxU⟩).elim + | univ => rfl + | inter s t hs ht ihs iht => rw [ihs hxU.1, iht hxU.2, Set.inter_univ] + | sUnion G hG ih => + obtain ⟨g, hgG, hxg⟩ := hxU + exact Set.univ_subset_iff.mp (ih g hgG hxg ▸ Set.subset_sUnion_of_mem hgG) + -- Choose a second point y ≠ x (the space is nontrivial); T₂ separation gives + -- disjoint open sets around x and y, but the one around x is forced to be `univ`. + obtain ⟨y, hy⟩ := exists_ne x + obtain ⟨U, V, hUo, _, hxU, hyV, hdisj⟩ := + @t2_separation M.Carrier (alexandrovTopology M.toSpacetime M.timeOrientation) + M.instT2SpaceAlexandrov x y (Ne.symm hy) + exact Set.disjoint_left.mp hdisj ((key U hUo hxU).ge (Set.mem_univ y)) hyV + +/-- **The Alexandrov diamonds form a topological basis.** On a Lorentzian spacetime +with at least two points, if the diamonds are downward-directed (the intersection +property), they form a genuine `IsTopologicalBasis` for the Alexandrov topology. The +covering condition is `sUnion_alexandrovBasis_eq_univ`; the generation condition is +definitional. -/ +theorem isTopologicalBasis_alexandrovBasis [Nontrivial M.Carrier] + (hdir : ∀ B₁ ∈ alexandrovBasis M.toSpacetime M.timeOrientation, + ∀ B₂ ∈ alexandrovBasis M.toSpacetime M.timeOrientation, + ∀ x ∈ B₁ ∩ B₂, ∃ B₃ ∈ alexandrovBasis M.toSpacetime M.timeOrientation, + x ∈ B₃ ∧ B₃ ⊆ B₁ ∩ B₂) : + @TopologicalSpace.IsTopologicalBasis M.Carrier + (alexandrovTopology M.toSpacetime M.timeOrientation) + (alexandrovBasis M.toSpacetime M.timeOrientation) := by + refine @TopologicalSpace.IsTopologicalBasis.mk M.Carrier + (alexandrovTopology M.toSpacetime M.timeOrientation) + (alexandrovBasis M.toSpacetime M.timeOrientation) + hdir (sUnion_alexandrovBasis_eq_univ M) ?_ + rfl + end LorentzianSpacetime end Spacetime diff --git a/Physicslib4/Spacetime/Minkowski.lean b/Physicslib4/Spacetime/Minkowski.lean index fb0b1d1..68c92fa 100644 --- a/Physicslib4/Spacetime/Minkowski.lean +++ b/Physicslib4/Spacetime/Minkowski.lean @@ -475,7 +475,7 @@ theorem minkowskiForm_single_zero_left (v : SpacetimeModel) : multiplication. -/ private theorem minkowskiForm_smul_left (r : ℝ) (a b : SpacetimeModel) : minkowskiForm (r • a) b = r * minkowskiForm a b := by - rw [map_smul, ContinuousLinearMap.smul_apply, smul_eq_mul] + rw [map_smul, smul_apply, smul_eq_mul] /-- Bilinearity of `minkowskiForm` in the right argument under scalar multiplication. -/ @@ -1111,7 +1111,7 @@ timelike future-oriented properties of `rep`) and pointwise applies `standardMinkowski_timelike_futurePointing_iff_mem_minkowskiForwardCone_zero`. -/ theorem standardMinkowski_trip_tangent_mem_minkowskiForwardCone_zero {p q : SpacetimeModel} {c : StandardMinkowskiSpacetime.SmoothCurve} - (htrip : Spacetime.IsTrip StandardMinkowskiSpacetime + (htrip : Spacetime.IsTripSegment StandardMinkowskiSpacetime standardMinkowskiTimeOrientation p q c) : ∃ (rep : StandardMinkowskiSpacetime.SmoothPath), c = Spacetime.SmoothCurve.ofPath StandardMinkowskiSpacetime rep ∧ @@ -1250,7 +1250,7 @@ The body wires together four named sub-lemmas: `standardMinkowski_smoothPath_tangent_continuousOn`. -/ theorem standardMinkowski_trip_displacement_eq_intervalIntegral {p q : SpacetimeModel} {c : StandardMinkowskiSpacetime.SmoothCurve} - (htrip : Spacetime.IsTrip StandardMinkowskiSpacetime + (htrip : Spacetime.IsTripSegment StandardMinkowskiSpacetime standardMinkowskiTimeOrientation p q c) : ∃ (rep : StandardMinkowskiSpacetime.SmoothPath) (a b : ℝ), a < b ∧ a ∈ rep.parameterSpace ∧ b ∈ rep.parameterSpace ∧ @@ -1377,7 +1377,7 @@ theorem intervalIntegral_mem_minkowskiForwardCone_zero have hT_apply : ∀ v : SpacetimeModel, T v = v - EuclideanSpace.single (0 : Fin 4) (v 0) := by intro v - simp only [hT_def, ContinuousLinearMap.sub_apply, ContinuousLinearMap.id_apply, + simp only [hT_def, sub_apply, ContinuousLinearMap.id_apply, ContinuousLinearMap.smulRight_apply, EuclideanSpace.coe_proj] -- (v 0) • single 0 1 = single 0 (v 0) congr 1 @@ -1518,16 +1518,15 @@ Minkowski-cone. The body wires together `intervalIntegral_mem_minkowskiForwardCone_zero`, and `mem_minkowskiForwardCone_iff_sub_mem`; the analytic content sits in those named lemmas. -/ -theorem chronologicalFuture_standardMinkowski_subset (p : SpacetimeModel) : - Spacetime.chronologicalFuture StandardMinkowskiSpacetime - standardMinkowskiTimeOrientation p - ⊆ minkowskiForwardCone p := by - intro q hq +theorem segmentPrecedes_mem_minkowskiForwardCone {p q : SpacetimeModel} + (hq : Spacetime.SegmentPrecedes StandardMinkowskiSpacetime + standardMinkowskiTimeOrientation p q) : + q ∈ minkowskiForwardCone p := by -- `StandardMinkowskiSpacetime.Carrier = SpacetimeModel` definitionally; we -- re-bind `q` at the model type so that arithmetic and cone membership -- elaborate cleanly. let q' : SpacetimeModel := q - -- Unpack the trip witness. + -- Unpack the segment witness. obtain ⟨c, htrip⟩ := hq -- FTC representation of `q' - p` as an interval integral of the trip's -- tangent. The lemma also delivers continuity of the tangent on `[a, b]` @@ -1548,16 +1547,63 @@ theorem chronologicalFuture_standardMinkowski_subset (p : SpacetimeModel) : change q' ∈ minkowskiForwardCone p exact (mem_minkowskiForwardCone_iff_sub_mem p q').mpr hsub +/-- *Forward subset* of `chronologicalFuture_standardMinkowski`: every +point in the chronological future of `p` lies in the open forward +Minkowski-cone. Because a trip is a finite chain of trip segments, this is a +transitive-closure induction: the base case is +`segmentPrecedes_mem_minkowskiForwardCone`, and the inductive step uses +forward-cone nesting `minkowskiForwardCone_subset`. -/ +theorem chronologicalFuture_standardMinkowski_subset (p : SpacetimeModel) : + Spacetime.chronologicalFuture StandardMinkowskiSpacetime + standardMinkowskiTimeOrientation p + ⊆ minkowskiForwardCone p := by + intro q hq + unfold Spacetime.chronologicalFuture at hq + simp only [Set.mem_setOf_eq, Spacetime.ChronologicallyPrecedes, Spacetime.IsTrip] at hq + induction hq with + | single h => + exact segmentPrecedes_mem_minkowskiForwardCone h + | tail h₁ h₂ ih => + rename_i b c + have hc_mem_b : (c : SpacetimeModel) ∈ minkowskiForwardCone (b : SpacetimeModel) := + segmentPrecedes_mem_minkowskiForwardCone h₂ + rcases ih with ⟨hp_b, hc_b⟩ + rcases hc_mem_b with ⟨hb_c, hc_c⟩ + have h_p_lt_c : p 0 < c.ofLp 0 := by + calc + p 0 < b.ofLp 0 := hp_b + _ < c.ofLp 0 := hb_c + have h_cone_add_aux : (c.ofLp 1 - p 1) ^ 2 + (c.ofLp 2 - p 2) ^ 2 + (c.ofLp 3 - p 3) ^ 2 + < (c.ofLp 0 - p 0) ^ 2 := by + set A := c.ofLp 0 - b.ofLp 0 with hA_def + set B := b.ofLp 0 - p 0 with hB_def + set x := c.ofLp 1 - b.ofLp 1 with hx_def + set y := c.ofLp 2 - b.ofLp 2 with hy_def + set z := c.ofLp 3 - b.ofLp 3 with hz_def + set u := b.ofLp 1 - p 1 with hu_def + set v := b.ofLp 2 - p 2 with hv_def + set w := b.ofLp 3 - p 3 with hw_def + have hA_pos : 0 < A := sub_pos.mpr hb_c + have hB_pos : 0 < B := sub_pos.mpr hp_b + have h1 : x^2 + y^2 + z^2 < A^2 := by linarith + have h2 : u^2 + v^2 + w^2 < B^2 := by linarith + have h_sum : (c.ofLp 0 - p 0) = A + B := by ring + have h_sum1 : c.ofLp 1 - p 1 = x + u := by ring + have h_sum2 : c.ofLp 2 - p 2 = y + v := by ring + have h_sum3 : c.ofLp 3 - p 3 = z + w := by ring + rw [h_sum, h_sum1, h_sum2, h_sum3] + nlinarith [sq_nonneg (A * u - B * x), sq_nonneg (A * v - B * y), + sq_nonneg (A * w - B * z), mul_pos hA_pos hB_pos, h1, h2] + refine ⟨h_p_lt_c, by nlinarith⟩ + /-- *Reverse subset* of `chronologicalFuture_standardMinkowski`: every point of the open forward Minkowski-cone of `p` lies in the chronological future of `p`. Witnessed by the straight-line path `standardMinkowskiLineSegmentPath`. -/ -theorem minkowskiForwardCone_subset_chronologicalFuture_standardMinkowski - (p : SpacetimeModel) : - minkowskiForwardCone p ⊆ - Spacetime.chronologicalFuture StandardMinkowskiSpacetime - standardMinkowskiTimeOrientation p := by - intro q hq +theorem minkowskiForwardCone_subset_segmentPrecedes {p q : SpacetimeModel} + (hq : q ∈ minkowskiForwardCone p) : + Spacetime.SegmentPrecedes StandardMinkowskiSpacetime + standardMinkowskiTimeOrientation p q := by obtain ⟨h_time, h_cone⟩ := hq have hpq : p ≠ q := by intro h @@ -1655,6 +1701,22 @@ theorem minkowskiForwardCone_subset_chronologicalFuture_standardMinkowski · intro s' hs' exact hs'.2 +/-- *Reverse subset* of `chronologicalFuture_standardMinkowski`: every point of +the open forward Minkowski-cone of `p` lies in the chronological future of `p`. +A single straight-line trip segment already realises the precedence, so this is +`Relation.TransGen.single` applied to `minkowskiForwardCone_subset_segmentPrecedes`. -/ +theorem minkowskiForwardCone_subset_chronologicalFuture_standardMinkowski + (p : SpacetimeModel) : + minkowskiForwardCone p ⊆ + Spacetime.chronologicalFuture StandardMinkowskiSpacetime + standardMinkowskiTimeOrientation p := by + intro q hq + -- Unfold `chronologicalFuture`, `ChronologicallyPrecedes`, `IsTrip`. + change Relation.TransGen + (Spacetime.SegmentPrecedes StandardMinkowskiSpacetime + standardMinkowskiTimeOrientation) p q + exact Relation.TransGen.single (minkowskiForwardCone_subset_segmentPrecedes hq) + /-- **Characterisation of `chronologicalFuture` on standard Minkowski.** The chronological future of `p` on `StandardMinkowskiSpacetime` agrees with the forward Minkowski-cone of `p`. This is the coordinate-explicit form of @@ -2026,4 +2088,99 @@ noncomputable def MinkowskiSpacetime : Spacetime where ((extChartAt _ x₀).map_source (mem_extChartAt_source x₀))] rfl +/-- **Part (i): existence of a chronological-future point (standard Minkowski).** +Every point `x` of standard Minkowski spacetime has a point strictly to its +chronological future; concretely `x + e₀` lies in the forward Minkowski cone of +`x`, since the connecting vector `e₀` is future-pointing timelike. -/ +theorem exists_chronologicalFuture_standardMinkowski (x : SpacetimeModel) : + ∃ b, b ∈ Spacetime.chronologicalFuture StandardMinkowskiSpacetime + standardMinkowskiTimeOrientation x := by + set b := x + EuclideanSpace.single (0 : Fin 4) (1 : ℝ) with hb + have single0 : (EuclideanSpace.single (0 : Fin 4) (1 : ℝ)) 0 = 1 := by + rw [PiLp.single_apply]; simp + have b0 : b 0 = x 0 + 1 := by + rw [hb, PiLp.add_apply, single0] + have b1 : b 1 = x 1 := by + rw [hb, PiLp.add_apply, PiLp.single_apply]; simp + have b2 : b 2 = x 2 := by + rw [hb, PiLp.add_apply, PiLp.single_apply]; simp + have b3 : b 3 = x 3 := by + rw [hb, PiLp.add_apply, PiLp.single_apply]; simp + refine ⟨b, ?_⟩ + rw [chronologicalFuture_standardMinkowski] + have hmem : b ∈ minkowskiForwardCone x := by + rw [mem_minkowskiForwardCone, b0, b1, b2, b3] + constructor + · nlinarith + · norm_num + exact hmem + +/-- **Part (i), dual: existence of a chronological-past point.** +Every point `x` of standard Minkowski spacetime has a point strictly to its +chronological past; concretely `x - e₀` lies in the backward Minkowski cone. -/ +theorem exists_chronologicalPast_standardMinkowski (x : SpacetimeModel) : + ∃ a, a ∈ Spacetime.chronologicalPast StandardMinkowskiSpacetime + standardMinkowskiTimeOrientation x := by + set a := x - EuclideanSpace.single (0 : Fin 4) (1 : ℝ) with ha + have single0 : (EuclideanSpace.single (0 : Fin 4) (1 : ℝ)) 0 = 1 := by + rw [PiLp.single_apply]; simp + have a0 : a 0 = x 0 - 1 := by + rw [ha, PiLp.sub_apply, single0] + have a1 : a 1 = x 1 := by + rw [ha, PiLp.sub_apply, PiLp.single_apply]; simp + have a2 : a 2 = x 2 := by + rw [ha, PiLp.sub_apply, PiLp.single_apply]; simp + have a3 : a 3 = x 3 := by + rw [ha, PiLp.sub_apply, PiLp.single_apply]; simp + refine ⟨a, ?_⟩ + rw [chronologicalPast_standardMinkowski] + have hmem : a ∈ minkowskiBackwardCone x := by + rw [mem_minkowskiBackwardCone, a0, a1, a2, a3] + constructor + · nlinarith + · norm_num + exact hmem + +/-- **Part (ii): Euclidean openness of the chronological future.** +On standard Minkowski spacetime `I⁺(p)` is open in the Euclidean (manifold) +topology on `ℝ⁴`; via the coordinate cone characterisation it coincides with the +forward Minkowski cone, which is open. -/ +theorem isOpen_chronologicalFuture_standardMinkowski (p : SpacetimeModel) : + IsOpen (Spacetime.chronologicalFuture StandardMinkowskiSpacetime + standardMinkowskiTimeOrientation p) := by + rw [chronologicalFuture_standardMinkowski] + exact isOpen_minkowskiForwardCone p + +/-- **Part (ii), dual: Euclidean openness of the chronological past.** -/ +theorem isOpen_chronologicalPast_standardMinkowski (q : SpacetimeModel) : + IsOpen (Spacetime.chronologicalPast StandardMinkowskiSpacetime + standardMinkowskiTimeOrientation q) := by + rw [chronologicalPast_standardMinkowski] + exact isOpen_minkowskiBackwardCone q + +/-- **Part (iii): unconditional Alexandrov openness of the chronological future.** +On standard Minkowski spacetime `I⁺(p)` is open in the Alexandrov topology, +unconditionally: the per-point hypothesis of the general lemma +`Spacetime.isOpen_chronologicalFuture` is discharged by part (i). -/ +theorem isOpen_alexandrov_chronologicalFuture_standardMinkowski (p : SpacetimeModel) : + @IsOpen _ (Spacetime.alexandrovTopology StandardMinkowskiSpacetime + standardMinkowskiTimeOrientation) + (Spacetime.chronologicalFuture StandardMinkowskiSpacetime + standardMinkowskiTimeOrientation p) := by + refine Spacetime.isOpen_chronologicalFuture StandardMinkowskiSpacetime + standardMinkowskiTimeOrientation p ?_ + intro x hx + exact exists_chronologicalFuture_standardMinkowski x + +/-- **Part (iii), dual: unconditional Alexandrov openness of the chronological past.** -/ +theorem isOpen_alexandrov_chronologicalPast_standardMinkowski (q : SpacetimeModel) : + @IsOpen _ (Spacetime.alexandrovTopology StandardMinkowskiSpacetime + standardMinkowskiTimeOrientation) + (Spacetime.chronologicalPast StandardMinkowskiSpacetime + standardMinkowskiTimeOrientation q) := by + refine Spacetime.isOpen_chronologicalPast StandardMinkowskiSpacetime + standardMinkowskiTimeOrientation q ?_ + intro x hx + exact exists_chronologicalPast_standardMinkowski x + end Physicslib4 diff --git a/Physicslib4/Spacetime/MinkowskiDirected.lean b/Physicslib4/Spacetime/MinkowskiDirected.lean index 2d984c3..5f35383 100644 --- a/Physicslib4/Spacetime/MinkowskiDirected.lean +++ b/Physicslib4/Spacetime/MinkowskiDirected.lean @@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Lean Community -/ import Physicslib4.Spacetime.Minkowski +import Mathlib.Topology.Bases /-! # Directedness of the Alexandrov basis of standard Minkowski spacetime @@ -154,5 +155,327 @@ theorem alexandrovBasis_directed {B₁ B₂ : Set SpacetimeModel} chronologicalPast_standardMinkowski] at hx ⊢ exact ⟨minkowskiForwardCone_subset hp2 hx.1, minkowskiBackwardCone_subset hq2 hx.2⟩ +/-! ### The Alexandrov diamonds form a genuine topological basis on standard Minkowski -/ + +/-- **Past interpolation.** If `x` is in the forward cones of `p₁` and `p₂`, there is +a point `a` in both forward cones with `x` in the forward cone of `a` (i.e. +`p₁, p₂ ≪ a ≪ x`). Take `a = x - ε • e₀` for small `ε > 0`: the spatial separation +from each `pᵢ` is unchanged, so the timelike condition survives, and `x - a = ε e₀` is +future-timelike. -/ +theorem exists_past_between_standardMinkowski {p₁ p₂ x : SpacetimeModel} + (h₁ : x ∈ minkowskiForwardCone p₁) (h₂ : x ∈ minkowskiForwardCone p₂) : + ∃ a, a ∈ minkowskiForwardCone p₁ ∧ a ∈ minkowskiForwardCone p₂ ∧ + x ∈ minkowskiForwardCone a := by + obtain ⟨h₁0, h₁c⟩ := h₁ + obtain ⟨h₂0, h₂c⟩ := h₂ + set T₁ := x 0 - p₁ 0 with hT₁ + set T₂ := x 0 - p₂ 0 with hT₂ + set S₁ := (x 1 - p₁ 1)^2 + (x 2 - p₁ 2)^2 + (x 3 - p₁ 3)^2 with hS₁ + set S₂ := (x 1 - p₂ 1)^2 + (x 2 - p₂ 2)^2 + (x 3 - p₂ 3)^2 with hS₂ + have hT₁pos : 0 < T₁ := sub_pos.mpr h₁0 + have hT₂pos : 0 < T₂ := sub_pos.mpr h₂0 + have hS₁ltT₁sq : S₁ < T₁ ^ 2 := by + dsimp [S₁, T₁] at h₁c ⊢ + linarith + have hS₂ltT₂sq : S₂ < T₂ ^ 2 := by + dsimp [S₂, T₂] at h₂c ⊢ + linarith + set δ₁ := T₁ ^ 2 - S₁ with hδ₁ + set δ₂ := T₂ ^ 2 - S₂ with hδ₂ + have hδ₁pos : 0 < δ₁ := by rw [hδ₁]; linarith + have hδ₂pos : 0 < δ₂ := by rw [hδ₂]; linarith + have hS₁_nonneg : 0 ≤ S₁ := by rw [hS₁]; positivity + have hS₂_nonneg : 0 ≤ S₂ := by rw [hS₂]; positivity + have hδ₁leT₁sq : δ₁ ≤ T₁ ^ 2 := by rw [hδ₁]; linarith + have hδ₂leT₂sq : δ₂ ≤ T₂ ^ 2 := by rw [hδ₂]; linarith + have hδ₁_div_pos : 0 < δ₁ / (2 * T₁) := div_pos hδ₁pos (by positivity) + have hδ₂_div_pos : 0 < δ₂ / (2 * T₂) := div_pos hδ₂pos (by positivity) + set ε := min (δ₁ / (2 * T₁)) (δ₂ / (2 * T₂)) with hε + have hεpos : 0 < ε := by + rw [hε] + exact lt_min_iff.mpr ⟨hδ₁_div_pos, hδ₂_div_pos⟩ + have hε_le_δ₁_div : ε ≤ δ₁ / (2 * T₁) := by + rw [hε]; exact min_le_left _ _ + have hε_le_δ₂_div : ε ≤ δ₂ / (2 * T₂) := by + rw [hε]; exact min_le_right _ _ + have hε_mul₁ : 2 * T₁ * ε ≤ δ₁ := by + have hpos : 0 < 2 * T₁ := by positivity + calc + 2 * T₁ * ε ≤ 2 * T₁ * (δ₁ / (2 * T₁)) := + mul_le_mul_of_nonneg_left hε_le_δ₁_div (by positivity) + _ = δ₁ := by field_simp [hpos.ne.symm] + have hε_mul₂ : 2 * T₂ * ε ≤ δ₂ := by + have hpos : 0 < 2 * T₂ := by positivity + calc + 2 * T₂ * ε ≤ 2 * T₂ * (δ₂ / (2 * T₂)) := + mul_le_mul_of_nonneg_left hε_le_δ₂_div (by positivity) + _ = δ₂ := by field_simp [hpos.ne.symm] + have hε_lt_T₁ : ε < T₁ := by + by_contra! h + have h2T₁ε_ge_2T₁sq : 2 * T₁ * ε ≥ 2 * T₁ ^ 2 := by + calc + 2 * T₁ * ε ≥ 2 * T₁ * T₁ := mul_le_mul_of_nonneg_left h (by positivity) + _ = 2 * T₁ ^ 2 := by ring + have hchain : 2 * T₁ ^ 2 ≤ T₁ ^ 2 := by + calc + 2 * T₁ ^ 2 ≤ 2 * T₁ * ε := h2T₁ε_ge_2T₁sq + _ ≤ δ₁ := hε_mul₁ + _ ≤ T₁ ^ 2 := hδ₁leT₁sq + have hpos : T₁ ^ 2 > 0 := pow_pos hT₁pos 2 + linarith + have hε_lt_T₂ : ε < T₂ := by + by_contra! h + have h2T₂ε_ge_2T₂sq : 2 * T₂ * ε ≥ 2 * T₂ ^ 2 := by + calc + 2 * T₂ * ε ≥ 2 * T₂ * T₂ := mul_le_mul_of_nonneg_left h (by positivity) + _ = 2 * T₂ ^ 2 := by ring + have hchain : 2 * T₂ ^ 2 ≤ T₂ ^ 2 := by + calc + 2 * T₂ ^ 2 ≤ 2 * T₂ * ε := h2T₂ε_ge_2T₂sq + _ ≤ δ₂ := hε_mul₂ + _ ≤ T₂ ^ 2 := hδ₂leT₂sq + have hpos : T₂ ^ 2 > 0 := pow_pos hT₂pos 2 + linarith + have hcone_ineq₁ : S₁ < (T₁ - ε) ^ 2 := by + have hsqpos : 0 < ε ^ 2 := pow_pos hεpos 2 + have hsub : 2 * T₁ * ε - ε ^ 2 < δ₁ := by + have htemp : 2 * T₁ * ε - ε ^ 2 < 2 * T₁ * ε := by linarith + exact htemp.trans_le hε_mul₁ + have eqn : (T₁ - ε) ^ 2 - S₁ = δ₁ - (2 * T₁ * ε - ε ^ 2) := by + rw [hδ₁]; ring + linarith + have hcone_ineq₂ : S₂ < (T₂ - ε) ^ 2 := by + have hsqpos : 0 < ε ^ 2 := pow_pos hεpos 2 + have hsub : 2 * T₂ * ε - ε ^ 2 < δ₂ := by + have htemp : 2 * T₂ * ε - ε ^ 2 < 2 * T₂ * ε := by linarith + exact htemp.trans_le hε_mul₂ + have eqn : (T₂ - ε) ^ 2 - S₂ = δ₂ - (2 * T₂ * ε - ε ^ 2) := by + rw [hδ₂]; ring + linarith + set a : SpacetimeModel := x - EuclideanSpace.single (0 : Fin 4) ε with ha + have ha0 : a 0 = x 0 - ε := by + rw [ha, PiLp.sub_apply, PiLp.single_apply, if_pos rfl] + have ha1 : a 1 = x 1 := by + rw [ha, PiLp.sub_apply, PiLp.single_apply, if_neg (by decide)] + simp + have ha2 : a 2 = x 2 := by + rw [ha, PiLp.sub_apply, PiLp.single_apply, if_neg (by decide)] + simp + have ha3 : a 3 = x 3 := by + rw [ha, PiLp.sub_apply, PiLp.single_apply, if_neg (by decide)] + simp + refine ⟨a, ?_, ?_, ?_⟩ + · -- a ∈ minkowskiForwardCone p₁ + rw [mem_minkowskiForwardCone, ha0, ha1, ha2, ha3] + dsimp [T₁, S₁] + constructor + · linarith + · linarith + · -- a ∈ minkowskiForwardCone p₂ + rw [mem_minkowskiForwardCone, ha0, ha1, ha2, ha3] + dsimp [T₂, S₂] + constructor + · linarith + · linarith + · -- x ∈ minkowskiForwardCone a + rw [mem_minkowskiForwardCone, ha0, ha1, ha2, ha3] + constructor + · linarith + · have : 0 < ε ^ 2 := pow_pos hεpos 2 + linarith + +/-- **Future interpolation.** If `x` is in the backward cones of `q₁` and `q₂`, there +is a point `b` in both backward cones with `x` in the backward cone of `b` (i.e. +`x ≪ b ≪ q₁, q₂`). Dual to `exists_past_between_standardMinkowski`, with `b = x + ε • e₀`. -/ +theorem exists_future_between_standardMinkowski {q₁ q₂ x : SpacetimeModel} + (h₁ : x ∈ minkowskiBackwardCone q₁) (h₂ : x ∈ minkowskiBackwardCone q₂) : + ∃ b, b ∈ minkowskiBackwardCone q₁ ∧ b ∈ minkowskiBackwardCone q₂ ∧ + x ∈ minkowskiBackwardCone b := by + obtain ⟨h₁0, h₁c⟩ := h₁ + obtain ⟨h₂0, h₂c⟩ := h₂ + set T₁ := q₁ 0 - x 0 with hT₁ + set T₂ := q₂ 0 - x 0 with hT₂ + set S₁ := (q₁ 1 - x 1)^2 + (q₁ 2 - x 2)^2 + (q₁ 3 - x 3)^2 with hS₁ + set S₂ := (q₂ 1 - x 1)^2 + (q₂ 2 - x 2)^2 + (q₂ 3 - x 3)^2 with hS₂ + have hT₁pos : 0 < T₁ := sub_pos.mpr h₁0 + have hT₂pos : 0 < T₂ := sub_pos.mpr h₂0 + have hS₁ltT₁sq : S₁ < T₁ ^ 2 := by + dsimp [S₁, T₁] at h₁c ⊢ + linarith + have hS₂ltT₂sq : S₂ < T₂ ^ 2 := by + dsimp [S₂, T₂] at h₂c ⊢ + linarith + set δ₁ := T₁ ^ 2 - S₁ with hδ₁ + set δ₂ := T₂ ^ 2 - S₂ with hδ₂ + have hδ₁pos : 0 < δ₁ := by rw [hδ₁]; linarith + have hδ₂pos : 0 < δ₂ := by rw [hδ₂]; linarith + have hS₁_nonneg : 0 ≤ S₁ := by rw [hS₁]; positivity + have hS₂_nonneg : 0 ≤ S₂ := by rw [hS₂]; positivity + have hδ₁leT₁sq : δ₁ ≤ T₁ ^ 2 := by rw [hδ₁]; linarith + have hδ₂leT₂sq : δ₂ ≤ T₂ ^ 2 := by rw [hδ₂]; linarith + have hδ₁_div_pos : 0 < δ₁ / (2 * T₁) := div_pos hδ₁pos (by positivity) + have hδ₂_div_pos : 0 < δ₂ / (2 * T₂) := div_pos hδ₂pos (by positivity) + set ε := min (δ₁ / (2 * T₁)) (δ₂ / (2 * T₂)) with hε + have hεpos : 0 < ε := by + rw [hε] + exact lt_min_iff.mpr ⟨hδ₁_div_pos, hδ₂_div_pos⟩ + have hε_le_δ₁_div : ε ≤ δ₁ / (2 * T₁) := by + rw [hε]; exact min_le_left _ _ + have hε_le_δ₂_div : ε ≤ δ₂ / (2 * T₂) := by + rw [hε]; exact min_le_right _ _ + have hε_mul₁ : 2 * T₁ * ε ≤ δ₁ := by + have hpos : 0 < 2 * T₁ := by positivity + calc + 2 * T₁ * ε ≤ 2 * T₁ * (δ₁ / (2 * T₁)) := + mul_le_mul_of_nonneg_left hε_le_δ₁_div (by positivity) + _ = δ₁ := by field_simp [hpos.ne.symm] + have hε_mul₂ : 2 * T₂ * ε ≤ δ₂ := by + have hpos : 0 < 2 * T₂ := by positivity + calc + 2 * T₂ * ε ≤ 2 * T₂ * (δ₂ / (2 * T₂)) := + mul_le_mul_of_nonneg_left hε_le_δ₂_div (by positivity) + _ = δ₂ := by field_simp [hpos.ne.symm] + have hε_lt_T₁ : ε < T₁ := by + by_contra! h + have h2T₁ε_ge_2T₁sq : 2 * T₁ * ε ≥ 2 * T₁ ^ 2 := by + calc + 2 * T₁ * ε ≥ 2 * T₁ * T₁ := mul_le_mul_of_nonneg_left h (by positivity) + _ = 2 * T₁ ^ 2 := by ring + have hchain : 2 * T₁ ^ 2 ≤ T₁ ^ 2 := by + calc + 2 * T₁ ^ 2 ≤ 2 * T₁ * ε := h2T₁ε_ge_2T₁sq + _ ≤ δ₁ := hε_mul₁ + _ ≤ T₁ ^ 2 := hδ₁leT₁sq + have hpos : T₁ ^ 2 > 0 := pow_pos hT₁pos 2 + linarith + have hε_lt_T₂ : ε < T₂ := by + by_contra! h + have h2T₂ε_ge_2T₂sq : 2 * T₂ * ε ≥ 2 * T₂ ^ 2 := by + calc + 2 * T₂ * ε ≥ 2 * T₂ * T₂ := mul_le_mul_of_nonneg_left h (by positivity) + _ = 2 * T₂ ^ 2 := by ring + have hchain : 2 * T₂ ^ 2 ≤ T₂ ^ 2 := by + calc + 2 * T₂ ^ 2 ≤ 2 * T₂ * ε := h2T₂ε_ge_2T₂sq + _ ≤ δ₂ := hε_mul₂ + _ ≤ T₂ ^ 2 := hδ₂leT₂sq + have hpos : T₂ ^ 2 > 0 := pow_pos hT₂pos 2 + linarith + have hcone_ineq₁ : S₁ < (T₁ - ε) ^ 2 := by + have hsqpos : 0 < ε ^ 2 := pow_pos hεpos 2 + have hsub : 2 * T₁ * ε - ε ^ 2 < δ₁ := by + have htemp : 2 * T₁ * ε - ε ^ 2 < 2 * T₁ * ε := by linarith + exact htemp.trans_le hε_mul₁ + have eqn : (T₁ - ε) ^ 2 - S₁ = δ₁ - (2 * T₁ * ε - ε ^ 2) := by + rw [hδ₁]; ring + linarith + have hcone_ineq₂ : S₂ < (T₂ - ε) ^ 2 := by + have hsqpos : 0 < ε ^ 2 := pow_pos hεpos 2 + have hsub : 2 * T₂ * ε - ε ^ 2 < δ₂ := by + have htemp : 2 * T₂ * ε - ε ^ 2 < 2 * T₂ * ε := by linarith + exact htemp.trans_le hε_mul₂ + have eqn : (T₂ - ε) ^ 2 - S₂ = δ₂ - (2 * T₂ * ε - ε ^ 2) := by + rw [hδ₂]; ring + linarith + set b : SpacetimeModel := x + EuclideanSpace.single (0 : Fin 4) ε with hb + have hb0 : b 0 = x 0 + ε := by + rw [hb, PiLp.add_apply, PiLp.single_apply, if_pos rfl] + have hb1 : b 1 = x 1 := by + rw [hb, PiLp.add_apply, PiLp.single_apply, if_neg (by decide)] + simp + have hb2 : b 2 = x 2 := by + rw [hb, PiLp.add_apply, PiLp.single_apply, if_neg (by decide)] + simp + have hb3 : b 3 = x 3 := by + rw [hb, PiLp.add_apply, PiLp.single_apply, if_neg (by decide)] + simp + refine ⟨b, ?_, ?_, ?_⟩ + · -- b ∈ minkowskiBackwardCone q₁ + rw [mem_minkowskiBackwardCone, hb0, hb1, hb2, hb3] + dsimp [T₁, S₁] + constructor + · linarith + · linarith + · -- b ∈ minkowskiBackwardCone q₂ + rw [mem_minkowskiBackwardCone, hb0, hb1, hb2, hb3] + dsimp [T₂, S₂] + constructor + · linarith + · linarith + · -- x ∈ minkowskiBackwardCone b + rw [mem_minkowskiBackwardCone, hb0, hb1, hb2, hb3] + constructor + · linarith + · have : 0 < ε ^ 2 := pow_pos hεpos 2 + linarith + +/-- **Downward intersection property of the diamonds.** For two Alexandrov diamonds of +standard Minkowski and a point `x` in their intersection, there is a diamond `B₃` with +`x ∈ B₃ ⊆ B₁ ∩ B₂`. Uses past/future interpolation to build `B₃ = I⁺(a) ∩ I⁻(b)` and +cone-nesting for the containment. -/ +theorem alexandrovBasis_exists_subset_inter_standardMinkowski + (B₁ : Set SpacetimeModel) + (h₁ : B₁ ∈ alexandrovBasis StandardMinkowskiSpacetime standardMinkowskiTimeOrientation) + (B₂ : Set SpacetimeModel) + (h₂ : B₂ ∈ alexandrovBasis StandardMinkowskiSpacetime standardMinkowskiTimeOrientation) + (x : SpacetimeModel) (hx : x ∈ B₁ ∩ B₂) : + ∃ B₃ ∈ alexandrovBasis StandardMinkowskiSpacetime standardMinkowskiTimeOrientation, + x ∈ B₃ ∧ B₃ ⊆ B₁ ∩ B₂ := by + obtain ⟨p₁, q₁, rfl⟩ := h₁ + obtain ⟨p₂, q₂, rfl⟩ := h₂ + simp only [chronologicalFuture_standardMinkowski, chronologicalPast_standardMinkowski] at hx + obtain ⟨⟨hxp1, hxq1⟩, ⟨hxp2, hxq2⟩⟩ := hx + obtain ⟨a, ha1, ha2, hax⟩ := exists_past_between_standardMinkowski hxp1 hxp2 + obtain ⟨b, hb1, hb2, hxb⟩ := exists_future_between_standardMinkowski hxq1 hxq2 + refine ⟨(chronologicalFuture StandardMinkowskiSpacetime standardMinkowskiTimeOrientation a ∩ + chronologicalPast StandardMinkowskiSpacetime standardMinkowskiTimeOrientation b), + ⟨a, b, rfl⟩, ?_, ?_⟩ + · simp only [chronologicalFuture_standardMinkowski, chronologicalPast_standardMinkowski] + exact ⟨hax, hxb⟩ + · intro y hy + simp only [chronologicalFuture_standardMinkowski, chronologicalPast_standardMinkowski] at hy ⊢ + obtain ⟨hyf, hyb⟩ := hy + refine ⟨⟨?_, ?_⟩, ⟨?_, ?_⟩⟩ + · exact minkowskiForwardCone_subset ha1 hyf + · exact minkowskiBackwardCone_subset hb1 hyb + · exact minkowskiForwardCone_subset ha2 hyf + · exact minkowskiBackwardCone_subset hb2 hyb + +/-- **The Alexandrov diamonds are a topological basis on standard Minkowski.** +Unconditionally: covering holds because every point has a chronological past and +future point, and the downward intersection property is +`alexandrovBasis_exists_subset_inter_standardMinkowski`; the generation condition is +definitional. -/ +theorem isTopologicalBasis_alexandrovBasis_standardMinkowski : + @TopologicalSpace.IsTopologicalBasis SpacetimeModel + (alexandrovTopology StandardMinkowskiSpacetime standardMinkowskiTimeOrientation) + (alexandrovBasis StandardMinkowskiSpacetime standardMinkowskiTimeOrientation) := by + have h1 : ∀ t₁ ∈ alexandrovBasis StandardMinkowskiSpacetime + standardMinkowskiTimeOrientation, + ∀ t₂ ∈ alexandrovBasis StandardMinkowskiSpacetime standardMinkowskiTimeOrientation, + ∀ x ∈ t₁ ∩ t₂, ∃ t₃ ∈ alexandrovBasis StandardMinkowskiSpacetime + standardMinkowskiTimeOrientation, + x ∈ t₃ ∧ t₃ ⊆ t₁ ∩ t₂ := + alexandrovBasis_exists_subset_inter_standardMinkowski + have h2 : ⋃₀ (alexandrovBasis StandardMinkowskiSpacetime + standardMinkowskiTimeOrientation) = Set.univ := by + apply Set.sUnion_eq_univ_iff.mpr + intro x + rcases exists_chronologicalPast_standardMinkowski x with ⟨a, ha⟩ + rcases exists_chronologicalFuture_standardMinkowski x with ⟨b, hb⟩ + refine ⟨chronologicalFuture StandardMinkowskiSpacetime standardMinkowskiTimeOrientation a ∩ + chronologicalPast StandardMinkowskiSpacetime standardMinkowskiTimeOrientation b, ?_, ?_⟩ + · exact ⟨a, b, rfl⟩ + · exact ⟨by + simpa [chronologicalFuture, chronologicalPast] using ha, + by + simpa [chronologicalPast, chronologicalFuture] using hb⟩ + have h3 : alexandrovTopology StandardMinkowskiSpacetime standardMinkowskiTimeOrientation = + TopologicalSpace.generateFrom + (alexandrovBasis StandardMinkowskiSpacetime standardMinkowskiTimeOrientation) := rfl + exact @TopologicalSpace.IsTopologicalBasis.mk SpacetimeModel + (alexandrovTopology StandardMinkowskiSpacetime standardMinkowskiTimeOrientation) + (alexandrovBasis StandardMinkowskiSpacetime standardMinkowskiTimeOrientation) h1 h2 h3 + end Spacetime end Physicslib4 diff --git a/blueprint/src/sections/sec10/10-2_spacetime.tex b/blueprint/src/sections/sec10/10-2_spacetime.tex index fae87aa..bcde896 100644 --- a/blueprint/src/sections/sec10/10-2_spacetime.tex +++ b/blueprint/src/sections/sec10/10-2_spacetime.tex @@ -228,22 +228,52 @@ \section{Spacetime}\label{sctn:spacetime} \begin{definition}[Trip] \label{def:trip} - \lean{Physicslib4.Spacetime.IsTrip, Physicslib4.Spacetime.ChronologicallyPrecedes} + \lean{Physicslib4.Spacetime.IsTripSegment, Physicslib4.Spacetime.IsTrip, Physicslib4.Spacetime.ChronologicallyPrecedes} \leanfile{Physicslib4/Spacetime/Causality.lean} \leanok \uses{def:curves, def:future-and-past-oriented-smooth-curves, def:timelike-and-causal-smooth-curves, def:endpoints} - A \textit{trip} is a curve which is piecewise a future-oriented, timelike geodesic. A trip \textit{from} $p$ to $q$ is a trip with past endpoint $p$ and future endpoint $q$. We write $p \ll q$ if and only if there exists a trip from $p$ to $q$. + A \textit{trip segment} is a curve which is a future-oriented, timelike geodesic. A \textit{trip} is a curve which is \emph{piecewise} a future-oriented, timelike geodesic: a finite chain of trip segments $p = x_0, x_1, \dots, x_n = q$ joined at matching endpoints. Formally this is the transitive closure of single-segment precedence, which is what makes the relation transitive by concatenation. A trip \textit{from} $p$ to $q$ is a trip with past endpoint $p$ and future endpoint $q$. We write $p \ll q$ if and only if there exists a trip from $p$ to $q$. \end{definition} \begin{definition}[Causal Trip] \label{def:causal-trip} - \lean{Physicslib4.Spacetime.IsCausalTrip, Physicslib4.Spacetime.CausallyPrecedes} + \lean{Physicslib4.Spacetime.IsCausalTripSegment, Physicslib4.Spacetime.IsCausalTrip, Physicslib4.Spacetime.CausallyPrecedes} \leanfile{Physicslib4/Spacetime/Causality.lean} \leanok \uses{def:curves, def:future-and-past-oriented-smooth-curves, def:timelike-and-causal-smooth-curves, def:endpoints} - A \textit{causal trip} is a curve which is piecewise a future-oriented, causal geodesic. (Note a causal geodesic is possibly degenerate.) A causal trip \textit{from} $p$ to $q$ is a causal trip with past endpoint $p$ and future endpoint $q$. We write $p \prec q$ if and only if there exists a causal trip from $p$ to $q$. + A \textit{causal trip segment} is a curve which is a future-oriented, causal geodesic. (Note a causal geodesic is possibly degenerate.) A \textit{causal trip} is a curve which is piecewise a future-oriented, causal geodesic: a finite chain of causal trip segments joined at matching endpoints. A causal trip \textit{from} $p$ to $q$ is a causal trip with past endpoint $p$ and future endpoint $q$. We write $p \prec q$ if and only if there exists a causal trip from $p$ to $q$. \end{definition} +\medskip +\noindent\textbf{Remark (geodesic placeholder in the formalization).} In the Lean formalization the ``geodesic'' clause of a (causal) trip segment is currently a \emph{placeholder}: the predicate \texttt{Physicslib4.Spacetime.IsGeodesic} is defined to be \texttt{True}, so it imposes no constraint. A faithful geodesic condition requires the Levi-Civita connection of the metric (auto-parallelism of the tangent vector along the curve), which the version of Mathlib pinned by this project does not provide. Consequently the formalized (causal) trip segments are future-oriented timelike (resp. causal) curves with the correct past and future endpoints, but their geodesic property is not yet enforced; the endpoint, timelike/causal, and future-orientation content is faithful. This is the one place where \ref{def:trip} and \ref{def:causal-trip} diverge from their Lean implementations, and it should be replaced by the genuine geodesic condition once a Lorentzian Levi-Civita connection is available in Mathlib. + +\begin{theorem}[Transitivity of chronological and causal precedence] + \label{thrm:precedence-transitive} + \lean{Physicslib4.Spacetime.chronologicallyPrecedes_trans, Physicslib4.Spacetime.causallyPrecedes_trans} + \leanfile{Physicslib4/Spacetime/Causality.lean} + \leanok + \uses{def:trip, def:causal-trip} + Chronological precedence $\ll$ and causal precedence $\prec$ are transitive: if $p \ll q$ and $q \ll r$ then $p \ll r$, and likewise for $\prec$. Two trips joined at the common point $q$ concatenate to a single piecewise trip; this is exactly the transitivity of the transitive closure. +\end{theorem} + +\begin{definition}[No Closed Causal Curve (Causality Condition)] + \label{def:no-closed-causal-curve} + \lean{Physicslib4.Spacetime.NoClosedCausalCurve} + \leanfile{Physicslib4/Spacetime/Causality.lean} + \leanok + \uses{def:causal-trip} + A spacetime $M$ with time orientation $t$ satisfies the \emph{causality condition} --- equivalently, has \emph{no closed causal curve} --- when no point causally precedes itself: $\lnot(p \prec p)$ for every $p$. A closed causal curve through $p$ would be a causal trip from $p$ back to $p$, i.e.\ $p \prec p$, so its absence is exactly this condition. This is the standard causality condition, strictly weaker than strong causality and strictly stronger than the chronology condition ($\lnot(p \ll p)$ for all $p$). +\end{definition} + +\begin{theorem}[Irreflexivity and Antisymmetry under Causality] + \label{thrm:causal-order-refinements} + \lean{Physicslib4.Spacetime.chronologicallyPrecedes_irrefl, Physicslib4.Spacetime.causallyPrecedes_asymm, Physicslib4.Spacetime.causallyPrecedes_antisymm} + \leanfile{Physicslib4/Spacetime/Causality.lean} + \uses{def:no-closed-causal-curve, thrm:precedence-transitive, lmm:chronological-implies-causal} + \leanok + Assume $M$ has no closed causal curve. Then chronological precedence is irreflexive, $\lnot(p \ll p)$ for every $p$ (since $p \ll p$ would give $p \prec p$ because chronological precedence implies causal precedence), and causal precedence is asymmetric and antisymmetric: $p \prec q$ excludes $q \prec p$, and $p \prec q$ together with $q \prec p$ forces $p = q$ (indeed both cannot hold, since transitivity would give the forbidden $p \prec p$). Thus, under the causality condition, $\prec$ is a strict partial order on the events of the spacetime. +\end{theorem} + \begin{definition}[Chronological Future and Chronological Past] \label{def:chronological-future-and-chronological-past} \lean{Physicslib4.Spacetime.chronologicalFuture, Physicslib4.Spacetime.chronologicalPast, Physicslib4.Spacetime.chronologicalFutureSet, Physicslib4.Spacetime.chronologicalPastSet} @@ -346,6 +376,113 @@ \section{Spacetime}\label{sctn:spacetime} Each follows directly from the pointwise definition: monotonicity by restricting the universally-quantified points, the empty cases vacuously, and the union cases by splitting the membership disjunction. \end{proof} +\begin{definition}[Spacelike Complement of a Region] + \label{def:spacelike-complement} + \lean{Physicslib4.Spacetime.LorentzianSpacetime.spacelikeComplement} + \leanfile{Physicslib4/Spacetime/CausalComplement.lean} + \leanok + \uses{def:completely-spacelike, def:lorentzian-spacetime} + The \emph{spacelike complement} $\mathbf{B}^\perp$ of a region $\mathbf{B}$ is the set of points completely spacelike-separated from all of $\mathbf{B}$: $\mathbf{B}^\perp = \{ x \mid \{x\} \text{ is completely spacelike to } \mathbf{B} \}$. It is the geometric substrate of locality and Haag duality. +\end{definition} + +\begin{lemma}[Order Structure of the Spacelike Complement] + \label{lmm:spacelike-complement-order} + \lean{Physicslib4.Spacetime.LorentzianSpacetime.spacelikeComplement_antitone, Physicslib4.Spacetime.LorentzianSpacetime.subset_spacelikeComplement_spacelikeComplement, Physicslib4.Spacetime.LorentzianSpacetime.spacelikeComplement_spacelikeComplement_spacelikeComplement, Physicslib4.Spacetime.LorentzianSpacetime.subset_spacelikeComplement_iff} + \leanfile{Physicslib4/Spacetime/CausalComplement.lean} + \leanok + \uses{def:spacelike-complement, lmm:completely-spacelike-symm, lmm:completely-spacelike-structural} + The spacelike complement is antitone ($\mathbf{B}_1 \subseteq \mathbf{B}_2 \Rightarrow \mathbf{B}_2^\perp \subseteq \mathbf{B}_1^\perp$), a region is contained in its double complement ($\mathbf{B} \subseteq \mathbf{B}^{\perp\perp}$), and the triple complement collapses ($\mathbf{B}^{\perp\perp\perp} = \mathbf{B}^\perp$). Moreover $\mathbf{B}_1 \subseteq \mathbf{B}_2^\perp$ if and only if $\mathbf{B}_1$ and $\mathbf{B}_2$ are completely spacelike-separated, so complementation is the Galois connection attached to the spacelike-separation relation. +\end{lemma} +\begin{proof} + \leanok + Antitonicity and the Galois bridge are the pointwise monotonicity of complete spacelike separation; the double-complement inclusion follows by symmetry of the relation; and the triple-complement identity is the standard consequence of antitonicity together with the double-complement inclusion. +\end{proof} + +\begin{definition}[Causal closure operator] + \label{def:causal-closure} + \lean{Physicslib4.Spacetime.LorentzianSpacetime.causalClosure} + \leanfile{Physicslib4/Spacetime/CausalComplement.lean} + \leanok + \uses{def:spacelike-complement, lmm:spacelike-complement-order} + The double spacelike complement $\mathbf{B} \mapsto \mathbf{B}^{\perp\perp}$ is a \emph{closure operator} on the regions of a Lorentzian spacetime: it is monotone, extensive ($\mathbf{B} \subseteq \mathbf{B}^{\perp\perp}$), and idempotent ($\mathbf{B}^{\perp\perp\perp\perp} = \mathbf{B}^{\perp\perp}$). Its three defining properties are exactly the order structure of the spacelike complement. +\end{definition} + +\begin{definition}[Causally complete region] + \label{def:causally-complete-region} + \lean{Physicslib4.Spacetime.LorentzianSpacetime.IsCausallyComplete} + \leanfile{Physicslib4/Spacetime/CausalComplement.lean} + \leanok + \uses{def:causal-closure} + A region is \emph{causally complete} if it equals its own double complement, $\mathbf{B}^{\perp\perp} = \mathbf{B}$ (a fixed point of the causal closure operator). These are the regions on which algebraic QFT is naturally indexed. +\end{definition} + +\begin{theorem}[Lattice of causally complete regions] + \label{thrm:causally-complete-lattice} + \lean{Physicslib4.Spacetime.LorentzianSpacetime.causalComplement_causalComplement} + \leanfile{Physicslib4/Spacetime/CausalComplement.lean} + \leanok + \uses{def:causally-complete-region} + The causally complete regions form a \emph{complete lattice} (meets are intersections, joins are causal closures of unions), obtained from the causal closure operator via its Galois insertion. The spacelike complement of any region is causally complete, causally complete regions are closed under intersection, and the causal complement $\mathbf{B} \mapsto \mathbf{B}^\perp$ is an \emph{order-reversing involution} on this lattice ($\mathbf{B}^{\perp\perp} = \mathbf{B}$). (The full orthocomplement law $\mathbf{B} \wedge \mathbf{B}^\perp = \bot$ does not hold at this generality, because the trip-based causal relation is irreflexive, so a point is spacelike-separated from itself; what holds is the complete lattice with an order-reversing De~Morgan involution.) +\end{theorem} + +\begin{lemma}[De Morgan Laws for the Spacelike Complement] + \label{lmm:spacelike-complement-de-morgan} + \lean{Physicslib4.Spacetime.LorentzianSpacetime.spacelikeComplement_union, Physicslib4.Spacetime.LorentzianSpacetime.spacelikeComplement_iUnion} + \leanfile{Physicslib4/Spacetime/CausalComplement.lean} + \uses{def:spacelike-complement, lmm:completely-spacelike-structural} + \leanok + At the level of the underlying sets, the spacelike complement turns unions into intersections. In binary form, for regions $\mathbf{B}_1, \mathbf{B}_2$, + \begin{align} + (\mathbf{B}_1 \cup \mathbf{B}_2)^\perp = \mathbf{B}_1^\perp \cap \mathbf{B}_2^\perp, + \end{align} + and, for an arbitrary indexed family $(\mathbf{B}_i)_{i \in I}$, + \begin{align} + \Bigl(\bigcup_{i \in I} \mathbf{B}_i\Bigr)^\perp = \bigcap_{i \in I} \mathbf{B}_i^\perp. + \end{align} +\end{lemma} +\begin{proof} + \leanok + \uses{def:spacelike-complement, lmm:completely-spacelike-structural} + Unfold the spacelike complement pointwise: $x \in \mathbf{B}^\perp$ means the singleton $\{x\}$ is completely spacelike to $\mathbf{B}$. By the structural properties of complete spacelike separation (\ref{lmm:completely-spacelike-structural}), $\{x\}$ is completely spacelike to a union $\bigcup_i \mathbf{B}_i$ if and only if it is completely spacelike to each member $\mathbf{B}_i$. Hence membership in the complement of the union is the conjunction of membership in the individual complements, which is exactly membership in their intersection. The binary case is the special case of a two-element family. +\end{proof} + +\begin{theorem}[De Morgan Laws for the Causal Complement] + \label{thrm:causal-complement-de-morgan} + \lean{Physicslib4.Spacetime.LorentzianSpacetime.causalComplement_antitone, Physicslib4.Spacetime.LorentzianSpacetime.causalComplement_bot, Physicslib4.Spacetime.LorentzianSpacetime.causalComplement_top, Physicslib4.Spacetime.LorentzianSpacetime.causalComplement_sup, Physicslib4.Spacetime.LorentzianSpacetime.causalComplement_inf, Physicslib4.Spacetime.LorentzianSpacetime.causalComplement_iSup, Physicslib4.Spacetime.LorentzianSpacetime.causalComplement_iInf} + \leanfile{Physicslib4/Spacetime/CausalComplement.lean} + \uses{thrm:causally-complete-lattice, lmm:spacelike-complement-de-morgan} + \leanok + On the complete lattice of causally complete regions the causal complement $\mathbf{B} \mapsto \mathbf{B}^\perp$ is an order-reversing involution, and therefore satisfies the full De Morgan laws. Explicitly: + \begin{itemize} + \item (order-reversing) $\mathbf{B}_1 \le \mathbf{B}_2 \Rightarrow \mathbf{B}_2^\perp \le \mathbf{B}_1^\perp$; + \item (bounds) $\bot^\perp = \top$ and $\top^\perp = \bot$; + \item (binary De Morgan) $(\mathbf{B}_1 \sqcup \mathbf{B}_2)^\perp = \mathbf{B}_1^\perp \sqcap \mathbf{B}_2^\perp$ and $(\mathbf{B}_1 \sqcap \mathbf{B}_2)^\perp = \mathbf{B}_1^\perp \sqcup \mathbf{B}_2^\perp$; + \item (infinitary De Morgan) $\bigl(\bigsqcup_i \mathbf{B}_i\bigr)^\perp = \bigsqcap_i \mathbf{B}_i^\perp$ and $\bigl(\bigsqcap_i \mathbf{B}_i\bigr)^\perp = \bigsqcup_i \mathbf{B}_i^\perp$. + \end{itemize} +\end{theorem} +\begin{proof} + \leanok + \uses{thrm:causally-complete-lattice, lmm:spacelike-complement-de-morgan} + Recall from the lattice structure (\ref{thrm:causally-complete-lattice}) that on causally complete regions meets are intersections of the underlying sets, joins are the causal closures of unions ($\mathbf{B}_1 \sqcup \mathbf{B}_2 = (\mathbf{B}_1 \cup \mathbf{B}_2)^{\perp\perp}$ and dually for arbitrary families), the complement of any region is causally complete, and every region in the lattice satisfies the involution $\mathbf{B}^{\perp\perp} = \mathbf{B}$; in particular the triple-complement identity $\mathbf{C}^{\perp\perp\perp} = \mathbf{C}^\perp$ holds for any underlying set $\mathbf{C}$, since $\mathbf{C}^\perp$ is causally complete. Each law is then a direct computation on the underlying sets driven by the set-level De Morgan lemma (\ref{lmm:spacelike-complement-de-morgan}). + + \begin{itemize} + \item (order-reversing) This is the antitonicity half of the order-reversing involution supplied by \ref{thrm:causally-complete-lattice}: $\mathbf{B}_1 \le \mathbf{B}_2$ means $\mathbf{B}_1 \subseteq \mathbf{B}_2$, whence $\mathbf{B}_2^\perp \subseteq \mathbf{B}_1^\perp$, i.e. $\mathbf{B}_2^\perp \le \mathbf{B}_1^\perp$. + \item (join laws) Since the join is the causal closure of the union, the triple-complement identity collapses one level of complement: + \begin{align} + (\mathbf{B}_1 \sqcup \mathbf{B}_2)^\perp = \bigl((\mathbf{B}_1 \cup \mathbf{B}_2)^{\perp\perp}\bigr)^\perp = (\mathbf{B}_1 \cup \mathbf{B}_2)^{\perp\perp\perp} = (\mathbf{B}_1 \cup \mathbf{B}_2)^\perp = \mathbf{B}_1^\perp \cap \mathbf{B}_2^\perp = \mathbf{B}_1^\perp \sqcap \mathbf{B}_2^\perp, + \end{align} + the fourth equality being the binary set-level De Morgan lemma (\ref{lmm:spacelike-complement-de-morgan}) and the last using that lattice meets are intersections. The indexed form is identical with the indexed De Morgan lemma in place of the binary one, giving $\bigl(\bigsqcup_i \mathbf{B}_i\bigr)^\perp = \bigsqcap_i \mathbf{B}_i^\perp$. + \item (meet laws) Apply the set-level De Morgan lemma to the complements $\mathbf{B}_1^\perp, \mathbf{B}_2^\perp$ and use $\mathbf{B}_i^{\perp\perp} = \mathbf{B}_i$ (each $\mathbf{B}_i$ is causally complete): $(\mathbf{B}_1^\perp \cup \mathbf{B}_2^\perp)^\perp = \mathbf{B}_1^{\perp\perp} \cap \mathbf{B}_2^{\perp\perp} = \mathbf{B}_1 \cap \mathbf{B}_2$. Taking the complement of both sides and recognising the meet as the intersection and the join as the double-complement of the union, + \begin{align} + (\mathbf{B}_1 \sqcap \mathbf{B}_2)^\perp = (\mathbf{B}_1 \cap \mathbf{B}_2)^\perp = (\mathbf{B}_1^\perp \cup \mathbf{B}_2^\perp)^{\perp\perp} = \mathbf{B}_1^\perp \sqcup \mathbf{B}_2^\perp, + \end{align} + and likewise $\bigl(\bigsqcap_i \mathbf{B}_i\bigr)^\perp = \bigsqcup_i \mathbf{B}_i^\perp$ from the indexed De Morgan lemma. + \item (bounds) The empty-family case of the indexed De Morgan lemma (\ref{lmm:spacelike-complement-de-morgan}) reads $\varnothing^\perp = \mathrm{univ}$, so $\top = \mathrm{univ} = \varnothing^\perp$. Hence $\top^\perp = \varnothing^{\perp\perp} = \bot$, while $\bot = \varnothing^{\perp\perp}$ and the triple-complement identity give $\bot^\perp = \varnothing^{\perp\perp\perp} = \varnothing^\perp = \top$. + \end{itemize} + + The mathematical subtlety is that this lattice is \emph{not} linearly ordered, so the binary equalities do \emph{not} follow from antitonicity alone: a general antitone map only yields the inequality $f(\mathbf{B}_1 \sqcup \mathbf{B}_2) \le f\mathbf{B}_1 \sqcap f\mathbf{B}_2$. The equalities hold precisely because the causal complement is an order-reversing \emph{bijection} (the involution $\mathbf{B}^{\perp\perp} = \mathbf{B}$), equivalently an order isomorphism onto the order-dual lattice; it is this bijectivity that both forces the finite equalities above and, through the same set-level De Morgan computation applied to arbitrary unions, upgrades them to the infinitary laws by carrying suprema to infima. +\end{proof} + \begin{definition}[Alexandrov Topology] \label{def:alexandrov-topology} \lean{Physicslib4.Spacetime.alexandrovTopology} @@ -368,6 +505,56 @@ \section{Spacetime}\label{sctn:spacetime} By construction the Alexandrov topology is generated by these basis sets, and any generating set is open in the generated topology. \end{proof} +\begin{lemma}[Openness of Chronological Futures and Pasts] + \label{lmm:chronological-future-past-open} + \lean{Physicslib4.Spacetime.isOpen_chronologicalFuture_inter_chronologicalPast, Physicslib4.Spacetime.isOpen_chronologicalFuture, Physicslib4.Spacetime.isOpen_chronologicalPast} + \leanfile{Physicslib4/Spacetime/Causality.lean} + \uses{def:chronological-future-and-chronological-past, def:alexandrov-topology, lmm:alexandrov-basis-open} + \leanok + Let $M$ be a spacetime with time orientation $t$, equipped with the Alexandrov topology. + \begin{itemize} + \item For all points $p, q \in M$ the set $I^+(p) \cap I^-(q)$ is open. This is just the basis lemma (\ref{lmm:alexandrov-basis-open}) restated on chronological futures and pasts. + \item If every point of $I^+(p)$ has a chronological-future point, i.e. for all $x \in I^+(p)$ there exists $b$ with $x \ll b$, then the chronological future $I^+(p)$ is open. + \item Dually, if every point of $I^-(p)$ has a chronological-past point, i.e. for all $x \in I^-(p)$ there exists $a$ with $a \ll x$, then the chronological past $I^-(p)$ is open. + \end{itemize} + + The per-point hypotheses in the last two items are quantified over the members of the set in question, so they hold \emph{vacuously} when that set is empty; this is consistent, since the empty set is open. The flat unconditional claim ``$I^+(p)$ is always open'' is \emph{false} for a general spacetime: if $I^+(p)$ is nonempty and contains a future-endpoint point $x$ (a point with no $b$ satisfying $x \ll b$), then $x$ lies in no basis set $I^+(a) \cap I^-(b)$, since membership there forces $a \ll x \ll b$ and in particular $x \ll b$. Hence $x$ has no basic Alexandrov neighbourhood contained in $I^+(p)$ and $I^+(p)$ fails to be open. The hypothesis is exactly the ``no future endpoints'' condition that removes this obstruction, and dually for pasts. +\end{lemma} +\begin{proof} + \leanok + \uses{def:chronological-future-and-chronological-past, def:alexandrov-topology, lmm:alexandrov-basis-open} + The first item is the basis lemma (\ref{lmm:alexandrov-basis-open}) directly: $I^+(p) \cap I^-(q)$ is a basis set, hence open. + + For the second item, under the hypothesis we have the set identity + \begin{align} + I^+(p) = \bigcup_{b \in M} \bigl(I^+(p) \cap I^-(b)\bigr). + \end{align} + The right-hand side is contained in $I^+(p)$ since every term is. Conversely, if $x \in I^+(p)$ then by hypothesis there is $b$ with $x \ll b$, i.e. $x \in I^-(b)$, so $x$ lies in the $b$-th term. Each set $I^+(p) \cap I^-(b)$ is a basis set and hence open (\ref{lmm:alexandrov-basis-open}), and an arbitrary union of open sets is open; therefore $I^+(p)$ is open. The third item is dual, using $I^-(p) = \bigcup_{a \in M} \bigl(I^+(a) \cap I^-(p)\bigr)$. (Recall also that chronological precedence $\ll$ is transitive, \ref{thrm:precedence-transitive}.) +\end{proof} + +\begin{lemma}[Unconditional Openness of Chronological Futures and Pasts on Standard Minkowski] + \label{lmm:minkowski-chronological-open} + \lean{Physicslib4.exists_chronologicalFuture_standardMinkowski, Physicslib4.exists_chronologicalPast_standardMinkowski, Physicslib4.isOpen_chronologicalFuture_standardMinkowski, Physicslib4.isOpen_chronologicalPast_standardMinkowski, Physicslib4.isOpen_alexandrov_chronologicalFuture_standardMinkowski, Physicslib4.isOpen_alexandrov_chronologicalPast_standardMinkowski} + \leanfile{Physicslib4/Spacetime/Minkowski.lean} + \uses{lmm:chronological-future-past-open, def:standard-minkowski-spacetime, def:chronological-future-and-chronological-past, def:alexandrov-topology} + \leanok + Work on standard Minkowski spacetime, with underlying manifold $\mathbb{R}^4$, and let $e_0$ denote the unit time vector (the first standard coordinate vector). + \begin{enumerate} + \item Every point has a chronological future point and a chronological past point: for all $x \in \mathbb{R}^4$ there exist $b, a$ with $x \ll b$ and $a \ll x$. Concretely $b = x + e_0$ lies in the forward cone of $x$ and $a = x - e_0$ lies in the backward cone of $x$, since the connecting vector $\pm e_0$ is future-, respectively past-pointing timelike. + \item For every point $p$ the chronological future $I^+(p)$ and the chronological past $I^-(p)$ are open in the Euclidean (manifold) topology on $\mathbb{R}^4$. On standard Minkowski the coordinate cone characterisation identifies $I^+(p)$ with the forward Minkowski cone of $p$ and $I^-(p)$ with the backward Minkowski cone of $p$, and each such cone is an open subset of $\mathbb{R}^4$. + \item For every point $p$ the chronological future $I^+(p)$ and the chronological past $I^-(p)$ are open in the Alexandrov topology, \emph{unconditionally}: the per-point hypothesis of \ref{lmm:chronological-future-past-open} is discharged on standard Minkowski by part (i). + \end{enumerate} +\end{lemma} +\begin{proof} + \leanok + \uses{lmm:chronological-future-past-open, def:standard-minkowski-spacetime, def:chronological-future-and-chronological-past, def:alexandrov-topology} + Part (i) is read off the coordinate cone description of standard Minkowski: for any $x$ the difference $(x + e_0) - x = e_0$ has metric square $g(e_0, e_0) = -1 < 0$ and positive time component, so it is future-pointing timelike; hence $x \ll x + e_0$ and the forward cone of $x$ is nonempty. Dually $(x - e_0) - x = -e_0$ is past-pointing timelike, so $x - e_0 \ll x$ and the backward cone of $x$ is nonempty. + + Part (ii) combines the coordinate characterisation of $I^\pm$ on standard Minkowski with the openness of the explicit cones. Under the identification of $I^+(p)$ with the forward Minkowski cone $\{y \in \mathbb{R}^4 : g(y - p, y - p) < 0,\ (y - p)^0 > 0\}$, this set is the intersection of the preimages of the open sets $(-\infty, 0)$ and $(0, \infty)$ under the continuous maps $y \mapsto g(y - p, y - p)$ (a quadratic form) and $y \mapsto (y - p)^0$ (a coordinate projection); hence it is open in the Euclidean topology on $\mathbb{R}^4$. The backward cone description of $I^-(p)$ is dual and open by the same argument. + + Part (iii) applies the general lemma \ref{lmm:chronological-future-past-open}: its last two items give the openness of $I^+(p)$ and $I^-(p)$ in the Alexandrov topology provided every point of the set in question has, respectively, a chronological-future point and a chronological-past point. On standard Minkowski these hypotheses hold at every point by part (i), so both conclusions are unconditional. +\end{proof} + \begin{definition}[Minkowski Spacetime] \label{def:minkowski-spacetime} \lean{Physicslib4.MinkowskiSpacetime} @@ -399,6 +586,102 @@ \section{Spacetime}\label{sctn:spacetime} These are restatements of the symmetry of complete spacelike separation and the openness of basis sets for the underlying spacetime, transported through the bundling of a Lorentzian spacetime over its underlying spacetime and time orientation. \end{proof} +\begin{lemma}[No-Diamond Points Have Only the Whole Space as Neighbourhood] + \label{lmm:alexandrov-nbhd-univ-of-no-diamond} + \lean{alexandrov_nbhd_univ_of_no_diamond} + \leanfile{Physicslib4/Spacetime/Causality.lean} + \uses{def:alexandrov-topology} + \leanok + On a spacetime equipped with the Alexandrov topology, suppose a point $x$ lies in no diamond $I^+(p) \cap I^-(q)$. Then every Alexandrov-open set containing $x$ is the whole space $M$: the only open neighbourhood of $x$ is $M$ itself. +\end{lemma} +\begin{proof} + \leanok + The Alexandrov topology is generated by the diamond subbasis, so its open sets are exactly those built by the inductive generating construction, and we induct over that construction to show any generated-open set $U$ with $x \in U$ equals $M$. A basic generating set is a diamond, which cannot contain $x$ by hypothesis, so that case is vacuous. The whole-space generator is $M$. A binary intersection $s \cap t$ containing $x$ has $x \in s$ and $x \in t$, so $s = t = M$ by the induction hypothesis and $s \cap t = M$. A union $\bigcup_i s_i$ containing $x$ contains $x$ in some member $s_i$, which equals $M$ by the induction hypothesis, so the union contains $M$ and hence equals $M$. Thus no generated-open set other than $M$ contains $x$. +\end{proof} + +\begin{lemma}[Covering from the Hausdorff Assumption] + \label{lmm:alexandrov-covering-hausdorff} + \lean{Physicslib4.Spacetime.LorentzianSpacetime.sUnion_alexandrovBasis_eq_univ} + \leanfile{Physicslib4/Spacetime/LorentzianSpacetime.lean} + \uses{def:lorentzian-spacetime, def:alexandrov-topology, lmm:alexandrov-nbhd-univ-of-no-diamond} + \leanok + On a Lorentzian spacetime with at least two points, the Alexandrov diamonds cover the whole space: every point lies in some diamond $I^+(p) \cap I^-(q)$. Equivalently, every point has both a chronological past point and a chronological future point (a ``no endpoints'' condition). This is a genuine consequence of the Hausdorff assumption on the Alexandrov topology, not an extra hypothesis. +\end{lemma} +\begin{proof} + \leanok + \uses{lmm:alexandrov-nbhd-univ-of-no-diamond} + Suppose a point $x$ lay in no diamond $I^+(p) \cap I^-(q)$. Then by \ref{lmm:alexandrov-nbhd-univ-of-no-diamond} the only Alexandrov-open set containing $x$ is the whole space $M$. Since the space has a second point $y \ne x$, the Hausdorff assumption on the Alexandrov topology provides disjoint open sets separating $x$ and $y$; but the one containing $x$ must be all of $M$, which also contains $y$, contradicting disjointness. Hence every point lies in some diamond, which is exactly the covering half of the Alexandrov-basis property; unfolding membership in a diamond gives the equivalent ``no endpoints'' statement. +\end{proof} + +\begin{theorem}[The Alexandrov Diamonds Form a Topological Basis] + \label{thrm:alexandrov-topological-basis} + \lean{Physicslib4.Spacetime.LorentzianSpacetime.isTopologicalBasis_alexandrovBasis} + \leanfile{Physicslib4/Spacetime/LorentzianSpacetime.lean} + \uses{lmm:alexandrov-covering-hausdorff, def:alexandrov-topology, def:lorentzian-spacetime} + \leanok + On a Lorentzian spacetime with at least two points, suppose the diamonds are downward-directed: for any two diamonds $B_1, B_2$ and any point $x \in B_1 \cap B_2$ there is a diamond $B_3$ with $x \in B_3 \subseteq B_1 \cap B_2$ (the intersection property). Then the diamonds form a genuine topological basis for the Alexandrov topology. +\end{theorem} +\begin{proof} + \leanok + The three conditions of a topological basis all hold. The intersection (downward-directedness) property is the standing hypothesis. The covering condition --- that the diamonds' union is the whole space --- is \ref{lmm:alexandrov-covering-hausdorff}. The topology-generation condition holds by definition, since the Alexandrov topology is \emph{defined} as the topology generated by the diamond subbasis. The directedness hypothesis is the genuinely geometric content: it is exactly the assertion that the Alexandrov topology has the diamonds as a base, and it is not implied by Hausdorffness alone; it is discharged for standard Minkowski in \ref{thrm:minkowski-alexandrov-basis}. +\end{proof} + +\begin{lemma}[Past Interpolation on Standard Minkowski] + \label{lmm:minkowski-past-between} + \lean{Physicslib4.Spacetime.exists_past_between_standardMinkowski} + \leanfile{Physicslib4/Spacetime/MinkowskiDirected.lean} + \uses{def:standard-minkowski-spacetime, def:chronological-future-and-chronological-past, lmm:minkowski-chronological-open} + \leanok + On standard Minkowski spacetime, if $p_1 \ll x$ and $p_2 \ll x$ then there is a point $a$ with $p_1 \ll a$, $p_2 \ll a$, and $a \ll x$. +\end{lemma} +\begin{proof} + \leanok + \uses{lmm:minkowski-chronological-open} + Take $a$ with the same spatial coordinates as $x$ and time coordinate $a^0 = x^0 - \varepsilon$ for a small $\varepsilon > 0$. Then $x - a = (\varepsilon, \mathbf{0})$ is future-pointing timelike, so $a \ll x$. For each $i$ the connecting vector $a - p_i$ has the same spatial part as $x - p_i$ while its time component is $(x^0 - p_i^0) - \varepsilon$; since $p_i \ll x$ makes the spatial separation strictly smaller than $x^0 - p_i^0$, for $\varepsilon$ small enough the reduced time gap still dominates the spatial separation and remains positive, so $a - p_i$ is future-pointing timelike and $p_i \ll a$. Both strict inequalities hold for a common small $\varepsilon$; the estimate is a direct coordinate computation (\texttt{nlinarith}). +\end{proof} + +\begin{lemma}[Future Interpolation on Standard Minkowski] + \label{lmm:minkowski-future-between} + \lean{Physicslib4.Spacetime.exists_future_between_standardMinkowski} + \leanfile{Physicslib4/Spacetime/MinkowskiDirected.lean} + \uses{def:standard-minkowski-spacetime, def:chronological-future-and-chronological-past, lmm:minkowski-chronological-open} + \leanok + On standard Minkowski spacetime, if $x \ll q_1$ and $x \ll q_2$ then there is a point $b$ with $x \ll b$, $b \ll q_1$, and $b \ll q_2$. +\end{lemma} +\begin{proof} + \leanok + \uses{lmm:minkowski-past-between, lmm:minkowski-chronological-open} + Dual to \ref{lmm:minkowski-past-between}: take $b$ with the same spatial coordinates as $x$ and time coordinate $b^0 = x^0 + \varepsilon$ for a small $\varepsilon > 0$. Then $b - x = (\varepsilon, \mathbf{0})$ is future-pointing timelike, so $x \ll b$, and for each $i$ the vector $q_i - b$ keeps the spatial part of $q_i - x$ with time component $(q_i^0 - x^0) - \varepsilon$; for $\varepsilon$ small enough it stays future-pointing timelike, giving $b \ll q_i$ for both $i$ by the same coordinate estimate. +\end{proof} + +\begin{lemma}[Standard Minkowski Diamonds Are Downward-Directed] + \label{lmm:minkowski-diamonds-downward-directed} + \lean{Physicslib4.Spacetime.alexandrovBasis_exists_subset_inter_standardMinkowski} + \leanfile{Physicslib4/Spacetime/MinkowskiDirected.lean} + \uses{lmm:minkowski-past-between, lmm:minkowski-future-between, thrm:precedence-transitive, def:standard-minkowski-spacetime, def:alexandrov-topology, def:chronological-future-and-chronological-past} + \leanok + On standard Minkowski spacetime the Alexandrov diamonds have the downward intersection property: for any two diamonds $B_1 = I^+(p_1) \cap I^-(q_1)$ and $B_2 = I^+(p_2) \cap I^-(q_2)$ and any $x \in B_1 \cap B_2$, there is a diamond $B_3$ with $x \in B_3 \subseteq B_1 \cap B_2$. +\end{lemma} +\begin{proof} + \leanok + \uses{lmm:minkowski-past-between, lmm:minkowski-future-between, thrm:precedence-transitive} + From $x \in B_1 \cap B_2$ we have $p_1 \ll x$, $p_2 \ll x$, $x \ll q_1$, and $x \ll q_2$. Past interpolation (\ref{lmm:minkowski-past-between}) yields $a$ with $p_1 \ll a$, $p_2 \ll a$, and $a \ll x$; future interpolation (\ref{lmm:minkowski-future-between}) yields $b$ with $x \ll b$, $b \ll q_1$, and $b \ll q_2$. Set $B_3 = I^+(a) \cap I^-(b)$; then $a \ll x \ll b$ gives $x \in B_3$. For containment, any $y$ with $a \ll y \ll b$ satisfies $p_i \ll a \ll y$ and $y \ll b \ll q_i$ for each $i$, so by transitivity of $\ll$ (\ref{thrm:precedence-transitive}) $y \in I^+(p_i) \cap I^-(q_i)$; hence $B_3 \subseteq B_1 \cap B_2$. +\end{proof} + +\begin{theorem}[The Alexandrov Diamonds are a Basis on Standard Minkowski] + \label{thrm:minkowski-alexandrov-basis} + \lean{Physicslib4.Spacetime.isTopologicalBasis_alexandrovBasis_standardMinkowski} + \leanfile{Physicslib4/Spacetime/MinkowskiDirected.lean} + \uses{thrm:alexandrov-topological-basis, lmm:minkowski-diamonds-downward-directed, lmm:minkowski-chronological-open, def:standard-minkowski-spacetime, def:alexandrov-topology} + \leanok + On standard Minkowski spacetime the Alexandrov diamonds form a genuine topological basis for the Alexandrov topology, unconditionally. +\end{theorem} +\begin{proof} + \leanok + \uses{thrm:alexandrov-topological-basis, lmm:minkowski-diamonds-downward-directed, lmm:minkowski-chronological-open} + Apply \ref{thrm:alexandrov-topological-basis}. Its downward intersection hypothesis is discharged by \ref{lmm:minkowski-diamonds-downward-directed}, and its covering condition holds because on standard Minkowski every point has a chronological past point and a chronological future point (\ref{lmm:minkowski-chronological-open}). The topology-generation condition holds by definition of the Alexandrov topology. +\end{proof} + \subsection{Isometries and basis-set preservation} \begin{lemma}[Isometries Preserve the Causal Classification] diff --git a/blueprint/src/sections/sec10/10-3_haag-kastler-axioms.tex b/blueprint/src/sections/sec10/10-3_haag-kastler-axioms.tex index 03ac155..d6727b3 100644 --- a/blueprint/src/sections/sec10/10-3_haag-kastler-axioms.tex +++ b/blueprint/src/sections/sec10/10-3_haag-kastler-axioms.tex @@ -216,6 +216,15 @@ \subsection{Local von Neumann Algebras} The separating property phrased on the bundled \texttt{VonNeumannAlgebra} $R(\mathbf{B}_2)$: with $\Omega$ cyclic for the local observables of $\mathbf{B}_1$, every $R$ in the bundled algebra $R(\mathbf{B}_2)$ of a spacelike-separated region with $R\Omega = 0$ is zero. It reduces to \ref{thrm:statistical-independence} through the coercion $\uparrow R(\mathbf{B}_2) = \pi(\mathfrak{U}(\mathbf{B}_2))''$. \end{theorem} +\begin{theorem}[Additive-Free Locality via the Spacelike Complement] + \label{thrm:additive-free-locality} + \lean{Physicslib4.AQFT.HaagKastler.HaagKastlerNet.localVonNeumannAlgebra_le_commutant_of_subset_spacelikeComplement} + \leanfile{Physicslib4/AQFT/HaagKastler/LocalVonNeumann.lean} + \leanok + \uses{thrm:von-neumann-bundled-order, def:spacelike-complement} + Locality expressed through the spacelike complement, without attaching any algebra to the unbounded complement: for basis sets $\mathbf{B}' \subseteq \mathbf{B}^\perp$, the local von Neumann algebra $R(\mathbf{B}')$ lies in the commutant $R(\mathbf{B})'$. It is a direct repackaging of bundled microcausality (\ref{thrm:von-neumann-bundled-order}) through the Galois bridge $\mathbf{B}' \subseteq \mathbf{B}^\perp \iff \mathbf{B}', \mathbf{B}$ completely spacelike, staying strictly within the physically local (bounded, diamond) regions. No local algebra is ever attached to the unbounded complement. +\end{theorem} + \begin{theorem}[Geometric Covariance of the von Neumann Net] \label{thrm:von-neumann-geometric-covariance} \lean{Physicslib4.AQFT.HaagKastler.CovariantQuasilocalAlgebra.lieConj_image_covLocalVonNeumann, Physicslib4.AQFT.HaagKastler.CovariantQuasilocalAlgebra.lieConj_image_covLocalOperators} @@ -505,6 +514,33 @@ \subsection{Unitary Equivalence and Superselection} The endomorphism algebra of an irreducible representation is $\mathbb{C}\cdot 1$: every self-intertwiner of an irreducible representation is a scalar multiple of the identity. This is the commutant form of irreducibility read through the intertwiner language, and it identifies each irreducible sector with a simple (one-dimensional-centred) object. \end{lemma} +\begin{theorem}[The commutant (self-intertwiner) von Neumann algebra] + \label{thrm:commutant-von-neumann} + \lean{Physicslib4.GNS.commutantVonNeumann, Physicslib4.GNS.mem_commutantVonNeumann_iff_intertwines, Physicslib4.GNS.isIrreducible_iff_commutantVonNeumann_eq_scalars} + \leanfile{Physicslib4/GNS/Superselection.lean} + \leanok + \uses{def:irreducible-representation, lmm:endomorphism-scalar} + The commutant $\pi(A)'$ of a representation is packaged as a von Neumann algebra --- the algebra of self-intertwiners, i.e. the intertwiner/gauge algebra of $\pi$. Its underlying set is the centralizer of $\pi(A)$ (self-adjoint, and a commutant is always a von Neumann algebra since $S''' = S'$), an operator lies in it exactly when it is a self-intertwiner of $\pi$, and $\pi$ is irreducible if and only if this algebra is trivial ($\pi(A)' = \mathbb{C}\cdot 1$) --- the von Neumann form of Schur's lemma. +\end{theorem} + +\begin{theorem}[Double-Commutant Duality] + \label{thrm:double-commutant-duality} + \lean{Physicslib4.GNS.commutant_gnsVonNeumannAlgebra, Physicslib4.GNS.commutant_commutantVonNeumann} + \leanfile{Physicslib4/GNS/Superselection.lean} + \uses{thrm:commutant-von-neumann} + \leanok + The generated von Neumann algebra $\pi(A)''$ and the commutant von Neumann algebra $\pi(A)'$ (\ref{thrm:commutant-von-neumann}) are each other's commutants. On one side, the commutant of $\pi(A)''$ is $\pi(A)'$: this is an instance of the triple-commutant collapse $S''' = S'$ applied to the self-adjoint image $\pi(A)$. On the other side, the commutant of $\pi(A)'$ is $\pi(A)''$, which is exactly the definition of the bicommutant. Together these are von Neumann's double-commutant relation for this pair, and they exhibit the bicommutant as idempotent: taking the commutant twice returns $(\pi(A)'')'' = \pi(A)''$, so $\pi(A)''$ and $\pi(A)'$ form a mutually dual pair under $S \mapsto S'$. +\end{theorem} + +\begin{theorem}[A Factor and its Commutant; Triviality Duality] + \label{thrm:commutant-factor-duality} + \lean{Physicslib4.GNS.isFactor_gnsVonNeumann_iff_isFactor_commutant, Physicslib4.GNS.commutantVonNeumann_eq_scalars_iff_gnsVonNeumann_eq_univ} + \leanfile{Physicslib4/GNS/Superselection.lean} + \uses{thrm:double-commutant-duality, thrm:commutant-von-neumann, thrm:irreducible-generates-all} + \leanok + A von Neumann algebra and its commutant share the same center: the intersection $\pi(A)'' \cap (\pi(A)'')' = \pi(A)'' \cap \pi(A)'$ is symmetric under the duality of \ref{thrm:double-commutant-duality}, being simultaneously the center of $\pi(A)''$ and the center of $\pi(A)'$. Consequently $\pi(A)''$ is a factor (trivial center) if and only if its commutant $\pi(A)'$ is a factor. Dually, at the extreme of triviality, the commutant collapses to the scalars $\pi(A)' = \mathbb{C}\cdot 1$ if and only if the generated algebra is everything $\pi(A)'' = \mathcal{B}(H)$; this is the commutant form of the equivalence ``irreducible $\iff$ generates $\mathcal{B}(H)$'' (\ref{thrm:commutant-von-neumann}), passing between the two sides through the bicommutant $(\mathbb{C}\cdot 1)' = \mathcal{B}(H)$. +\end{theorem} + \begin{theorem}[The Pure-State Dichotomy] \label{thrm:pure-state-dichotomy} \lean{Physicslib4.GNS.exists_gns_areDisjoint_or_unitaryEquiv_of_isPure} diff --git a/blueprint/src/sections/sec10/10-4_haag-kastler-axioms-in-curved-spacetime.tex b/blueprint/src/sections/sec10/10-4_haag-kastler-axioms-in-curved-spacetime.tex index f33fec9..e14b4b6 100644 --- a/blueprint/src/sections/sec10/10-4_haag-kastler-axioms-in-curved-spacetime.tex +++ b/blueprint/src/sections/sec10/10-4_haag-kastler-axioms-in-curved-spacetime.tex @@ -217,6 +217,15 @@ \subsection{Local von Neumann Algebras in Curved Spacetime} The separating property phrased on the bundled \texttt{VonNeumannAlgebra} $R(\mathbf{B}_2)$: with $\Omega$ cyclic for the local observables of $\mathbf{B}_1$, every $R$ in the bundled algebra $R(\mathbf{B}_2)$ of a spacelike-separated subregion with $R\Omega = 0$ is zero. It reduces to \ref{thrm:statistical-independence-in-curved-spacetime} through the coercion $\uparrow R(\mathbf{B}_2) = \pi(\mathfrak{U}(\mathbf{B}_2))''$. \end{theorem} +\begin{theorem}[Additive-Free Locality via the Spacelike Complement (Curved Spacetime)] + \label{thrm:additive-free-locality-in-curved-spacetime} + \lean{Physicslib4.AQFT.HaagKastlerCurved.HaagKastlerNet.localVonNeumannAlgebra_le_commutant_of_subset_spacelikeComplement_geometric} + \leanfile{Physicslib4/AQFT/HaagKastlerCurved/Concrete.lean} + \leanok + \uses{thrm:additive-free-locality, thrm:von-neumann-bundled-order-in-curved-spacetime, def:spacelike-complement} + The geometric specialisation of additive-free locality to a curved local net over a concrete Lorentzian spacetime $L$: for basis sets $\mathbf{B}_1 \subseteq \mathbf{B}_2^\perp$ inside a common containing region $\mathbf{B}$, the local von Neumann algebra $R(\mathbf{B}_1)$ lies in the commutant $R(\mathbf{B}_2)'$. As in Minkowski, the spacelike complement $\mathbf{B}_2^\perp$ only \emph{selects} the bounded regions spacelike to $\mathbf{B}_2$; no algebra is attached to the unbounded complement. The Galois bridge discharges the spacelike hypothesis, and $L.\mathtt{toAbstract}$ identifies the concrete and abstract spacelike relations. +\end{theorem} + \begin{theorem}[Geometric Covariance of the von Neumann Net (Curved Spacetime)] \label{thrm:von-neumann-geometric-covariance-in-curved-spacetime} \lean{Physicslib4.AQFT.HaagKastlerCurved.HaagKastlerNet.lieConj_image_localVonNeumann, Physicslib4.AQFT.HaagKastlerCurved.HaagKastlerNet.lieConj_image_localOperators} diff --git a/home_page/index.md b/home_page/index.md index 152d833..93d890d 100644 --- a/home_page/index.md +++ b/home_page/index.md @@ -25,7 +25,17 @@ usemathjax: true In 1964, Rudolf Haag and Daniel Kastler introduced a set of axioms for Algebraic Quantum Field Theory (AQFT) in Minkowski spacetime, proposing a mathematically rigorous, operator-algebraic framework for quantum field theory in terms of nets of C\*-algebras indexed by regions of Minkowski spacetime. This project formalises a "sharpened" version of these axioms in the [Lean Theorem Prover](https://leanprover-community.github.io), following the [original paper by Haag and Kastler](https://doi.org/10.1063/1.1704187). The original axioms, while revolutionary, left several details underspecified. This project clarifies those details and produces definitions, theorems, and axioms amenable to computer-assisted formalisation. In addition, this project formalises these "sharpened" axioms in curved spacetime too. -The blueprint is structured so that Chapters 1–9 motivate and analyse each of the original Haag–Kastler axioms in turn as well as their generalisation to curved spacetime. These chapters serve as mathematical background and are not themselves formalised in Lean. Chapter 10 then collects the "sharpened" axioms together with the supporting definitions and theorems that have been carefully stated for formalisation; it is the content of Chapter 10—and only Chapter 10—that is formalised in Lean. +The blueprint is structured so that Chapters 1–9 motivate and analyse each of the original Haag–Kastler axioms in turn as well as their generalisation to curved spacetime. These chapters serve as mathematical background and are not themselves formalised in Lean. Chapter 10 then collects the "sharpened" axioms together with the supporting definitions and theorems that have been carefully stated for formalisation; it is the content of Chapter 10—and only Chapter 10—that is formalised in Lean. The formalised declarations of Chapter 10 are numbered consecutively, running from Definition 13 through Definition 207, and comprise 195 declarations in total: 74 definitions, 80 theorems, and 41 lemmas. (The lower numbers, 1 through 12, label supporting theorems and definitions that are introduced along the way in the motivational Chapters 1–9; these are background results, cited when needed, and are not themselves formalised in Lean.) + +At a glance, these 195 declarations break down by the four top-level sections of Chapter 10 as follows: + +| Section | Topic | Definitions | Theorems | Lemmas | Total | +|---|---|---|---|---|---| +| §10.1 | GNS Construction | 2 | 1 | 3 | 6 | +| §10.2 | Spacetime and causal structure | 24 | 9 | 22 | 55 | +| §10.3 | Haag–Kastler Axioms (Minkowski) | 30 | 44 | 12 | 86 | +| §10.4 | Haag–Kastler Axioms (curved spacetime) | 18 | 26 | 4 | 48 | +| **Total** | | **74** | **80** | **41** | **195** | If you'd like to contribute, you may find the following links useful: @@ -39,62 +49,67 @@ If you'd like to contribute, you may find the following links useful: Chapters 1–9 of the blueprint unpack and analyse the original Haag–Kastler axioms one by one: -- **Chapter 1** presents the original Haag–Kastler axioms as stated in the 1964 paper. -- **Chapter 2 (Axiom 0 – Minkowski Space)** examines the role of Minkowski spacetime and compares the standard, indiscrete, Euclidean, and Alexandrov topologies on it, settling on the Alexandrov topology—generated by the "double cone" sets $$I^+(p) \cap I^-(q)$$—as the physically natural choice, which happens to coincide with the Euclidean topology on $$\mathbb{R}^4$$. -- **Chapter 3 (Axiom 1 – Local Algebras)** discusses the notion of regions of measurement and the assignment of a C\*-algebra to each such region, arguing that the "physically natural" regions are double cones $$I^+(p) \cap I^-(q)$$ rather than arbitrary open sets with compact closure, and rejecting the causal (light-cone) alternative $$J^+(p) \cap J^-(q)$$ because it would force single points to carry algebras, which conflicts with fields being operator-valued distributions. -- **Chapter 4 (Axiom 2 – Isotony)** introduces the GNS Construction in motivating context, studies the isotony condition—the requirement that inclusions of spacetime regions induce \*-monomorphisms of the corresponding algebras—and settles the "common unit" convention flagged in the original axiom by assigning the empty region the algebra $$\mathbb{C}1$$, so that every local algebra automatically contains a unit. -- **Chapter 5 (Axiom 3 – Local Commutativity)** introduces the notion of completely spacelike separated regions and the quasilocal algebra, and studies the requirement that observables localised in spacelike separated regions commute, clarifying that this commutation is to be understood inside the quasilocal algebra $$\mathfrak{U}$$, since isotony alone cannot place two spacelike-separated (and hence non-nested) regions in a common algebra. -- **Chapter 6 (Axiom 4 – Quasilocal Algebra)** analyses the construction of the quasilocal algebra as the completion of the set-theoretic union of all local algebras, and the axiom that $$\mathfrak{U}$$ contains all observables of interest—which is shown to mean that $$\pi_\omega(\mathfrak{U})$$ is strongly dense in the von Neumann algebra $$\pi_\omega(\mathfrak{U})''$$ it generates, so that any "missing" observable in $$\pi_\omega(\mathfrak{U})'' \setminus \pi_\omega(\mathfrak{U})$$ is experimentally indistinguishable from one in $$\mathfrak{U}$$. -- **Chapter 7 (Axiom 5 – Lorentz Covariance)** studies the action of the inhomogeneous Lorentz group (connected to the identity) on the net of local algebras and the covariance requirement, and shows, via the Bounded Linear Transformation Theorem, how this norm-one action extends uniquely from the dense union of local algebras to the whole quasilocal algebra. -- **Chapter 8 (Axiom 6 – Primitivity)** examines faithful and irreducible representations, noting that every unital C\*-algebra already has a faithful representation (Gelfand–Naimark) so primitivity is a genuinely extra condition; this axiom is ultimately abandoned in the sharpened formulation, following later presentations by Haag himself, on the grounds that its physical motivation is thin. -- **Chapter 9 (Haag–Kastler Axioms in Curved Spacetime)** generalises the Haag–Kastler axioms from Minkowski spacetime to curved (Lorentzian) spacetime. It first pins down a precise definition of Lorentzian spacetime and its Alexandrov topology, then shows—via a Schwarzschild black-hole counterexample—that a quasilocal algebra need not exist on a generic Lorentzian spacetime, so Local Commutativity and the local-algebra axiom must be restated relative to a common containing region rather than a global algebra. The final section replaces Lorentz covariance with covariance under identity-component isometries; a formalisation remark notes that the Lean development works with the intersection of the identity component with the (explicitly orientation-preserving) isometry subgroup, since the inclusion of the identity component into the orientation-preserving isometries would otherwise rely on a Myers–Steenrod-type rigidity result not yet available in Mathlib—an implementation choice that does not alter the mathematical content of the axiom. +- **Chapter 1 (p. 3)** presents the original Haag–Kastler axioms as stated in the 1964 paper. +- **Chapter 2 (Axiom 0 – Minkowski Space, p. 4)** examines the role of Minkowski spacetime and compares the standard, indiscrete, Euclidean, and Alexandrov topologies on it, settling on the Alexandrov topology—generated by the "double cone" sets $$I^+(p) \cap I^-(q)$$—as the physically natural choice, which happens to coincide with the Euclidean topology on $$\mathbb{R}^4$$. +- **Chapter 3 (Axiom 1 – Local Algebras, p. 6)** discusses the notion of regions of measurement and the assignment of a C\*-algebra to each such region, arguing that the "physically natural" regions are double cones $$I^+(p) \cap I^-(q)$$ rather than arbitrary open sets with compact closure, and rejecting the causal (light-cone) alternative $$J^+(p) \cap J^-(q)$$ because it would force single points to carry algebras, which conflicts with fields being operator-valued distributions. +- **Chapter 4 (Axiom 2 – Isotony, p. 9)** introduces the GNS Construction in motivating context, studies the isotony condition—the requirement that inclusions of spacetime regions induce \*-monomorphisms of the corresponding algebras—and settles the "common unit" convention flagged in the original axiom by assigning the empty region the algebra $$\mathbb{C}1$$, so that every local algebra automatically contains a unit. +- **Chapter 5 (Axiom 3 – Local Commutativity, p. 12)** introduces the notion of completely spacelike separated regions and the quasilocal algebra, and studies the requirement that observables localised in spacelike separated regions commute, clarifying that this commutation is to be understood inside the quasilocal algebra $$\mathfrak{U}$$, since isotony alone cannot place two spacelike-separated (and hence non-nested) regions in a common algebra. +- **Chapter 6 (Axiom 4 – Quasilocal Algebra, p. 14)** analyses the construction of the quasilocal algebra as the completion of the set-theoretic union of all local algebras, and the axiom that $$\mathfrak{U}$$ contains all observables of interest—which is shown to mean that $$\pi_\omega(\mathfrak{U})$$ is strongly dense in the von Neumann algebra $$\pi_\omega(\mathfrak{U})''$$ it generates, so that any "missing" observable in $$\pi_\omega(\mathfrak{U})'' \setminus \pi_\omega(\mathfrak{U})$$ is experimentally indistinguishable from one in $$\mathfrak{U}$$. +- **Chapter 7 (Axiom 5 – Lorentz Covariance, p. 17)** studies the action of the inhomogeneous Lorentz group (connected to the identity) on the net of local algebras and the covariance requirement, and shows, via the Bounded Linear Transformation Theorem, how this norm-one action extends uniquely from the dense union of local algebras to the whole quasilocal algebra. +- **Chapter 8 (Axiom 6 – Primitivity, p. 19)** examines faithful and irreducible representations, noting that every unital C\*-algebra already has a faithful representation (Gelfand–Naimark) so primitivity is a genuinely extra condition; this axiom is ultimately abandoned in the sharpened formulation, following later presentations by Haag himself, on the grounds that its physical motivation is thin. +- **Chapter 9 (Haag–Kastler Axioms in Curved Spacetime, p. 21)** generalises the Haag–Kastler axioms from Minkowski spacetime to curved (Lorentzian) spacetime. It first pins down a precise definition of Lorentzian spacetime and its Alexandrov topology, then shows—via a Schwarzschild black-hole counterexample—that a quasilocal algebra need not exist on a generic Lorentzian spacetime, so Local Commutativity and the local-algebra axiom must be restated relative to a common containing region rather than a global algebra. The final section replaces Lorentz covariance with covariance under identity-component isometries; a formalisation remark notes that the Lean development works with the intersection of the identity component with the (explicitly orientation-preserving) isometry subgroup, since the inclusion of the identity component into the orientation-preserving isometries would otherwise rely on a Myers–Steenrod-type rigidity result not yet available in Mathlib—an implementation choice that does not alter the mathematical content of the axiom. Chapter 10 assembles the formalisation-ready content, organised into seven main blocks that follow the section structure of the chapter itself (§10.1–§10.4): -- **GNS Construction (§10.1).** Carefully states and proves the GNS Construction Theorem in full detail—construction of the GNS Hilbert space, the \*-representation, the cyclic vector, faithfulness, and uniqueness up to unitary equivalence—since both the theorem and specific steps of its proof are used in the axioms that follow. +- **GNS Construction (§10.1, pp. 28–37).** Carefully states and proves the GNS Construction Theorem (Theorem 15) in full detail—construction of the GNS Hilbert space, the \*-representation, the cyclic vector, faithfulness of the representation for a faithful state, and uniqueness up to unitary equivalence—since both the theorem and specific steps of its proof are used in the axioms that follow. The supporting lemmas are the Cauchy–Schwarz inequality for positive functionals (Lemma 16) and the two equivalent descriptions of the GNS left ideal $$\mathcal{N}$$, which is shown to be a closed linear subspace (Lemmas 17–18). + +- **Spacetime and causal structure (§10.2, pp. 37–48).** Gives precise definitions of spacetime (Definition 19), standard Minkowski spacetime (Definition 20), Minkowski spacetime—standard Minkowski spacetime equipped with the Alexandrov topology (Definition 64)—and Lorentzian spacetime, a spacetime whose Alexandrov topology is Hausdorff (Definition 65). The full apparatus of causal structure is built up alongside: timelike, spacelike, and null vectors (Definition 21); time orientations (Definition 25); future- and past-pointing vectors (Definition 26); paths, curves, and oriented curves, defined as equivalence classes of paths up to reparametrisation (Definitions 31–36), with the causal type and the future/past orientation each shown to be well-defined on the quotient (Theorems 35 and 37) and a forgetful projection from oriented to unoriented curves (Theorem 38); trips and causal trips (Definitions 40–41); chronological and causal futures and pasts (Definitions 45–46); spacelike separation of points and of regions (Definitions 49–50); and the Alexandrov topology itself (Definition 60). Supporting lemmas establish the basic geometry: the causal classification trichotomy (Lemma 22), the reverse Cauchy–Schwarz and reverse triangle inequalities for timelike vectors (Lemmas 23–24), the sign lemma for the future cone, the definiteness of the spacelike complement of a timelike vector, and the convexity of the future and past cones (Lemmas 27–30), the inclusion of chronological in causal precedence (Lemma 47), the monotonicity of futures and pasts (Lemma 48), and the symmetry and structural properties of spacelike separation (Lemmas 51–52). The block then develops three further layers: + - *The causal order.* Chronological and causal precedence are shown to be transitive (Theorem 42). A spacetime is said to satisfy the causality condition when it has no closed causal curves—equivalently, when no point causally precedes itself (Definition 43). Under this condition, chronological precedence is irreflexive and causal precedence is asymmetric and antisymmetric, so that causal precedence is a strict partial order on the events of the spacetime (Theorem 44). + - *The spacelike complement and causal closure.* The spacelike complement $$\mathbf{B}^\perp$$ of a region—the set of points completely spacelike-separated from it (Definition 53)—is antitone, every region is contained in its double complement, and the triple complement collapses to the single one, making complementation the Galois connection attached to the spacelike-separation relation (Lemma 54). The double complement $$\mathbf{B} \mapsto \mathbf{B}^{\perp\perp}$$ is therefore a closure operator (Definition 55), whose fixed points are the causally complete regions (Definition 56). The causally complete regions form a complete lattice—meets are intersections, joins are causal closures of unions—on which the causal complement is an order-reversing involution (Theorem 57): the set-level De Morgan laws for the spacelike complement (Lemma 58) lift to full binary and infinitary De Morgan laws on the lattice (Theorem 59). The blueprint is careful to note what does not hold: the full orthocomplement law $$\mathbf{B} \wedge \mathbf{B}^\perp = \bot$$ fails at this generality, because the trip-based causal relation is irreflexive and so a point is spacelike-separated from itself; what holds is the complete lattice with an order-reversing De Morgan involution. + - *The Alexandrov basis theorems.* Every diamond $$I^+(p) \cap I^-(q)$$ is open in the Alexandrov topology (Lemma 61). Chronological futures and pasts are open under an explicit "no endpoints" hypothesis—every point of the set has a point strictly in its chronological future, respectively past (Lemma 62)—and are open unconditionally on standard Minkowski spacetime, where the coordinate-cone description discharges the hypothesis (Lemma 63). A point lying in no diamond is pathological: its only Alexandrov neighbourhood is the whole space (Lemma 67). The Hausdorff assumption on a Lorentzian spacetime rules this out, forcing the diamonds to cover the space—equivalently, every point has both a chronological past point and a chronological future point (Lemma 68). Given a downward-directedness (intersection) property, the diamonds then form a genuine topological basis for the Alexandrov topology (Theorem 69); the past and future interpolation lemmas (Lemmas 70–71) prove downward-directedness on standard Minkowski spacetime (Lemma 72), so there the diamonds are an unconditional basis (Theorem 73). -- **Spacetime and causal structure (§10.2).** Gives precise definitions of spacetime, Minkowski spacetime, and Lorentzian spacetime, together with the full apparatus of causal structure: timelike, spacelike, and null vectors; time orientation; future- and past-pointing vectors; paths; curves and oriented curves, defined as equivalence classes of paths up to reparametrisation, with the causal type and the future/past orientation each shown to be well-defined on the quotient (Theorems 35 and 37) and a forgetful projection from oriented to unoriented curves (Theorem 38); trips and causal trips; chronological and causal futures and pasts; spacelike separation; and the Alexandrov topology. Supporting lemmas establish the basic geometry (the causal classification trichotomy, the reverse Cauchy–Schwarz and reverse triangle inequalities for timelike vectors, convexity of the future and past cones, monotonicity of futures and pasts, symmetry of spacelike separation, and, in §10.2.1, the fact that isometries preserve causal classification, chronology, and Alexandrov-basis sets). + A formalisation remark records the one known divergence from the Lean code: the "geodesic" clause of a (causal) trip segment is currently a placeholder (`IsGeodesic` is defined to be `True`), pending a Lorentzian Levi-Civita connection in Mathlib; the endpoint, timelike/causal, and future-orientation content of trips is faithful. Finally, §10.2.1 shows that (future-orientation-preserving) isometries preserve the causal classification of tangent vectors (Lemma 74), have well-defined pushforwards of paths (Lemmas 75–76), preserve chronology (Lemma 77), and map Alexandrov-basis diamonds to diamonds (Lemma 78), which is exactly the well-definedness condition for the Axiom 5 action (Lemma 79). -- **Sharpened Haag–Kastler Axioms in Minkowski spacetime (§10.3, §10.3.1, §10.3.6).** States the sharpened axioms—Local Algebras, Isotony, Local Commutativity, Quasilocal Completeness, and Lorentz Covariance—bundled into a single `HaagKastlerNet` structure (Definitions 61–68). Derives the operator form of Einstein Causality in a representation (Theorem 69). Then develops the covariance structure: - - Defines covariant families of local states (Definition 113) and the lift of the fiberwise covariance action to a \*-automorphism of the quasilocal algebra—the `QuasilocalCovarianceAutomorphism` (Definition 115)—and establishes its uniqueness (Lemma 116), existence (Theorem 117), and existence for the trivial net (Theorem 118). This data is bundled into a `CovariantQuasilocalAlgebra` structure (Definition 119), on which the covariance action is a genuine group action (Lemma 120). - - Defines invariant states (Definition 121) and proves GNS-unitary implementation of a Poincaré-invariant state (Theorem 122). - - Proves that a state that is both invariant and pure yields a GNS representation that is simultaneously covariant and irreducible—a necessary precursor to a vacuum representation (Theorem 123). - - Lays a "bounded-generator" scaffold toward the spectrum condition, deliberately sidestepping Stone's theorem and unbounded self-adjoint operators (not yet available for this purpose in Mathlib): positive energy for a bounded generator (Definition 124) together with its basic API—the trivial group has positive energy, the witnessing generator is unique, positive energy is preserved under unitary conjugation, and a positive-energy group is automatically strongly continuous (Theorem 125); a generator-parameterised notion of vacuum state (Definition 126) and its Stone-free consequences, namely invariance and, for a pure state, irreducibility of the resulting covariant GNS representation (Theorem 127); the future-timelike translation subgroup of the inhomogeneous Lorentz group, which supplies the concrete family of one-parameter subgroups the spectrum condition is to be imposed on (Definition 128); and the vacuum-state definition with this concrete predicate substituted in, leaving no free parameter (Definition 129). - - Proves that purity of a state is preserved by any \*-automorphism and is therefore a Lorentz-covariance-invariant property (Theorem 130). +- **Sharpened Haag–Kastler Axioms in Minkowski spacetime (§10.3, p. 49; §10.3.1, p. 51; §10.3.6, p. 58).** States the sharpened axioms—Local Algebras (Definition 80), Isotony (Definition 81), Local Commutativity (Definition 83), Quasilocal Completeness (Definition 85), and Lorentz Covariance (Definition 86), together with the quasilocal algebra (Definition 82) and quasilocal observables (Definition 84)—bundled into a single `HaagKastlerNet` structure (Definition 87). Derives the operator form of Einstein Causality in a representation (Theorem 88). Then develops the covariance structure: + - Defines covariant families of local states (Definition 136) with their composition law (Lemma 137), and the lift of the fiberwise covariance action to a \*-automorphism of the quasilocal algebra—the `QuasilocalCovarianceAutomorphism` (Definition 138)—and establishes its uniqueness (Lemma 139), existence (Theorem 140), and existence for the trivial net (Theorem 141). This data is bundled into a `CovariantQuasilocalAlgebra` structure (Definition 142), on which the covariance action is a genuine group action (Lemma 143). + - Defines invariant states (Definition 144) and proves GNS-unitary implementation of a Poincaré-invariant state (Theorem 145). + - Proves that a state that is both invariant and pure yields a GNS representation that is simultaneously covariant and irreducible—a necessary precursor to a vacuum representation (Theorem 146). + - Lays a "bounded-generator" scaffold toward the spectrum condition, deliberately sidestepping Stone's theorem and unbounded self-adjoint operators (not yet available for this purpose in Mathlib): positive energy for a bounded generator (Definition 147) together with its basic API—the trivial group has positive energy, the witnessing generator is unique, positive energy is preserved under unitary conjugation, and a positive-energy group is automatically strongly continuous (Theorem 148); a generator-parameterised notion of vacuum state (Definition 149) and its Stone-free consequences, namely invariance and, for a pure state, irreducibility of the resulting covariant GNS representation (Theorem 150); the future-timelike translation subgroup of the inhomogeneous Lorentz group, which supplies the concrete family of one-parameter subgroups the spectrum condition is to be imposed on (Definition 151); and the vacuum-state definition with this concrete predicate substituted in, leaving no free parameter (Definition 152). + - Proves that purity of a state is preserved by any \*-automorphism and is therefore a Lorentz-covariance-invariant property (Theorem 153). -- **Sharpened Haag–Kastler Axioms in curved spacetime (§10.4, §10.4.1, §10.4.4, §10.4.5).** States the curved-spacetime axioms—Local Algebras, Isotony, Local Commutativity, Local Completeness, and Isometric Covariance—bundled into a `HaagKastlerNet` in curved spacetime (Definitions 147–153). Derives the operator form of Einstein Causality relative to a containing local algebra (Theorem 154). Then develops the curved-spacetime covariance structure: - - Defines covariant families of local states in curved spacetime (Definition 170) and proves their composition law (Lemma 171). - - Since no quasilocal algebra exists in a generic Lorentzian spacetime, the covariance action restricts to the stabiliser subgroup $$\mathrm{Stab}(\mathbf{B})$$ of a region—the isometries that fix $$\mathbf{B}$$—defining automorphisms of the single local algebra $$\mathfrak{U}(\mathbf{B})$$ (Definition 172), and proves that this stabiliser action is a genuine group action (Lemma 173). - - Proves that a stabiliser-invariant state carries a unitary GNS representation of $$\mathrm{Stab}(\mathbf{B})$$ (Theorem 174), strongly continuous when the matrix coefficients are continuous (Theorem 175). - - Proves that a state that is both stabiliser-invariant and pure yields an irreducible covariant GNS representation of $$\mathrm{Stab}(\mathbf{B})$$—the curved-spacetime analogue of the precursor to a vacuum representation (Theorem 176). - - Proves that purity of a state on a local algebra is invariant under the stabiliser action (Theorem 177). +- **Sharpened Haag–Kastler Axioms in curved spacetime (§10.4, p. 62; §10.4.1, p. 64; §10.4.4, p. 67; §10.4.5, p. 67).** States the curved-spacetime axioms—Local Algebras (Definition 170), Isotony (Definition 171), Local Commutativity (Definition 172), Local Completeness (Definition 174), and Isometric Covariance (Definition 175), together with local observables (Definition 173)—bundled into a `HaagKastlerNet` in curved spacetime (Definition 176). Derives the operator form of Einstein Causality relative to a containing local algebra (Theorem 177). Then develops the curved-spacetime covariance structure: + - Defines covariant families of local states in curved spacetime (Definition 194) and proves their composition law (Lemma 195). + - Since no quasilocal algebra exists in a generic Lorentzian spacetime, the covariance action restricts to the stabiliser subgroup $$\mathrm{Stab}(\mathbf{B})$$ of a region—the isometries that fix $$\mathbf{B}$$—defining automorphisms of the single local algebra $$\mathfrak{U}(\mathbf{B})$$ (Definition 196), and proves that this stabiliser action is a genuine group action (Lemma 197). + - Proves that a stabiliser-invariant state carries a unitary GNS representation of $$\mathrm{Stab}(\mathbf{B})$$ (Theorem 198), strongly continuous when the matrix coefficients are continuous (Theorem 199). + - Proves that a state that is both stabiliser-invariant and pure yields an irreducible covariant GNS representation of $$\mathrm{Stab}(\mathbf{B})$$—the curved-spacetime analogue of the precursor to a vacuum representation (Theorem 200). + - Proves that purity of a state on a local algebra is invariant under the stabiliser action (Theorem 201). -- **Local von Neumann algebras, irreducibility, and superselection theory (§10.3.2–§10.3.5, §10.4.2–§10.4.3).** This is the largest block, developing the von Neumann algebra layer of the theory in both settings, then the representation-theoretic machinery—irreducibility, purity, unitary equivalence, and direct sums—that sits on top of it: - - *Local algebras and the net.* Defines the local von Neumann algebra $$R(\mathbf{B}) = \pi(\mathfrak{U}(\mathbf{B}))''$$ of a region in a representation (Definitions 70–71 in Minkowski spacetime, Definitions 155–156 in curved spacetime), and proves Microcausality (Theorems 72, 157) and Isotony of the von Neumann net (Theorems 73, 158), together with their bundled forms on Mathlib's `VonNeumannAlgebra` type (Theorems 74, 159). Packages the region-indexed assignment $$\mathbf{B} \mapsto R(\mathbf{B})$$ as an order-preserving map on the poset of regions—the net of von Neumann algebras itself—both for the full quasilocal net in Minkowski spacetime (Definition 75) and, relative to a containing region, in curved spacetime (Definition 160). - - *Statistical independence and geometric covariance.* Proves the Statistical Independence (Schlieder) property: if the cyclic vector of one region is cyclic for its local observables, it is separating for the local von Neumann algebra of any spacelike-separated region (Theorems 76–77 in Minkowski spacetime, Theorems 161–162 in curved spacetime). Proves Geometric Covariance of the von Neumann net: conjugation by the unitary implementing a symmetry carries the local von Neumann algebra of a region onto that of the transformed region, via the covariance representation in Minkowski spacetime (Theorem 78) and via the stabiliser GNS representation in curved spacetime (Theorem 163). As a consequence, being a factor is constant along the orbit of a region under the symmetry (Theorems 79, 164), and the underlying set-level equality upgrades to a first-class \*-algebra isomorphism of the bundled local von Neumann algebras (Theorems 80, 165). - - *Irreducibility, purity, and Schur's Lemma.* Introduces irreducible representations via their commutant (Definition 81) and establishes the Topological Schur Lemma for cyclic representations (Theorem 82), together with the operator-theoretic bridge identifying commutant scalars with coefficients proportional to the state (Theorem 83). Defines pure states (Definition 84) and proves "pure implies irreducible" directly (Theorem 85), then the full equivalence Pure $$\iff$$ Irreducible (Theorem 88) via a GNS Radon–Nikodym theorem that realises every dominated positive functional as an operator in the commutant (Theorems 86–87). Proves that an irreducible representation generates a factor (Theorem 89) and, more sharply, generates the whole of $$\mathcal{B}(H)$$ (Theorem 90), with a bundled density form of this statement on Mathlib's `VonNeumannAlgebra` type (Theorem 91); consequently the GNS representation of a pure state generates a factor (Theorem 92) and, more sharply, the whole of $$\mathcal{B}(H)$$ (Theorem 93). Proves that the norm of any positive linear functional on a unital C\*-algebra equals its value on the unit (Theorem 94), and uses this to establish Pure $$\iff$$ Extreme Point of the state space (Definition 95, Theorem 96), the underlying convexity of the state space and its link to Mathlib's extreme-points API (Theorem 97), and the weak-\* compactness of the state space, which supplies the existence of pure states via Krein–Milman (Theorem 98). Specialises all of the above to the quasilocal algebra $$\mathfrak{U}$$ (Theorems 99–100) and to each local algebra $$\mathfrak{U}(\mathbf{B})$$ in curved spacetime (Theorems 166–168), and additionally registers, per region, the irreducible dichotomy discussed next (Theorem 169). - - *Unitary equivalence and superselection theory.* Defines unitary equivalence of representations as an equivalence relation (Definition 101), and shows irreducibility and factoriality are unitary invariants, transported by the cross-space conjugation induced by the implementing unitary (Theorem 102). Defines disjointness of representations via the vanishing of all intertwiners (Definition 103) and the coarser notion of quasi-equivalence via a \*-isomorphism of generated von Neumann algebras (Definition 104), with unitary equivalence shown to imply quasi-equivalence. Proves Schur's Lemma in the form of the Irreducible Dichotomy: a nonzero intertwiner between two irreducible representations rescales to a unitary equivalence, so two irreducible representations are always either disjoint or unitarily equivalent (Theorem 105)—the foundational trichotomy of superselection theory. Proves the space of intertwiners between two irreducible representations is at most one-dimensional (Lemma 106) and that the endomorphism algebra of an irreducible representation is exactly $$\mathbb{C} \cdot 1$$ (Lemma 107). Applies the dichotomy to GNS representations of pure states to obtain the Pure-State Dichotomy underlying superselection sectors (Theorem 108). - - *Direct sums, amplification, and reducibility.* Defines the direct-sum representation of a family of \*-representations on the $$\ell^2$$-direct sum of their Hilbert spaces (Definition 109), and shows each summand embeds as a subrepresentation whose projection lies in the commutant of the sum (Theorem 110). Defines the $$\iota$$-fold amplification of a single representation as the direct sum of $$\iota$$ copies of itself (Definition 111), and proves a direct sum with at least two nonzero summands is always reducible, so a multiply-amplified representation is never irreducible (Theorem 112). +- **Local von Neumann algebras, irreducibility, and superselection theory (§10.3.2–§10.3.5, pp. 51–58; §10.4.2–§10.4.3, pp. 64–67).** This is the largest block, developing the von Neumann algebra layer of the theory in both settings, then the representation-theoretic machinery—irreducibility, purity, unitary equivalence, and direct sums—that sits on top of it: + - *Local algebras and the net.* Defines the local von Neumann algebra $$R(\mathbf{B}) = \pi(\mathfrak{U}(\mathbf{B}))''$$ of a region in a representation (Definitions 89–90 in Minkowski spacetime, Definitions 178–179 in curved spacetime), and proves Microcausality (Theorems 91, 180) and Isotony of the von Neumann net (Theorems 92, 181), together with their bundled forms on Mathlib's `VonNeumannAlgebra` type (Theorems 93, 182). In curved spacetime the isotony statements carry an explicit coherence hypothesis on the chosen isotony embeddings—that the embedding of a smaller region into a larger one factors through any intermediate region—since the curved axiom selects those embeddings by choice, with no built-in composition law; the hypothesis holds automatically whenever the embeddings form a genuine inclusion family. Packages the region-indexed assignment $$\mathbf{B} \mapsto R(\mathbf{B})$$ as an order-preserving map on the poset of regions—the net of von Neumann algebras itself—both for the full quasilocal net in Minkowski spacetime (Definition 94) and, relative to a containing region, in curved spacetime (Definition 183). + - *Statistical independence, additive-free locality, and geometric covariance.* Proves the Statistical Independence (Schlieder) property: if the cyclic vector of one region is cyclic for its local observables, it is separating for the local von Neumann algebra of any spacelike-separated region (Theorems 95–96 in Minkowski spacetime, Theorems 184–185 in curved spacetime). Proves additive-free locality: for a basis set lying inside the spacelike complement of a region, the local von Neumann algebra of the former lies in the commutant of that of the latter—locality expressed through the spacelike complement without any algebra ever being attached to the unbounded complement itself (Theorem 97 in Minkowski spacetime, Theorem 186 in curved spacetime). Proves Geometric Covariance of the von Neumann net: conjugation by the unitary implementing a symmetry carries the local von Neumann algebra of a region onto that of the transformed region, via the covariance representation in Minkowski spacetime (Theorem 98) and via the stabiliser GNS representation in curved spacetime (Theorem 187, where basis-set preservation and the coherence of the stabiliser action with the chosen isotony embeddings enter as explicit hypotheses, discharged for nets arising from a concrete geometric spacetime). As a consequence, being a factor is constant along the orbit of a region under the symmetry (Theorems 99, 188), and the underlying set-level equality upgrades to a first-class \*-algebra isomorphism of the bundled local von Neumann algebras (Theorems 100, 189). + - *Irreducibility, purity, and Schur's Lemma.* Introduces irreducible representations via their commutant (Definition 101) and establishes the Topological Schur Lemma for cyclic representations (Theorem 102), together with the operator-theoretic bridge identifying commutant scalars with coefficients proportional to the state (Theorem 103). Defines pure states (Definition 104) and proves "pure implies irreducible" directly (Theorem 105), then the full equivalence Pure $$\iff$$ Irreducible (Theorem 108) via a GNS Radon–Nikodym theorem that realises every dominated positive functional as an operator in the commutant (Theorems 106–107). Proves that an irreducible representation generates a factor (Theorem 109) and, more sharply, generates the whole of $$\mathcal{B}(H)$$ (Theorem 110), with a bundled density form of this statement on Mathlib's `VonNeumannAlgebra` type (Theorem 111); consequently the GNS representation of a pure state generates a factor (Theorem 112) and, more sharply, the whole of $$\mathcal{B}(H)$$ (Theorem 113). Proves that the norm of any positive linear functional on a unital C\*-algebra equals its value on the unit (Theorem 114), and uses this to establish Pure $$\iff$$ Extreme Point of the state space (Definition 115, Theorem 116), the underlying convexity of the state space and its link to Mathlib's extreme-points API (Theorem 117), and the weak-\* compactness of the state space, which supplies the existence of pure states via Krein–Milman (Theorem 118). Specialises all of the above to the quasilocal algebra $$\mathfrak{U}$$ (Theorems 119–120) and to each local algebra $$\mathfrak{U}(\mathbf{B})$$ in curved spacetime (Theorems 190–192), and additionally registers, per region, the irreducible dichotomy discussed next (Theorem 193). + - *Unitary equivalence and superselection theory.* Defines unitary equivalence of representations as an equivalence relation (Definition 121), and shows irreducibility and factoriality are unitary invariants, transported by the cross-space conjugation induced by the implementing unitary (Theorem 122). Defines disjointness of representations via the vanishing of all intertwiners (Definition 123) and the coarser notion of quasi-equivalence via a \*-isomorphism of generated von Neumann algebras (Definition 124), with unitary equivalence shown to imply quasi-equivalence. Proves Schur's Lemma in the form of the Irreducible Dichotomy: a nonzero intertwiner between two irreducible representations rescales to a unitary equivalence, so two irreducible representations are always either disjoint or unitarily equivalent (Theorem 125)—the foundational trichotomy of superselection theory. Proves the space of intertwiners between two irreducible representations is at most one-dimensional (Lemma 126) and that the endomorphism algebra of an irreducible representation is exactly $$\mathbb{C} \cdot 1$$ (Lemma 127). Packages the commutant itself as a von Neumann algebra—the self-intertwiner, or gauge, algebra of the representation, which is trivial exactly when the representation is irreducible (Theorem 128)—and proves the double-commutant duality between the generated algebra and the commutant algebra (Theorem 129), from which it follows that the generated algebra is a factor if and only if its commutant is a factor, and that the commutant collapses to the scalars if and only if the generated algebra is all of $$\mathcal{B}(H)$$ (Theorem 130). Applies the dichotomy to GNS representations of pure states to obtain the Pure-State Dichotomy underlying superselection sectors (Theorem 131). + - *Direct sums, amplification, and reducibility.* Defines the direct-sum representation of a family of \*-representations on the $$\ell^2$$-direct sum of their Hilbert spaces (Definition 132), and shows each summand embeds as a subrepresentation whose projection lies in the commutant of the sum (Theorem 133). Defines the $$\iota$$-fold amplification of a single representation as the direct sum of $$\iota$$ copies of itself (Definition 134), and proves a direct sum with at least two nonzero summands is always reducible, so a multiply-amplified representation is never irreducible (Theorem 135). -- **Separating vectors and faithful states (§10.3.7).** Proves that the cyclic vector of a faithful state is also separating for the image of the GNS representation (Theorem 131)—the basic datum of Tomita–Takesaki modular theory. This result holds in any representation reproducing a faithful state, not only the canonical GNS one. +- **Separating vectors and faithful states (§10.3.7, p. 60).** Proves that the cyclic vector of a faithful state is also separating for the image of the GNS representation (Theorem 154)—the basic datum of Tomita–Takesaki modular theory. This result holds in any representation reproducing a faithful state, not only the canonical GNS one. -- **KMS condition and thermal equilibrium (§10.3.8, §10.3.9, §10.4.6).** Introduces one-parameter automorphism groups (Definition 132) and KMS states (Definition 133) as the algebraic characterisation of thermal equilibrium. The main analytical ingredients are: - - The Strip-Liouville Principle (Definition 136): a function continuous and bounded on a closed strip, holomorphic on the open strip, and with equal boundary values on both edges must be constant along the real axis. - - This is proved at positive inverse temperature via a periodic entire extension—the strip Schwarz reflection (Theorem 137)—followed by Liouville's theorem (Theorem 138). +- **KMS condition and thermal equilibrium (§10.3.8, p. 60; §10.3.9, p. 62; §10.4.6, p. 68).** Introduces one-parameter automorphism groups (Definition 155) and KMS states (Definition 156) as the algebraic characterisation of thermal equilibrium. The condition is phrased purely as an analyticity statement about correlation functions, so—unlike the spectrum condition—it needs no unbounded-operator theory (no Stone theorem, no spectral measures). The main analytical ingredients are: + - The Strip-Liouville Principle (Definition 159): a function continuous and bounded on a closed strip, holomorphic on the open strip, and with equal boundary values on both edges must be constant along the real axis. + - This is proved at positive inverse temperature via a periodic entire extension—the strip Schwarz reflection (Theorem 160)—followed by Liouville's theorem (Theorem 161). From these ingredients the following consequences are derived: - - Every KMS state at positive inverse temperature is automatically invariant under the time evolution, via a boundary-coincidence argument (Lemma 135, Theorem 139). - - The analytic completion of a KMS correlation function is unique: any two strip-functions sharing both boundary values agree everywhere on the strip (Theorems 140–141). - - The set of KMS states at fixed temperature and flow is convex (Theorem 134). + - Every KMS state at positive inverse temperature is automatically invariant under the time evolution, via a boundary-coincidence argument (Lemma 158, Theorem 162). + - The analytic completion of a KMS correlation function is unique: any two strip-functions sharing both boundary values agree everywhere on the strip (Theorems 163–164). + - The set of KMS states at fixed temperature and flow is convex (Theorem 157). - In the Minkowski setting, a one-parameter subgroup of the inhomogeneous Lorentz group induces a one-parameter automorphism group on the quasilocal algebra via the covariance lift (Definition 142, Lemma 143), and KMS states for that flow are defined accordingly (Definition 144; convexity Theorem 145). The corresponding zero-temperature ($$\beta \to \infty$$) notion—a ground state for a covariance flow, whose GNS-implementing unitary group has positive energy—is recorded alongside it (Definition 146). + In the Minkowski setting, a one-parameter subgroup of the inhomogeneous Lorentz group induces a one-parameter automorphism group on the quasilocal algebra via the covariance lift (Definition 165, Lemma 166), and KMS states for that flow are defined accordingly (Definition 167; convexity Theorem 168). The corresponding zero-temperature ($$\beta \to \infty$$) notion—a ground state for a covariance flow, whose GNS-implementing unitary group has positive energy—is recorded alongside it (Definition 169). - In the curved-spacetime setting, Killing flows are identified as one-parameter subgroups of the stabiliser of a region, inducing a one-parameter automorphism group on the local algebra $$\mathfrak{U}(\mathbf{B})$$ (Definition 178, Lemma 179). KMS states for a Killing flow are the precise algebraic sense in which the Hartle–Hawking and Gibbons–Hawking states are thermal (Definition 180). A KMS state for a Killing flow at positive inverse temperature automatically carries a strongly continuous one-parameter unitary group on its GNS Hilbert space implementing the flow, yielding the curved-spacetime thermal (equilibrium) representation (Theorem 181; convexity Theorem 182). The corresponding ground state for a Killing flow is recorded alongside it too (Definition 183). + In the curved-spacetime setting, Killing flows are identified as one-parameter subgroups of the stabiliser of a region, inducing a one-parameter automorphism group on the local algebra $$\mathfrak{U}(\mathbf{B})$$ (Definition 202, Lemma 203). KMS states for a Killing flow are the precise algebraic sense in which the Hartle–Hawking and Gibbons–Hawking states are thermal (Definition 204). A KMS state for a Killing flow at positive inverse temperature automatically carries a strongly continuous one-parameter unitary group on its GNS Hilbert space implementing the flow, yielding the curved-spacetime thermal (equilibrium) representation—the analogue of the Minkowski vacuum representation (Theorem 205; convexity Theorem 206). The corresponding ground state for a Killing flow is recorded alongside it too (Definition 207). ## What is Being Formalised -Only the content of Chapter 10 is formalised in Lean. This comprises: +Only the content of Chapter 10 is formalised in Lean. Its declarations are numbered consecutively from Definition 13 through Definition 207, and are listed below grouped by topic. This comprises: ### Definitions @@ -106,53 +121,55 @@ Only the content of Chapter 10 is formalised in Lean. This comprises: - Timelike / Spacelike / Null Vectors (Definition 21), Time Orientation (Definition 25), Future- and Past-Pointing Vectors (Definition 26) - Paths (Definition 31), Curves (Definition 32), Timelike and Causal Smooth Curves (Definition 33), Future- and Past-Oriented Smooth Curves (Definition 34), Oriented Smooth Curve (Definition 36) - Endpoints (Definition 39), Trip (Definition 40), Causal Trip (Definition 41) -- Chronological Future and Chronological Past (Definition 42), Causal Future and Causal Past (Definition 43) -- Spacelike Related (Definition 46), Completely Spacelike (Definition 47) -- Alexandrov Topology (Definition 50), Minkowski Spacetime (Definition 52), Lorentzian Spacetime (Definition 53) +- No Closed Causal Curve — the Causality Condition (Definition 43) +- Chronological Future and Chronological Past (Definition 45), Causal Future and Causal Past (Definition 46) +- Spacelike Related (Definition 49), Completely Spacelike (Definition 50) +- Spacelike Complement of a Region (Definition 53), Causal Closure Operator (Definition 55), Causally Complete Region (Definition 56) +- Alexandrov Topology (Definition 60), Minkowski Spacetime (Definition 64), Lorentzian Spacetime (Definition 65) **Sharpened axioms – Minkowski spacetime** -- Axiom 1: Local Algebras (Definition 61), Axiom 2: Isotony (Definition 62) -- Quasilocal Algebra (Definition 63), Axiom 3: Local Commutativity (Definition 64) -- Quasilocal Observable (Definition 65), Axiom 4: Quasilocal Completeness (Definition 66) -- Axiom 5: Lorentz Covariance (Definition 67), Haag–Kastler Net (Definition 68) -- Covariant Family of Local States (Definition 113), Quasilocal Covariance Automorphism (Definition 115) -- Covariant Quasilocal Algebra (Definition 119), Invariant State (Definition 121) -- Positive Energy for a bounded generator (Definition 124), Vacuum State, generator-parameterised scaffold (Definition 126) -- Future-Timelike Translation Subgroup (Definition 128), Vacuum State with the Concrete Spectrum Condition (Definition 129) +- Axiom 1: Local Algebras (Definition 80), Axiom 2: Isotony (Definition 81) +- Quasilocal Algebra (Definition 82), Axiom 3: Local Commutativity (Definition 83) +- Quasilocal Observable (Definition 84), Axiom 4: Quasilocal Completeness (Definition 85) +- Axiom 5: Lorentz Covariance (Definition 86), Haag–Kastler Net (Definition 87) +- Covariant Family of Local States (Definition 136), Quasilocal Covariance Automorphism (Definition 138) +- Covariant Quasilocal Algebra (Definition 142), Invariant State (Definition 144) +- Positive Energy for a bounded generator (Definition 147), Vacuum State, generator-parameterised scaffold (Definition 149) +- Future-Timelike Translation Subgroup (Definition 151), Vacuum State with the Concrete Spectrum Condition (Definition 152) **Sharpened axioms – curved spacetime** -- Axiom 1: Local Algebras (Definition 147), Axiom 2: Isotony (Definition 148) -- Axiom 3: Local Commutativity (Definition 149), Local Observable (Definition 150) -- Axiom 4: Local Completeness (Definition 151), Axiom 5: Isometric Covariance (Definition 152) -- Haag–Kastler Net in Curved Spacetime (Definition 153) -- Covariant Family of Local States in Curved Spacetime (Definition 170) -- Stabiliser Action on a Local Algebra (Definition 172) -- Killing-Flow Automorphism Family (Definition 178), KMS State for a Killing Flow (Definition 180), Ground State for a Killing Flow (Definition 183) +- Axiom 1: Local Algebras (Definition 170), Axiom 2: Isotony (Definition 171) +- Axiom 3: Local Commutativity (Definition 172), Local Observable (Definition 173) +- Axiom 4: Local Completeness (Definition 174), Axiom 5: Isometric Covariance (Definition 175) +- Haag–Kastler Net in Curved Spacetime (Definition 176) +- Covariant Family of Local States in Curved Spacetime (Definition 194) +- Stabiliser Action on a Local Algebra (Definition 196) +- Killing-Flow Automorphism Family (Definition 202), KMS State for a Killing Flow (Definition 204), Ground State for a Killing Flow (Definition 207) **Local von Neumann algebras and irreducibility** -- Local von Neumann Algebra – Minkowski spacetime (Definition 70) -- $$R(\mathbf{B})$$ as a von Neumann Algebra – Minkowski spacetime (Definition 71) -- The Net of von Neumann Algebras – Minkowski spacetime (Definition 75) -- Local von Neumann Algebra – curved spacetime (Definition 155) -- $$R(\mathbf{B}')$$ as a von Neumann Algebra – curved spacetime (Definition 156) -- The Net of von Neumann Algebras – curved spacetime (Definition 160) -- Irreducible Representation (Definition 81) -- Pure State (Definition 84) -- Extreme Point of the State Space (Definition 95) +- Local von Neumann Algebra – Minkowski spacetime (Definition 89) +- $$R(\mathbf{B})$$ as a von Neumann Algebra – Minkowski spacetime (Definition 90) +- The Net of von Neumann Algebras – Minkowski spacetime (Definition 94) +- Local von Neumann Algebra – curved spacetime (Definition 178) +- $$R(\mathbf{B}')$$ as a von Neumann Algebra – curved spacetime (Definition 179) +- The Net of von Neumann Algebras – curved spacetime (Definition 183) +- Irreducible Representation (Definition 101) +- Pure State (Definition 104) +- Extreme Point of the State Space (Definition 115) **Unitary equivalence and superselection theory** -- Unitary Equivalence of Representations (Definition 101) -- Disjoint Representations (Definition 103) -- Quasi-Equivalence of Representations (Definition 104) +- Unitary Equivalence of Representations (Definition 121) +- Disjoint Representations (Definition 123) +- Quasi-Equivalence of Representations (Definition 124) **Direct sums, amplification, and reducibility** -- Direct-Sum Representation (Definition 109) -- Amplification (Definition 111) +- Direct-Sum Representation (Definition 132) +- Amplification (Definition 134) **KMS condition** -- One-Parameter Automorphism Group (Definition 132), KMS State (Definition 133) -- Strip-Liouville Principle (Definition 136) -- Covariance-Flow Automorphism Family (Definition 142), KMS State for the Covariance Flow (Definition 144), Ground State for a Covariance Flow (Definition 146) +- One-Parameter Automorphism Group (Definition 155), KMS State (Definition 156) +- Strip-Liouville Principle (Definition 159) +- Covariance-Flow Automorphism Family (Definition 165), KMS State for the Covariance Flow (Definition 167), Ground State for a Covariance Flow (Definition 169) ### Lemmas and Theorems @@ -164,101 +181,120 @@ Only the content of Chapter 10 is formalised in Lean. This comprises: **Causal structure** - Causal classification trichotomy (Lemma 22) - Reverse Cauchy–Schwarz inequality for timelike vectors (Lemma 23); reverse triangle inequality (Lemma 24) -- Orientation of pointing vectors is well-defined (Lemma 27); sign lemma for the future cone (Lemma 28); definiteness of the spacelike complement (Lemma 29); convexity of the future and past cones (Lemma 30) +- Orientation of pointing vectors is well-defined (Lemma 27); sign lemma for the future cone (Lemma 28); definiteness of the spacelike complement of a timelike vector (Lemma 29); convexity of the future and past cones (Lemma 30) - Reparametrisation-invariance of the causal type of a curve (Theorem 35); reparametrisation-invariance of future/past orientation (Theorem 37); the forgetful projection from oriented to unoriented curves (Theorem 38) -- Chronological precedence implies causal precedence (Lemma 44) -- Monotonicity of futures and pasts (Lemma 45); symmetry of spacelike separation (Lemma 48) -- Structural properties of complete spacelike separation (Lemma 49); basis sets are Alexandrov-open (Lemma 51); bundled spacelike separation and basis openness (Lemma 54) +- Transitivity of chronological and causal precedence (Theorem 42) +- Irreflexivity and antisymmetry of the causal order under the causality condition (Theorem 44) +- Chronological precedence implies causal precedence (Lemma 47) +- Monotonicity of futures and pasts (Lemma 48); symmetry of spacelike separation (Lemma 51) +- Structural properties of complete spacelike separation (Lemma 52); basis sets are Alexandrov-open (Lemma 61); bundled spacelike separation and basis openness (Lemma 66) + +**Spacelike complement and causal closure** +- Order structure of the spacelike complement: antitone, a region is contained in its double complement, the triple complement collapses, and complementation is the Galois connection attached to the spacelike-separation relation (Lemma 54) +- The causally complete regions form a complete lattice, and the causal complement is an order-reversing involution on it (Theorem 57) +- De Morgan laws for the spacelike complement at the level of underlying sets (Lemma 58) +- Full De Morgan laws—binary and infinitary—for the causal complement on the lattice of causally complete regions (Theorem 59) + +**Alexandrov topology** +- Openness of chronological futures and pasts under a "no endpoints" hypothesis (Lemma 62); unconditional openness of chronological futures and pasts on standard Minkowski spacetime (Lemma 63) +- A point lying in no diamond has only the whole space as a neighbourhood (Lemma 67); the Hausdorff assumption on a Lorentzian spacetime forces the diamonds to cover the space (Lemma 68) +- The Alexandrov diamonds form a topological basis given downward-directedness (Theorem 69) +- Past and future interpolation on standard Minkowski spacetime (Lemmas 70–71); standard Minkowski diamonds are downward-directed (Lemma 72); the Alexandrov diamonds are an unconditional basis on standard Minkowski spacetime (Theorem 73) **Isometry preservation** -- Isometries preserve the causal classification (Lemma 55) -- Unique differentials along a path (Lemma 56); pushforward of a path under an isometry (Lemma 57) -- Isometries preserve chronology (Lemma 58); isometries preserve Alexandrov-basis sets, formalised for the oriented identity component of the isometry group (Lemma 59) -- Axiom 5 basis-set preservation (Lemma 60) +- Isometries preserve the causal classification (Lemma 74) +- Unique differentials along a path (Lemma 75); pushforward of a path under an isometry (Lemma 76) +- Isometries preserve chronology (Lemma 77); isometries preserve Alexandrov-basis sets, formalised for the oriented identity component of the isometry group (Lemma 78) +- Axiom 5 basis-set preservation (Lemma 79) **Covariance – Minkowski spacetime** -- Composition of covariance (Lemma 114) -- Uniqueness of the quasilocal covariance lift (Lemma 116); existence of the quasilocal covariance lift (Theorem 117); existence for the trivial net (Theorem 118) -- Group-action coherence of the covariance automorphism (Lemma 120) -- GNS-unitary implementation of an invariant state (Theorem 122) -- Irreducible covariant GNS representation of a pure invariant state (Theorem 123) -- Positive-Energy API: the trivial group has positive energy, the witnessing generator is unique, positive energy is preserved under unitary conjugation, and a positive-energy group is strongly continuous (Theorem 125) -- No-Stone consequences of a vacuum state: invariance, and (for a pure state) irreducibility of the covariant GNS representation (Theorem 127) -- Purity is covariance-invariant: purity is preserved under pullback by any \*-automorphism, and in particular under the covariance automorphism $$\beta_L$$ (Theorem 130) -- Einstein Causality in a representation (Theorem 69) +- Composition of covariance (Lemma 137) +- Uniqueness of the quasilocal covariance lift (Lemma 139); existence of the quasilocal covariance lift (Theorem 140); existence for the trivial net (Theorem 141) +- Group-action coherence of the covariance automorphism (Lemma 143) +- GNS-unitary implementation of an invariant state (Theorem 145) +- Irreducible covariant GNS representation of a pure invariant state (Theorem 146) +- Positive-Energy API: the trivial group has positive energy, the witnessing generator is unique, positive energy is preserved under unitary conjugation, and a positive-energy group is strongly continuous (Theorem 148) +- No-Stone consequences of a vacuum state: invariance, and (for a pure state) irreducibility of the covariant GNS representation (Theorem 150) +- Purity is covariance-invariant: purity is preserved under pullback by any \*-automorphism, and in particular under the covariance automorphism $$\beta_L$$ (Theorem 153) +- Einstein Causality in a representation (Theorem 88) **Covariance – curved spacetime** -- Composition of covariance in curved spacetime (Lemma 171) -- The stabiliser action is a group action (Lemma 173) -- GNS unitary representation of the stabiliser (Theorem 174); strongly continuous stabiliser GNS unitary (Theorem 175) -- Irreducible covariant GNS representation of a pure invariant state on a local algebra (Theorem 176) -- Purity is invariant under the stabiliser action (Theorem 177) -- Einstein Causality in a representation, curved spacetime (Theorem 154) +- Composition of covariance in curved spacetime (Lemma 195) +- The stabiliser action is a group action (Lemma 197) +- GNS unitary representation of the stabiliser (Theorem 198); strongly continuous stabiliser GNS unitary (Theorem 199) +- Irreducible covariant GNS representation of a pure invariant state on a local algebra (Theorem 200) +- Purity is invariant under the stabiliser action (Theorem 201) +- Einstein Causality in a representation, curved spacetime (Theorem 177) **Local von Neumann algebras – Minkowski spacetime** -- Microcausality: spacelike-separated local von Neumann algebras commute (Theorem 72) -- Isotony of the von Neumann net (Theorem 73) -- Bundled von Neumann microcausality and isotony (Theorem 74) -- Statistical Independence (Schlieder Property): the cyclic vector of one region is separating for the local von Neumann algebra of any spacelike-separated region (Theorems 76–77) -- Geometric Covariance of the von Neumann net: conjugation by the implementing unitary carries the local von Neumann algebra of a region onto that of the transformed region (Theorem 78); orbit-invariance of factoriality along the symmetry orbit (Theorem 79); upgrade to a \*-algebra isomorphism of the bundled local von Neumann algebras (Theorem 80) -- Topological Schur Lemma for cyclic representations (Theorem 82) -- Commutant operator is scalar iff its diagonal coefficient is proportional to the state (Theorem 83) -- Pure state implies irreducible GNS representation (Theorem 85) -- GNS Radon–Nikodym form is bounded (Theorem 86); GNS Radon–Nikodym operator exists and commutes with the representation (Theorem 87) -- Pure state $$\iff$$ irreducible GNS representation (Theorem 88) -- An irreducible representation generates a von Neumann algebra with trivial centre, i.e. a factor (Theorem 89); more sharply, an irreducible representation generates the whole of $$\mathcal{B}(H)$$ (Theorem 90); bundled density form on Mathlib's `VonNeumannAlgebra` type (Theorem 91) -- The GNS representation of a pure state generates a factor (Theorem 92); more sharply, generates the whole of $$\mathcal{B}(H)$$ (Theorem 93) -- Norm of a positive linear functional equals its value on the unit (Theorem 94) -- Pure state $$\iff$$ extreme point of the state space (Theorem 96); state-space convexity and the extreme-point bridge (Theorem 97); weak-\* compactness of the state space (Theorem 98) -- Pure state $$\iff$$ extreme point of the state space of the quasilocal algebra (Theorem 99) -- Pure state $$\iff$$ irreducible GNS representation on the quasilocal algebra (Theorem 100) +- Microcausality: spacelike-separated local von Neumann algebras commute (Theorem 91) +- Isotony of the von Neumann net (Theorem 92) +- Bundled von Neumann microcausality and isotony (Theorem 93) +- Statistical Independence (Schlieder Property): the cyclic vector of one region is separating for the local von Neumann algebra of any spacelike-separated region (Theorems 95–96) +- Additive-free locality via the spacelike complement: locality expressed through $$\mathbf{B}' \subseteq \mathbf{B}^\perp$$, with no algebra attached to the unbounded complement (Theorem 97) +- Geometric Covariance of the von Neumann net: conjugation by the implementing unitary carries the local von Neumann algebra of a region onto that of the transformed region (Theorem 98); orbit-invariance of factoriality along the symmetry orbit (Theorem 99); upgrade to a \*-algebra isomorphism of the bundled local von Neumann algebras (Theorem 100) +- Topological Schur Lemma for cyclic representations (Theorem 102) +- Commutant operator is scalar iff its diagonal coefficient is proportional to the state (Theorem 103) +- Pure state implies irreducible GNS representation (Theorem 105) +- GNS Radon–Nikodym form is bounded (Theorem 106); GNS Radon–Nikodym operator exists and commutes with the representation (Theorem 107) +- Pure state $$\iff$$ irreducible GNS representation (Theorem 108) +- An irreducible representation generates a von Neumann algebra with trivial centre, i.e. a factor (Theorem 109); more sharply, an irreducible representation generates the whole of $$\mathcal{B}(H)$$ (Theorem 110); bundled density form on Mathlib's `VonNeumannAlgebra` type (Theorem 111) +- The GNS representation of a pure state generates a factor (Theorem 112); more sharply, generates the whole of $$\mathcal{B}(H)$$ (Theorem 113) +- Norm of a positive linear functional equals its value on the unit (Theorem 114) +- Pure state $$\iff$$ extreme point of the state space (Theorem 116); state-space convexity and the extreme-point bridge (Theorem 117); weak-\* compactness of the state space (Theorem 118) +- Pure state $$\iff$$ extreme point of the state space of the quasilocal algebra (Theorem 119) +- Pure state $$\iff$$ irreducible GNS representation on the quasilocal algebra (Theorem 120) **Local von Neumann algebras – curved spacetime** -- Microcausality relative to a containing local algebra (Theorem 157) -- Isotony of the curved von Neumann net (Theorem 158) -- Bundled von Neumann microcausality and isotony, curved spacetime (Theorem 159) -- Statistical Independence (Schlieder Property) in curved spacetime (Theorems 161–162) -- Geometric Covariance of the von Neumann net in curved spacetime, via the stabiliser GNS representation (Theorem 163); orbit-invariance of factoriality along the stabiliser orbit (Theorem 164); upgrade to a \*-algebra isomorphism of the bundled local von Neumann algebras (Theorem 165) -- Pure state $$\iff$$ extreme point of the state space of a local algebra (Theorem 166) -- Pure state $$\iff$$ irreducible GNS representation on a local algebra (Theorem 167) -- The GNS representation of a pure state on a local algebra generates a factor and, more sharply, the whole of $$\mathcal{B}(H)$$ (Theorem 168) -- The irreducible dichotomy (Theorem 105) specialised to curved local algebras (Theorem 169) +- Microcausality relative to a containing local algebra (Theorem 180) +- Isotony of the curved von Neumann net, with the isotony-coherence hypothesis made explicit (Theorem 181) +- Bundled von Neumann microcausality and isotony, curved spacetime (Theorem 182) +- Statistical Independence (Schlieder Property) in curved spacetime (Theorems 184–185) +- Additive-free locality via the spacelike complement in curved spacetime (Theorem 186) +- Geometric Covariance of the von Neumann net in curved spacetime, via the stabiliser GNS representation (Theorem 187); orbit-invariance of factoriality along the stabiliser orbit (Theorem 188); upgrade to a \*-algebra isomorphism of the bundled local von Neumann algebras (Theorem 189) +- Pure state $$\iff$$ extreme point of the state space of a local algebra (Theorem 190) +- Pure state $$\iff$$ irreducible GNS representation on a local algebra (Theorem 191) +- The GNS representation of a pure state on a local algebra generates a factor and, more sharply, the whole of $$\mathcal{B}(H)$$ (Theorem 192) +- The irreducible dichotomy (Theorem 125) specialised to curved local algebras (Theorem 193) **Unitary equivalence and superselection theory** -- Irreducibility and factoriality are unitary invariants (Theorem 102) -- Schur's Lemma and the Irreducible Dichotomy: two irreducible representations are disjoint or unitarily equivalent (Theorem 105) -- Schur multiplicity: the intertwiner space between two irreducible representations is at most one-dimensional (Lemma 106) -- The endomorphism algebra of an irreducible representation is $$\mathbb{C} \cdot 1$$ (Lemma 107) -- The Pure-State Dichotomy: the GNS representations of two pure states are disjoint or unitarily equivalent (Theorem 108) +- Irreducibility and factoriality are unitary invariants (Theorem 122) +- Schur's Lemma and the Irreducible Dichotomy: two irreducible representations are disjoint or unitarily equivalent (Theorem 125) +- Schur multiplicity: the intertwiner space between two irreducible representations is at most one-dimensional (Lemma 126) +- The endomorphism algebra of an irreducible representation is $$\mathbb{C} \cdot 1$$ (Lemma 127) +- The commutant packaged as the self-intertwiner (gauge) von Neumann algebra, trivial exactly when the representation is irreducible (Theorem 128) +- Double-commutant duality between the generated algebra and the commutant algebra (Theorem 129) +- A factor and its commutant: each is a factor iff the other is, and the commutant is the scalars iff the generated algebra is all of $$\mathcal{B}(H)$$ (Theorem 130) +- The Pure-State Dichotomy: the GNS representations of two pure states are disjoint or unitarily equivalent (Theorem 131) **Direct sums, amplification, and reducibility** -- Subrepresentations and commutant of a direct sum (Theorem 110) -- Reducibility of a direct sum with at least two nonzero summands, hence of any multiply-amplified representation (Theorem 112) +- Subrepresentations and commutant of a direct sum (Theorem 133) +- Reducibility of a direct sum with at least two nonzero summands, hence of any multiply-amplified representation (Theorem 135) **Separating vectors and faithful states** -- Separating vector of a faithful state (Theorem 131) +- Separating vector of a faithful state (Theorem 154) **KMS condition** -- The KMS state set is convex (Theorem 134) -- Boundary coincidence for $$a = 1$$ (Lemma 135) -- $$i\beta$$-periodic entire extension / strip Schwarz reflection (Theorem 137) -- Strip-Liouville holds for $$\beta > 0$$ (Theorem 138) -- KMS states are invariant (Theorem 139) -- Uniqueness on the strip from boundary values (Theorem 140) -- Uniqueness of the KMS correlation function (Theorem 141) -- A Lorentz one-parameter subgroup induces a one-parameter automorphism group on the quasilocal algebra (Lemma 143) -- Convexity of the covariance-flow KMS states – Minkowski spacetime (Theorem 145) -- A Killing flow induces a one-parameter automorphism group on the local algebra (Lemma 179) -- The Killing-Flow KMS Thermal Representation: a KMS state for a Killing flow at positive inverse temperature carries a strongly continuous one-parameter unitary group on its GNS Hilbert space implementing the flow (Theorem 181) -- Convexity of the Killing-flow KMS states – curved spacetime (Theorem 182) +- The KMS state set is convex (Theorem 157) +- Boundary coincidence for $$a = 1$$ (Lemma 158) +- $$i\beta$$-periodic entire extension / strip Schwarz reflection (Theorem 160) +- Strip-Liouville holds for $$\beta > 0$$ (Theorem 161) +- KMS states are invariant (Theorem 162) +- Uniqueness on the strip from boundary values (Theorem 163) +- Uniqueness of the KMS correlation function (Theorem 164) +- A Lorentz one-parameter subgroup induces a one-parameter automorphism group on the quasilocal algebra (Lemma 166) +- Convexity of the covariance-flow KMS states – Minkowski spacetime (Theorem 168) +- A Killing flow induces a one-parameter automorphism group on the local algebra (Lemma 203) +- The Killing-Flow KMS Thermal Representation: a KMS state for a Killing flow at positive inverse temperature carries a strongly continuous one-parameter unitary group on its GNS Hilbert space implementing the flow (Theorem 205) +- Convexity of the Killing-flow KMS states – curved spacetime (Theorem 206) ### Axioms Axiom 6 (Primitivity) from the original 1964 Haag–Kastler paper is not carried into the sharpened axiom set—see Chapter 8 for the discussion of why it is dropped. The five sharpened axioms below, bundled together as a `HaagKastlerNet`, are what is actually formalised. -**Minkowski spacetime:** Local Algebras (Definition 61), Isotony (Definition 62), Local Commutativity (Definition 64), Quasilocal Completeness (Definition 66), Lorentz Covariance (Definition 67). +**Minkowski spacetime:** Local Algebras (Definition 80), Isotony (Definition 81), Local Commutativity (Definition 83), Quasilocal Completeness (Definition 85), Lorentz Covariance (Definition 86). -**Curved spacetime:** Local Algebras (Definition 147), Isotony (Definition 148), Local Commutativity (Definition 149), Local Completeness (Definition 151), Isometric Covariance (Definition 152). +**Curved spacetime:** Local Algebras (Definition 170), Isotony (Definition 171), Local Commutativity (Definition 172), Local Completeness (Definition 174), Isometric Covariance (Definition 175). ## Contributing diff --git a/lake-manifest.json b/lake-manifest.json index 4f5b2ba..dcd4f35 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -1,11 +1,21 @@ {"version": "1.2.0", "packagesDir": ".lake/packages", "packages": - [{"url": "https://github.com/leanprover/doc-gen4", + [{"url": "https://github.com/leanprover-community/mathlib4", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "81a5d257c8e410db227a6665ed08f64fea08e997", + "name": "mathlib", + "manifestFile": "lake-manifest.json", + "inputRev": "v4.32.0", + "inherited": false, + "configFile": "lakefile.lean"}, + {"url": "https://github.com/leanprover/doc-gen4", "type": "git", "subDir": null, "scope": "", - "rev": "3b5b1c801e32b876edce69678cf7b1952d84ded2", + "rev": "5f906957bf710c7e7be21f2bd8340ae019cfd36a", "name": "«doc-gen4»", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -21,136 +31,126 @@ "inputRev": null, "inherited": false, "configFile": "lakefile.lean"}, - {"url": "https://github.com/leanprover-community/mathlib4", + {"url": "https://github.com/leanprover-community/plausible", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "d568c8c09630de097a046763c17b9ea99f95f950", - "name": "mathlib", - "manifestFile": "lake-manifest.json", - "inputRev": "v4.31.0-rc1", - "inherited": false, - "configFile": "lakefile.lean"}, - {"url": "https://github.com/leanprover/leansqlite", - "type": "git", - "subDir": null, - "scope": "", - "rev": "55ec82f5518ddbbcdc4ad330668b61abb6f028b6", - "name": "leansqlite", + "rev": "e12c1910fe855cbfc38803cd4e55543906d5fa62", + "name": "plausible", "manifestFile": "lake-manifest.json", "inputRev": "main", "inherited": true, - "configFile": "lakefile.lean"}, - {"url": "https://github.com/leanprover/lean4-cli", + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover-community/LeanSearchClient", "type": "git", "subDir": null, - "scope": "", - "rev": "48bdcff4c5fa27e09028f9f330e59baa0d4640cf", - "name": "Cli", + "scope": "leanprover-community", + "rev": "c5d5b8fe6e5158def25cd28eb94e4141ad97c843", + "name": "LeanSearchClient", "manifestFile": "lake-manifest.json", "inputRev": "main", "inherited": true, "configFile": "lakefile.toml"}, - {"url": "https://github.com/fgdorais/lean4-unicode-basic", + {"url": "https://github.com/leanprover-community/import-graph", "type": "git", "subDir": null, - "scope": "", - "rev": "d8780304285a799100ecb492200e5b99248044bd", - "name": "UnicodeBasic", + "scope": "leanprover-community", + "rev": "7e9612bf0b9ee66db3cb5b9988a35afc706f5a12", + "name": "importGraph", "manifestFile": "lake-manifest.json", "inputRev": "main", "inherited": true, - "configFile": "lakefile.lean"}, - {"url": "https://github.com/dupuisf/BibtexQuery", - "type": "git", - "subDir": null, - "scope": "", - "rev": "5d31b64fb703c5d77f6ef4d1fb958f9bdf1ea539", - "name": "BibtexQuery", - "manifestFile": "lake-manifest.json", - "inputRev": "nightly-testing", - "inherited": true, "configFile": "lakefile.toml"}, - {"url": "https://github.com/acmepjz/md4lean", + {"url": "https://github.com/leanprover-community/ProofWidgets4", "type": "git", "subDir": null, - "scope": "", - "rev": "6a3fb240133bcb7e1a066fdc784b3fdc304e3fc5", - "name": "MD4Lean", + "scope": "leanprover-community", + "rev": "6e311e2a844da9b2cc3971187df2fe0066947b93", + "name": "proofwidgets", "manifestFile": "lake-manifest.json", "inputRev": "main", "inherited": true, "configFile": "lakefile.lean"}, - {"url": "https://github.com/leanprover-community/plausible", + {"url": "https://github.com/leanprover-community/aesop", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "d575be693add4fe9cb996968968ce42ce75c5ccd", - "name": "plausible", + "rev": "a7dbf0c63b694e47f425f3dcddbc0e178bb432d3", + "name": "aesop", "manifestFile": "lake-manifest.json", - "inputRev": "main", + "inputRev": "master", "inherited": true, "configFile": "lakefile.toml"}, - {"url": "https://github.com/leanprover-community/LeanSearchClient", + {"url": "https://github.com/leanprover-community/quote4", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "c5d5b8fe6e5158def25cd28eb94e4141ad97c843", - "name": "LeanSearchClient", + "rev": "38d591e778f100aec9762bb582f9c7f55f50e9dc", + "name": "Qq", "manifestFile": "lake-manifest.json", - "inputRev": "main", + "inputRev": "master", "inherited": true, "configFile": "lakefile.toml"}, - {"url": "https://github.com/leanprover-community/import-graph", + {"url": "https://github.com/leanprover-community/batteries", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "6db47de43aa7f516708053ae2fdadd29dd9baaaa", - "name": "importGraph", + "rev": "023ce7d62a0531e22a5331e20b587817a80d49ff", + "name": "batteries", "manifestFile": "lake-manifest.json", "inputRev": "main", "inherited": true, "configFile": "lakefile.toml"}, - {"url": "https://github.com/leanprover-community/ProofWidgets4", + {"url": "https://github.com/leanprover/leansqlite", "type": "git", "subDir": null, - "scope": "leanprover-community", - "rev": "85bb7e7637e84a7d9803be7d954579fdae42c64b", - "name": "proofwidgets", + "scope": "", + "rev": "b61f1cfac14d03094cb3c0e65acd504416e47cad", + "name": "leansqlite", "manifestFile": "lake-manifest.json", - "inputRev": "v0.0.100", + "inputRev": "main", "inherited": true, "configFile": "lakefile.lean"}, - {"url": "https://github.com/leanprover-community/aesop", + {"url": "https://github.com/leanprover/lean4-cli", "type": "git", "subDir": null, - "scope": "leanprover-community", - "rev": "fafca80479ff95e041d84373dda7122adf1295f2", - "name": "aesop", + "scope": "leanprover", + "rev": "88679d088c9720c27ebdf2ba4dafe17341747f94", + "name": "Cli", "manifestFile": "lake-manifest.json", - "inputRev": "v4.31.0-rc1", + "inputRev": "v4.32.0", "inherited": true, "configFile": "lakefile.toml"}, - {"url": "https://github.com/leanprover-community/quote4", + {"url": "https://github.com/fgdorais/lean4-unicode-basic", "type": "git", "subDir": null, - "scope": "leanprover-community", - "rev": "8d33324ee877e9735d2829bc6f1f439e60cf98b1", - "name": "Qq", + "scope": "", + "rev": "3b873385fdbca8b43ee1e3310bf282743091a14d", + "name": "UnicodeBasic", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.lean"}, + {"url": "https://github.com/dupuisf/BibtexQuery", + "type": "git", + "subDir": null, + "scope": "", + "rev": "97ed9112d5b51279509f16fa04037b9b1b8df824", + "name": "BibtexQuery", "manifestFile": "lake-manifest.json", - "inputRev": "v4.31.0-rc1", + "inputRev": "master", "inherited": true, "configFile": "lakefile.toml"}, - {"url": "https://github.com/leanprover-community/batteries", + {"url": "https://github.com/acmepjz/md4lean", "type": "git", "subDir": null, - "scope": "leanprover-community", - "rev": "708b057842c4cd0845fba132bd94b08493f6fc42", - "name": "batteries", + "scope": "", + "rev": "6a3fb240133bcb7e1a066fdc784b3fdc304e3fc5", + "name": "MD4Lean", "manifestFile": "lake-manifest.json", - "inputRev": "v4.31.0-rc1", + "inputRev": "main", "inherited": true, - "configFile": "lakefile.toml"}], + "configFile": "lakefile.lean"}], "name": "physicslib4", "lakeDir": ".lake", "fixedToolchain": false} diff --git a/lakefile.toml b/lakefile.toml index 934f26e..ca52f07 100644 --- a/lakefile.toml +++ b/lakefile.toml @@ -10,12 +10,6 @@ relaxedAutoImplicit = false weak.linter.mathlibStandardSet = true maxSynthPendingDepth = 3 -[[require]] -name = "mathlib" -scope = "leanprover-community" -rev = "v4.31.0-rc1" - - [[require]] name = "checkdecls" git = "https://github.com/PatrickMassot/checkdecls.git" @@ -26,3 +20,8 @@ git = "https://github.com/leanprover/doc-gen4" rev = "main" [[lean_lib]] name = "Physicslib4" + +[[require]] +name = "mathlib" +scope = "leanprover-community" +rev = "v4.32.0" diff --git a/lean-toolchain b/lean-toolchain index 7217ff5..94b9f49 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.31.0-rc1 \ No newline at end of file +leanprover/lean4:v4.32.0