diff --git a/Physicslib4/Geometry/PseudoRiemannian/Basic.lean b/Physicslib4/Geometry/PseudoRiemannian/Basic.lean index c372b32..52bc205 100644 --- a/Physicslib4/Geometry/PseudoRiemannian/Basic.lean +++ b/Physicslib4/Geometry/PseudoRiemannian/Basic.lean @@ -24,9 +24,12 @@ metrics are included. The smoothness condition has the same bundle-section shape ## Main results * `Physicslib4.Geometry.PseudoRiemannianMetric.bijective_val`: at each point, `v ↦ g_x(v, ·)` is - a linear isomorphism `T_xM → T_x*M` (the musical isomorphism). + a linear isomorphism `T_xM → T_x*M` (the musical isomorphism), packaged as `flatEquiv`. +* `Physicslib4.Geometry.PseudoRiemannianMetric.contMDiff_flatEquiv_symm`: `x ↦ ♭_x⁻¹` is a `C^∞` + section of `Hom(T*M, TM)`. -Blueprint reference: `def:pseudo-riemannian-metric`, `lmm:musical-isomorphism`. +Blueprint reference: `def:pseudo-riemannian-metric`, `lmm:musical-isomorphism`, +`lmm:musical-inverse-smooth`. -/ open Bundle @@ -78,6 +81,59 @@ theorem bijective_val [FiniteDimensional ℝ E] (g : PseudoRiemannianMetric I M) exact (Subspace.dual_finrank_eq).symm exact ⟨hinj, (LinearMap.injective_iff_surjective_of_finrank_eq_finrank hrank).1 hinj⟩ +/-- The musical isomorphism `♭_x : T_xM ≃ T_x*M`, `v ↦ g_x(v, ·)`, as a continuous linear +equivalence (`bijective_val`; continuity of the inverse is automatic in finite dimension). + +Blueprint reference: `lmm:musical-isomorphism`. -/ +noncomputable def flatEquiv [FiniteDimensional ℝ E] (g : PseudoRiemannianMetric I M) (x : M) : + TangentSpace I x ≃L[ℝ] (TangentSpace I x →L[ℝ] ℝ) := + haveI : FiniteDimensional ℝ (TangentSpace I x) := inferInstanceAs (FiniteDimensional ℝ E) + (LinearEquiv.ofBijective (g.val x : TangentSpace I x →ₗ[ℝ] (TangentSpace I x →L[ℝ] ℝ)) + (g.bijective_val x)).toContinuousLinearEquiv + +theorem flatEquiv_apply [FiniteDimensional ℝ E] (g : PseudoRiemannianMetric I M) (x : M) + (v : TangentSpace I x) : g.flatEquiv x v = g.val x v := + rfl + +/-- **Smoothness of the inverse musical isomorphism.** The map `x ↦ ♭_x⁻¹` is a `C^∞` section of +the bundle `Hom(T*M, TM)`, whose fibre at `x` is `T_x*M →L[ℝ] T_xM`, stated in the same +bundle-section idiom as the smoothness of `g` itself. + +Blueprint reference: `lmm:musical-inverse-smooth`. -/ +theorem contMDiff_flatEquiv_symm [FiniteDimensional ℝ E] (g : PseudoRiemannianMetric I M) : + ContMDiff I (I.prod 𝓘(ℝ, (E →L[ℝ] ℝ) →L[ℝ] E)) ∞ + (fun x ↦ TotalSpace.mk' ((E →L[ℝ] ℝ) →L[ℝ] E) + (E := fun x ↦ (TangentSpace I x →L[ℝ] ℝ) →L[ℝ] TangentSpace I x) x + ((g.flatEquiv x).symm : (TangentSpace I x →L[ℝ] ℝ) →L[ℝ] TangentSpace I x)) := by + intro x₀ + rw [contMDiffAt_hom_bundle] + refine ⟨contMDiffAt_id, ?_⟩ + have hg := (contMDiffAt_hom_bundle _).1 (g.contMDiff x₀) |>.2 + simp only at hg ⊢ + have h₁ : x₀ ∈ (trivializationAt E (TangentSpace I) x₀).baseSet := + FiberBundle.mem_baseSet_trivializationAt' x₀ + have h₂ : x₀ ∈ (trivializationAt (E →L[ℝ] ℝ) + (fun x ↦ TangentSpace I x →L[ℝ] ℝ) x₀).baseSet := + FiberBundle.mem_baseSet_trivializationAt' x₀ + have hinv := (ContinuousLinearMap.IsInvertible.contDiffAt_map_inverse (𝕜 := ℝ) (n := ∞) + (e := ContinuousLinearMap.inCoordinates E (TangentSpace I) + (E →L[ℝ] ℝ) (fun x ↦ TangentSpace I x →L[ℝ] ℝ) x₀ x₀ x₀ x₀ (g.val x₀)) ?_).contMDiffAt + · refine (hinv.comp x₀ hg).congr_of_eventuallyEq ?_ + filter_upwards [(trivializationAt _ _ x₀).open_baseSet.mem_nhds h₁, + (trivializationAt _ _ x₀).open_baseSet.mem_nhds h₂] with x hx hx' + simp only [Function.comp_apply] + rw [ContinuousLinearMap.inCoordinates_eq hx hx', ContinuousLinearMap.inCoordinates_eq hx' hx] + change _ = ContinuousLinearMap.inverse + (_ ∘L ((g.flatEquiv x : TangentSpace I x →L[ℝ] (TangentSpace I x →L[ℝ] ℝ)) ∘L _)) + simp only [ContinuousLinearMap.inverse_equiv_comp, ContinuousLinearMap.inverse_comp_equiv, + ContinuousLinearMap.inverse_equiv, ContinuousLinearEquiv.symm_symm] + rfl + · rw [ContinuousLinearMap.inCoordinates_eq h₁ h₂] + change ContinuousLinearMap.IsInvertible + (_ ∘L ((g.flatEquiv x₀ : TangentSpace I x₀ →L[ℝ] (TangentSpace I x₀ →L[ℝ] ℝ)) ∘L _)) + exact ContinuousLinearMap.isInvertible_equiv.comp + (ContinuousLinearMap.isInvertible_equiv.comp ContinuousLinearMap.isInvertible_equiv) + end PseudoRiemannianMetric end Geometry diff --git a/Physicslib4/Geometry/PseudoRiemannian/LeviCivita.lean b/Physicslib4/Geometry/PseudoRiemannian/LeviCivita.lean index 466090f..3b0d05e 100644 --- a/Physicslib4/Geometry/PseudoRiemannian/LeviCivita.lean +++ b/Physicslib4/Geometry/PseudoRiemannian/LeviCivita.lean @@ -143,18 +143,6 @@ each point, and the musical isomorphism `flatEquiv` turns it into the desired ` variable (g : PseudoRiemannianMetric I M) -/-- The **musical isomorphism** `v ↦ g_x(v, ·)` as a continuous linear equivalence -(`bijective_val`). - -Blueprint reference: `lmm:musical-isomorphism`. -/ -noncomputable def flatEquiv (x : M) : - TangentSpace I x ≃L[ℝ] (TangentSpace I x →L[ℝ] ℝ) := - haveI : FiniteDimensional ℝ (TangentSpace I x) := inferInstanceAs (FiniteDimensional ℝ E) - (LinearEquiv.ofBijective (g.val x : TangentSpace I x →ₗ[ℝ] TangentSpace I x →L[ℝ] ℝ) - (g.bijective_val x)).toContinuousLinearEquiv - -theorem flatEquiv_apply (x : M) (v : TangentSpace I x) : g.flatEquiv x v = g.val x v := rfl - variable {X Y Z : Π x : M, TangentSpace I x} variable (X Y Z) in diff --git a/blueprint/src/macros/print.tex b/blueprint/src/macros/print.tex index 668fec1..7d711a8 100644 --- a/blueprint/src/macros/print.tex +++ b/blueprint/src/macros/print.tex @@ -26,4 +26,22 @@ \NewDocumentCommand{\proves}{m} {\clist_map_inline:nn{#1}{\vphantom{\ref{##1}}}% \ignorespaces} -\ExplSyntaxOff \ No newline at end of file +\ExplSyntaxOff +% Line breaking for long Lean names and paths (pdf only). Lean identifiers such as +% `Physicslib4.Spectral.Stone.isEssentiallySelfAdjoint_generator` are set with \texttt, +% which TeX never breaks, so they overflow the margin. Allow a break after each `.`, `_` +% and `/` inside \texttt, and give TeX extra stretch before it resorts to an overfull line. +\NewCommandCopy{\bpOrigTexttt}{\texttt} +\ExplSyntaxOn +\tl_new:N \l__bp_texttt_tl +\RenewDocumentCommand{\texttt}{m} + { + \tl_set:Nn \l__bp_texttt_tl {#1} + \tl_replace_all:Nnn \l__bp_texttt_tl {\_} {\_\allowbreak} + \tl_replace_all:Nnn \l__bp_texttt_tl {.} {.\allowbreak} + \tl_replace_all:Nnn \l__bp_texttt_tl {/} {/\allowbreak} + \exp_args:NV \bpOrigTexttt \l__bp_texttt_tl + } +\ExplSyntaxOff +\setlength{\emergencystretch}{3em} +\tolerance=2000 diff --git a/blueprint/src/move b/blueprint/src/move new file mode 100755 index 0000000..7258319 --- /dev/null +++ b/blueprint/src/move @@ -0,0 +1,29 @@ +git mv sections/sec1/1-1_original_haag_kastler_axioms.tex sections/sec1/original-haag-kastler-axioms.tex +git mv sections/sec10/10-1_gns-construction-details.tex sections/sec10/gns-construction-details.tex +git mv sections/sec10/10-2_spacetime.tex sections/sec10/spacetime.tex +git mv sections/sec10/10-3_haag-kastler-axioms.tex sections/sec10/haag-kastler-axioms.tex +git mv sections/sec10/10-4_haag-kastler-axioms-in-curved-spacetime.tex sections/sec10/haag-kastler-axioms-in-curved-spacetime.tex +git mv sections/sec10/10-5_general-covariance-in-curved-spacetime.tex sections/sec10/general-covariance-in-curved-spacetime.tex +git mv sections/sec2/2-1_standard_topology_on_minkowski_space.tex sections/sec2/standard-topology-on-minkowski-space.tex +git mv sections/sec2/2-2_indiscrete_topology_on_minkowski_space.tex sections/sec2/indiscrete-topology-on-minkowski-space.tex +git mv sections/sec2/2-3_euclidean_topology_on_minkowski_space.tex sections/sec2/euclidean-topology-on-minkowski-space.tex +git mv sections/sec2/2-4_alexandrov_topology_on_minkowski_space.tex sections/sec2/alexandrov-topology-on-minkowski-space.tex +git mv sections/sec3/3-1_regions_of_measurement.tex sections/sec3/regions-of-measurement.tex +git mv sections/sec4/4-1_gns_construction.tex sections/sec4/gns-construction.tex +git mv sections/sec4/4-2_isotony.tex sections/sec4/isotony.tex +git mv sections/sec4/4-3_common_unit.tex sections/sec4/common-unit.tex +git mv sections/sec5/5-1_completely_spacelike.tex sections/sec5/completely-spacelike.tex +git mv sections/sec5/5-2_quasilocal_algebra.tex sections/sec5/quasilocal-algebra.tex +git mv sections/sec6/6-1_set_theoretic_union.tex sections/sec6/set-theoretic-union.tex +git mv sections/sec6/6-2_completion_of_the_set_theoretic_union.tex sections/sec6/completion-of-the-set-theoretic-union.tex +git mv sections/sec6/6-3_all_observables_of_interest.tex sections/sec6/all-observables-of-interest.tex +git mv sections/sec7/7-1_inhomogeneous_lorentz_group.tex sections/sec7/inhomogeneous-lorentz-group.tex +git mv sections/sec7/7-2_action_of_the_inhomogeneous_lorentz_groups_identity_component.tex sections/sec7/action-of-the-inhomogeneous-lorentz-groups-identity-component.tex +git mv sections/sec8/8-1_faithful_representations.tex sections/sec8/faithful-representations.tex +git mv sections/sec8/8-2_faithful_and_irreducible_representations.tex sections/sec8/faithful-and-irreducible-representations.tex +git mv sections/sec9/9-1_prologue.tex sections/sec9/prologue.tex +git mv sections/sec9/9-2_axiom_1_local_algebras.tex sections/sec9/axiom-1-local-algebras.tex +git mv sections/sec9/9-3_axiom_2_isotony.tex sections/sec9/axiom-2-isotony.tex +git mv sections/sec9/9-4_axiom_3_local_commutativity.tex sections/sec9/axiom-3-local-commutativity.tex +git mv sections/sec9/9-4_axiom_4_local_algebra.tex sections/sec9/axiom-4-local-algebra.tex +git mv sections/sec9/9-5_axiom_5_isometric_covariance.tex sections/sec9/axiom-5-isometric-covariance.tex diff --git a/blueprint/src/sections/sec10/haag-kastler-axioms-in-curved-spacetime.tex b/blueprint/src/sections/sec10/haag-kastler-axioms-in-curved-spacetime.tex index ab51f97..c663f72 100644 --- a/blueprint/src/sections/sec10/haag-kastler-axioms-in-curved-spacetime.tex +++ b/blueprint/src/sections/sec10/haag-kastler-axioms-in-curved-spacetime.tex @@ -267,7 +267,7 @@ \subsection{Local von Neumann Algebras in Curved Spacetime} \begin{proof} \leanok \uses{def:spacelike-complement, thrm:additive-free-locality, thrm:von-neumann-bundled-order-in-curved-spacetime} - The Galois bridge discharges the spacelike hypothesis, and $L.\mathtt{toAbstractIdentityComponent}$ identifies the concrete and abstract spacelike relations. + The Galois bridge discharges the spacelike hypothesis, and \texttt{L.toAbstractIdentityComponent} identifies the concrete and abstract spacelike relations. \end{proof} \begin{theorem}[Geometric Covariance of the von Neumann Net (Curved Spacetime)] diff --git a/blueprint/src/sections/sec10/spacetime.tex b/blueprint/src/sections/sec10/spacetime.tex index 1344d86..d8e4e30 100644 --- a/blueprint/src/sections/sec10/spacetime.tex +++ b/blueprint/src/sections/sec10/spacetime.tex @@ -8,7 +8,8 @@ \section{Spacetime}\label{sctn:spacetime} \emph{The smoothness clause, precisely.} The metric field is a family of \emph{continuous bilinear forms} $g_x : TM|_x \to_L[\mathbb{R}] TM|_x \to_L[\mathbb{R}] \mathbb{R}$, and ``smooth'' is the field \texttt{contMDiff}, which asserts that $g$ is a $C^\infty$ \emph{section of the bundle of continuous bilinear forms on the tangent bundle} --- the regularity index being $\infty$, on which see the remark on the index below. Writing $E$ for the model space and $I$ for the model with corners of $M$, it reads \begin{align} - \mathtt{ContMDiff}\;I\;\Big(I.\mathtt{prod}\;\mathcal{I}\big(\mathbb{R},\, E \to_L[\mathbb{R}] E \to_L[\mathbb{R}] \mathbb{R}\big)\Big)\;\infty\;\Big(x \mapsto \mathtt{Bundle.TotalSpace.mk'}\;\big(E \to_L[\mathbb{R}] E \to_L[\mathbb{R}] \mathbb{R}\big)\;x\;(g_x)\Big), + &\mathtt{ContMDiff}\;I\;\Big(I.\mathtt{prod}\;\mathcal{I}\big(\mathbb{R},\, E \to_L[\mathbb{R}] E \to_L[\mathbb{R}] \mathbb{R}\big)\Big)\;\infty \notag \\ + &\qquad \Big(x \mapsto \mathtt{Bundle.TotalSpace.mk'}\;\big(E \to_L[\mathbb{R}] E \to_L[\mathbb{R}] \mathbb{R}\big)\;x\;(g_x)\Big), \end{align} the fibre over $x$ being $TM|_x \to_L[\mathbb{R}] TM|_x \to_L[\mathbb{R}] \mathbb{R}$ and the index being $\infty$. @@ -18,7 +19,8 @@ \section{Spacetime}\label{sctn:spacetime} \emph{It is Mathlib's idiom.} The clause is deliberately the shape of the \texttt{contMDiff} field of Mathlib's \texttt{Bundle.ContMDiffRiemannianMetric}, whose own field is \begin{align} - \mathtt{ContMDiff}\;I_B\;\big(I_B.\mathtt{prod}\;\mathcal{I}(\mathbb{R}, F \to_L[\mathbb{R}] F \to_L[\mathbb{R}] \mathbb{R})\big)\;n\;\big(b \mapsto \mathtt{TotalSpace.mk'}\;(F \to_L[\mathbb{R}] F \to_L[\mathbb{R}] \mathbb{R})\;b\;(\mathtt{inner}\;b)\big), + &\mathtt{ContMDiff}\;I_B\;\big(I_B.\mathtt{prod}\;\mathcal{I}(\mathbb{R}, F \to_L[\mathbb{R}] F \to_L[\mathbb{R}] \mathbb{R})\big)\;n \notag \\ + &\qquad \big(b \mapsto \mathtt{TotalSpace.mk'}\;(F \to_L[\mathbb{R}] F \to_L[\mathbb{R}] \mathbb{R})\;b\;(\mathtt{inner}\;b)\big), \end{align} read with $\mathtt{inner}$ replaced by $g$. Matching it verbatim is what makes the whole bundle-section API of \texttt{Mathlib/Geometry/Manifold/VectorBundle/} apply to $g$ without translation. @@ -385,10 +387,13 @@ \section{Spacetime}\label{sctn:spacetime} \begin{lemma}[Smoothness of the Inverse Musical Isomorphism] \label{lmm:musical-inverse-smooth} + \lean{Physicslib4.Geometry.PseudoRiemannianMetric.contMDiff_flatEquiv_symm, Physicslib4.Geometry.PseudoRiemannianMetric.flatEquiv} \uses{lmm:musical-isomorphism} + \leanok The map $x \mapsto \flat_x^{-1}$ of \ref{lmm:musical-isomorphism} is smooth: it is a $C^\infty$ section of the bundle $\mathrm{Hom}(T^*M, TM)$. \end{lemma} \begin{proof} + \leanok \uses{lmm:musical-isomorphism, def:pseudo-riemannian-metric} Work in a local trivialisation of the bundle of bilinear forms: there $x \mapsto \flat_x$ is a $C^\infty$ map into the invertible elements of $E \to_L E^*$ by the smoothness clause of $g$, and inversion of continuous linear equivalences is $C^\infty$ (\texttt{contDiffAt\_map\_inverse}), so the composite $x \mapsto \flat_x^{-1}$ is $C^\infty$ in each trivialisation. \end{proof} @@ -400,7 +405,8 @@ \section{Spacetime}\label{sctn:spacetime} \leanok Let $\nabla$ be a Levi-Civita connection of $g$. For every $x \in M$ and all vector fields $X, Y, Z$ differentiable at $x$, \begin{align} - 2\,g\big(\nabla_X Y, Z\big) = X\,g(Y,Z) + Y\,g(X,Z) - Z\,g(X,Y) + g\big([X,Y],Z\big) - g\big([X,Z],Y\big) - g\big([Y,Z],X\big), + 2\,g\big(\nabla_X Y, Z\big) &= X\,g(Y,Z) + Y\,g(X,Z) - Z\,g(X,Y) \notag \\ + &\qquad + g\big([X,Y],Z\big) - g\big([X,Z],Y\big) - g\big([Y,Z],X\big), \end{align} both sides evaluated at $x$. \end{lemma} @@ -1653,7 +1659,8 @@ \subsection{Pullback metrics and cross-metric isometries} The chain rule to cite is \texttt{mfderiv\_comp\_apply\_of\_eq}, \emph{not} \texttt{mfderiv\_comp} (nor its \texttt{\_apply} form). Its exact shape is \begin{align} - \big(hg : \mathtt{MDifferentiableAt}\;f\text{'s target model}\;g\;y\big) \to \big(hf : \mathtt{MDifferentiableAt}\;f\;x\big) \to \big(hy : f\,x = y\big) \to \mathtt{mfderiv}\,(g \circ f)\,x\,v = \mathtt{mfderiv}\,g\,y\,\big(\mathtt{mfderiv}\,f\,x\,v\big), + &\big(hg : \mathtt{MDifferentiableAt}\;f\text{'s target model}\;g\;y\big) \to \big(hf : \mathtt{MDifferentiableAt}\;f\;x\big) \notag \\ + &\qquad \to \big(hy : f\,x = y\big) \to \mathtt{mfderiv}\,(g \circ f)\,x\,v = \mathtt{mfderiv}\,g\,y\,\big(\mathtt{mfderiv}\,f\,x\,v\big), \end{align} and the base-point argument $hy$ is exactly what is needed here: instantiated at $g := \psi$, $f := \psi.\mathtt{symm}$, base point $\psi(x)$ and $y := x$, it requires $hy : \psi.\mathtt{symm}(\psi\,x) = x$, which is \texttt{Diffeomorph.symm\_apply\_apply}. Without that transport the plain \texttt{mfderiv\_comp} produces the outer factor as $\mathtt{mfderiv}\;\psi\;\big(\psi.\mathtt{symm}(\psi\,x)\big)$, whose value lives in the tangent space at $\psi(\psi.\mathtt{symm}(\psi\,x))$ rather than at $\psi(x)$; those two tangent spaces are propositionally but not definitionally identified, so the composition does not typecheck until the base point has been transported. The \texttt{\_of\_eq} variant is the lemma that takes the transport as an argument and states its conclusion at $y$. @@ -1745,7 +1752,8 @@ \subsection{Pullback metrics and cross-metric isometries} \leanok The assignment $x \mapsto (\psi^*g)_x$ of \ref{def:pullback-metric} satisfies the \texttt{contMDiff} field of \ref{def:spacetime}: it is a section of the bundle of continuous bilinear forms on the tangent bundle of regularity index $\infty$, i.e.\ a $C^\infty$ section, \begin{align} - \mathtt{ContMDiff}\;I\;\Big(I.\mathtt{prod}\;\mathcal{I}\big(\mathbb{R},\, E \to_L[\mathbb{R}] E \to_L[\mathbb{R}] \mathbb{R}\big)\Big)\;\infty\;\Big(x \mapsto \mathtt{Bundle.TotalSpace.mk'}\;\big(E \to_L[\mathbb{R}] E \to_L[\mathbb{R}] \mathbb{R}\big)\;x\;\big((\psi^*g)_x\big)\Big). + &\mathtt{ContMDiff}\;I\;\Big(I.\mathtt{prod}\;\mathcal{I}\big(\mathbb{R},\, E \to_L[\mathbb{R}] E \to_L[\mathbb{R}] \mathbb{R}\big)\Big)\;\infty \notag \\ + &\qquad \Big(x \mapsto \mathtt{Bundle.TotalSpace.mk'}\;\big(E \to_L[\mathbb{R}] E \to_L[\mathbb{R}] \mathbb{R}\big)\;x\;\big((\psi^*g)_x\big)\Big). \end{align} The index is $\infty$: that is what \ref{def:spacetime} demands. @@ -1984,7 +1992,8 @@ \subsection{Pullback metrics and cross-metric isometries} \leanok This is \texttt{mfderivWithin\_comp} for the composite of $\mu$ with $\psi$. Write $P$ for the parameter space of $\mu$ (the inner set), $u$ for the outer set, and keep $s \in P$ for the parameter of the statement; the set and the point must be kept notationally apart, since \texttt{mfderivWithin\_comp} takes both. With that convention its exact hypotheses are \begin{align} - hg &: \mathtt{MDifferentiableWithinAt}\;I'\;I''\;\psi\;u\;(\mu(s)), \qquad hf : \mathtt{MDifferentiableWithinAt}\;I\;I'\;\mu\;P\;s, \\ + hg &: \mathtt{MDifferentiableWithinAt}\;I'\;I''\;\psi\;u\;(\mu(s)), \\ + hf &: \mathtt{MDifferentiableWithinAt}\;I\;I'\;\mu\;P\;s, \\ h &: P \subseteq \mu^{-1}(u), \qquad hxs : \mathtt{UniqueMDiffWithinAt}\;I\;P\;s, \end{align} of which two are easy to overlook. The uniqueness hypothesis is \emph{pointwise} --- a $\mathtt{UniqueMDiffWithinAt}$ at the single parameter $s$, not a $\mathtt{UniqueMDiffOn}$ on the whole of $P$ --- so what \ref{lmm:path-parameter-unique-diff} supplies must be specialised to $s$ and converted, as $(\dots\,s\,hs).\mathtt{uniqueMDiffWithinAt}$. And there is a set side condition $P \subseteq \mu^{-1}(u)$ relating the inner set to the outer one; here $u = \mathtt{univ}$, so it is immediate, and correspondingly the outer derivative is an unrestricted \texttt{mfderiv} obtained by \texttt{mfderivWithin\_univ}. Differentiability of $\mu$ within $P$ comes from its smoothness, and differentiability of $\psi$ from \texttt{Diffeomorph.mdifferentiable} (with side condition $n \neq 0$), which is what the repository template cited below actually uses --- not from \ref{lmm:mfderiv-diffeo-linear-equiv}, which delivers a \texttt{ContinuousLinearEquiv} rather than an $\mathtt{MDifferentiableWithinAt}$ hypothesis. diff --git a/blueprint/src/sections/sec10/spectral-theorems.tex b/blueprint/src/sections/sec10/spectral-theorems.tex index 51570c6..f736f2f 100644 --- a/blueprint/src/sections/sec10/spectral-theorems.tex +++ b/blueprint/src/sections/sec10/spectral-theorems.tex @@ -4596,8 +4596,10 @@ \subsubsection{Spectral Theorem for Bounded Self-Adjoint Operators} \leanok Let $A \in \mathcal{B}(\mathbf{H})$ be self-adjoint, and let $f \mapsto f(A)$ be the bounded Borel functional calculus of Definition~\ref{def:hall-8.8}. Write \begin{align} - \mathcal{F}_1 &\equiv \{ f \text{ bounded, Borel-measurable on } \sigma(A) \mid (fg)(A) = f(A)g(A) \text{ for all } g \in C^0(\sigma(A); \mathbb{R}) \}, \\ - \mathcal{F}_2 &\equiv \{ g \text{ bounded, Borel-measurable on } \sigma(A) \mid (fg)(A) = f(A)g(A) \text{ for all bounded, Borel-measurable } f \}. + \mathcal{F}_1 &\equiv \{ f \text{ bounded, Borel-measurable on } \sigma(A) \mid \notag \\ + &\qquad (fg)(A) = f(A)g(A) \text{ for all } g \in C^0(\sigma(A); \mathbb{R}) \}, \\ + \mathcal{F}_2 &\equiv \{ g \text{ bounded, Borel-measurable on } \sigma(A) \mid \notag \\ + &\qquad (fg)(A) = f(A)g(A) \text{ for all bounded, Borel-measurable } f \}. \end{align} These are distinct from the class $\mathcal{F}$ of Definition~\ref{def:F-class}: the subscripted classes concern \textit{multiplicativity} of the functional calculus, not boundedness of a quadratic form. \end{definition} diff --git a/blueprint/src/sections/sec10/unbounded-spectral-theorems.tex b/blueprint/src/sections/sec10/unbounded-spectral-theorems.tex index c539903..9a6dc90 100644 --- a/blueprint/src/sections/sec10/unbounded-spectral-theorems.tex +++ b/blueprint/src/sections/sec10/unbounded-spectral-theorems.tex @@ -397,7 +397,7 @@ \subsubsection{Unbounded Operators} Our first observation is that the adjoint's graph is always closed, regardless of any hypothesis on $A$; from this, closability of symmetric operators follows immediately. -\begin{proposition}[Closedness of the Adjoint's Graph; Closability of Symmetric Operators] +\begin{proposition}[Closed Graph of the Adjoint; Closability of Symmetric Operators] \label{prpstn:hall-9.8} \lean{Physicslib4.Spectral.Unbounded.isClosable_of_isSymmetric, LinearPMap.adjoint_isClosed} \leanok @@ -755,7 +755,8 @@ \subsubsection{Unbounded Operators} \begin{align} \left< (A-\lambda\mathbf{1})\psi, (A-\lambda\mathbf{1})\psi \right> &= \left< (A-a\mathbf{1})\psi - ib\psi,\ (A-a\mathbf{1})\psi - ib\psi \right> \\ - &= \left< (A-a\mathbf{1})\psi, (A-a\mathbf{1})\psi \right> - ib\left< (A-a\mathbf{1})\psi, \psi \right> + ib \left< \psi, (A-a\mathbf{1})\psi \right> + b^2 \left< \psi, \psi \right>. + &= \left< (A-a\mathbf{1})\psi, (A-a\mathbf{1})\psi \right> - ib\left< (A-a\mathbf{1})\psi, \psi \right> \notag \\ + &\qquad + ib \left< \psi, (A-a\mathbf{1})\psi \right> + b^2 \left< \psi, \psi \right>. \end{align} Here the cross terms arise as follows: expanding the first argument by conjugate-linearity contributes $\overline{(-ib)} = ib$ to the $\psi$-term, and expanding the second by linearity contributes $-ib$; the final term is $\overline{(-ib)}(-ib)\left< \psi,\psi \right> = (ib)(-ib)\left< \psi,\psi\right> = b^2\left<\psi,\psi\right>$. By the symmetry identity just established, $\left< (A-a\mathbf{1})\psi, \psi \right> = \left< \psi, (A-a\mathbf{1})\psi \right>$, so the middle two terms cancel: $-ib\left< (A-a\mathbf{1})\psi, \psi \right> + ib \left< \psi, (A-a\mathbf{1})\psi \right> = -ib\left< \psi, (A-a\mathbf{1})\psi \right> + ib \left< \psi, (A-a\mathbf{1})\psi \right> = 0$. So \begin{align} @@ -3040,9 +3041,8 @@ \subsubsection{Proof of the Spectral Theorem for Unbounded Self-Adjoint Operator For $n \ge 1$ define \begin{align} - F_1 \equiv \big\{ u \in \sigma(U) \;\mid\; \lvert u-1 \rvert \ge 1 \big\} \cup \big( \{1\} \cap \sigma(U) \big), - \qquad - F_n \equiv \left\{ u \in \sigma(U) \;\middle|\; \frac{1}{n} \le \lvert u - 1 \rvert < \frac{1}{n-1} \right\} \ (n \ge 2). + F_1 &\equiv \big\{ u \in \sigma(U) \;\mid\; \lvert u-1 \rvert \ge 1 \big\} \cup \big( \{1\} \cap \sigma(U) \big), \\ + F_n &\equiv \left\{ u \in \sigma(U) \;\middle|\; \frac{1}{n} \le \lvert u - 1 \rvert < \frac{1}{n-1} \right\} \ (n \ge 2). \end{align} These are pairwise disjoint Borel subsets of $\sigma(U)$ with $\bigcup_{n\ge1} F_n = \sigma(U)$: every $u \ne 1$ has $\lvert u-1\rvert > 0$ and so lies in exactly one of the annuli, and $u=1$ has been placed in $F_1$. diff --git a/blueprint/src/web.paux b/blueprint/src/web.paux new file mode 100644 index 0000000..7d7f928 Binary files /dev/null and b/blueprint/src/web.paux differ diff --git a/home_page/guide.md b/home_page/guide.md index 4e7f268..4ffe655 100644 --- a/home_page/guide.md +++ b/home_page/guide.md @@ -13,7 +13,7 @@ The blueprint is 341 pages long and splits cleanly in two. **Chapters 1–9 are mathematical background and are not formalised in Lean.** They motivate and analyse each of the original Haag–Kastler axioms in turn, and then generalise them to curved spacetime. Along the way they cite twelve supporting results, numbered 1 through 12 — Gelfand–Naimark, the Bounded Linear Transformation Theorem, the existence of a Lorentz metric, and so on. These are quoted from the literature where needed; none of them carries a Lean declaration. -**Chapter 10 collects the formalisation-ready content, and it is the content of Chapter 10 that is formalised in Lean.** Its items are numbered consecutively, running from Definition 13 through Definition 676, and comprise **661 declarations in total: 150 definitions, 156 theorems, 252 lemmas, 99 propositions, and 4 corollaries**, mapped onto **1,143 distinct Lean declarations** (where Mathlib already supplies a result, the blueprint names the Mathlib declaration directly). Three further numbered items — Conventions 22, 213 and 260, standing hypotheses of the two spectral-theory sections — share the numbering but are conventions rather than declarations, and are not counted. Chapter 10 is divided into eight top-level sections, §10.1 through §10.8. +**Chapter 10 collects the formalisation-ready content, and it is the content of Chapter 10 that is formalised in Lean.** Its items are numbered consecutively, running from Definition 13 through Definition 676, and comprise **661 declarations in total: 150 definitions, 156 theorems, 252 lemmas, 99 propositions, and 4 corollaries**, mapped onto **1,145 distinct Lean declarations** (where Mathlib already supplies a result, the blueprint names the Mathlib declaration directly). Three further numbered items — Conventions 22, 213 and 260, standing hypotheses of the two spectral-theory sections — share the numbering but are conventions rather than declarations, and are not counted. Chapter 10 is divided into eight top-level sections, §10.1 through §10.8. ## Chapters 1–9: unpacking the original axioms diff --git a/home_page/index.md b/home_page/index.md index 92113cc..9556adc 100644 --- a/home_page/index.md +++ b/home_page/index.md @@ -29,9 +29,9 @@ The blueprint is 341 pages long and splits cleanly in two. **Chapters 1–9 are mathematical background and are not formalised in Lean.** They motivate and analyse each of the original Haag–Kastler axioms in turn, and then generalise them to curved spacetime. Along the way they cite twelve supporting results, numbered 1 through 12 — Gelfand–Naimark, the Bounded Linear Transformation Theorem, the existence of a Lorentz metric, and so on. These are quoted from the literature where needed; none of them carries a Lean declaration. -**Chapter 10 collects the formalisation-ready content, and it is the content of Chapter 10 that is formalised in Lean.** Its items are numbered consecutively, running from Definition 13 through Definition 676, and comprise **661 declarations in total: 150 definitions, 156 theorems, 252 lemmas, 99 propositions, and 4 corollaries**, mapped onto **1,143 distinct Lean declarations** (where Mathlib already supplies a result, the blueprint names the Mathlib declaration directly). Three further numbered items — Conventions 22, 213 and 260, standing hypotheses of the two spectral-theory sections — share the numbering but are conventions rather than declarations, and are not counted. Chapter 10 is divided into eight top-level sections, §10.1 through §10.8. +**Chapter 10 collects the formalisation-ready content, and it is the content of Chapter 10 that is formalised in Lean.** Its items are numbered consecutively, running from Definition 13 through Definition 676, and comprise **661 declarations in total: 150 definitions, 156 theorems, 252 lemmas, 99 propositions, and 4 corollaries**, mapped onto **1,145 distinct Lean declarations** (where Mathlib already supplies a result, the blueprint names the Mathlib declaration directly). Three further numbered items — Conventions 22, 213 and 260, standing hypotheses of the two spectral-theory sections — share the numbering but are conventions rather than declarations, and are not counted. Chapter 10 is divided into eight top-level sections, §10.1 through §10.8. -**660 of the 661 are formalised, statements and proofs alike, and the Lean contains no `sorry`.** The one exception is Lemma 358, which is not yet formalised at all; it is discussed under [Formalisation status](#formalisation-status) below. Of the 511 theorems, lemmas, propositions and corollaries in Chapter 10, 471 carry a written proof in the blueprint; the other 40, in §10.2, §10.3 and §10.4, are standard results quoted from the literature (Heine–Borel, Stone–Weierstrass, dominated convergence, the Bochner integral and the like) that the blueprint states in full but deliberately does not prove. 510 of the 511 proofs are formalised in Lean, including all 40 of the quoted results, which are linked to the Mathlib declarations that supply them. +**All 661 are formalised, statements and proofs alike, and the Lean contains no `sorry`.** Of the 511 theorems, lemmas, propositions and corollaries in Chapter 10, 471 carry a written proof in the blueprint; the other 40, in §10.2, §10.3 and §10.4, are standard results quoted from the literature (Heine–Borel, Stone–Weierstrass, dominated convergence, the Bochner integral and the like) that the blueprint states in full but deliberately does not prove. All 511 proofs are formalised in Lean, including the 40 quoted results, which are linked to the Mathlib declarations that supply them. At a glance, the 661 declarations break down by top-level section as follows (click a section to see its items): @@ -41,11 +41,11 @@ At a glance, the 661 declarations break down by top-level section as follows (cl | [§10.2](sec10-2-spectral.html) | Spectral Theorems (bounded) | 38–155 | 25 | 24 | 27 | 67 | 1 | 144 | 144 | | [§10.3](sec10-3-unbounded.html) | Unbounded Spectral Theorems | 155–235 | 27 | 13 | 50 | 30 | 3 | 123 | 123 | | [§10.4](sec10-4-stone.html) | Stone's Theorem | 235–249 | 3 | 2 | 34 | 2 | 0 | 41 | 41 | -| [§10.5](sec10-5-spacetime.html) | Spacetime and causal structure | 249–286 | 34 | 17 | 86 | 0 | 0 | 137 | 136 | +| [§10.5](sec10-5-spacetime.html) | Spacetime and causal structure | 249–286 | 34 | 17 | 86 | 0 | 0 | 137 | 137 | | [§10.6](sec10-6-haag-kastler.html) | Haag–Kastler Axioms (Minkowski) | 286–327 | 40 | 70 | 49 | 0 | 0 | 159 | 159 | | [§10.7](sec10-7-curved.html) | Haag–Kastler Axioms (curved spacetime) | 327–337 | 17 | 29 | 3 | 0 | 0 | 49 | 49 | | [§10.8](sec10-8-general-covariance.html) | General Covariance | 337–338 | 2 | 0 | 0 | 0 | 0 | 2 | 2 | -| **Total** | | | **150** | **156** | **252** | **99** | **4** | **661** | **660** | +| **Total** | | | **150** | **156** | **252** | **99** | **4** | **661** | **661** | ## Explore @@ -63,13 +63,11 @@ At a glance, the 661 declarations break down by top-level section as follows (cl ## Formalisation status -The blueprint annotates every node with the Lean declarations that realise it, so the status of each node is a matter of record rather than of estimate. There is exactly one node in Chapter 10 that is not formalised, and one further place where the Lean is deliberately differently shaped than the prose. Both are flagged in the blueprint text itself; they are collected here so that they are not discovered by surprise. The project contains no `sorry`. +The blueprint annotates every node with the Lean declarations that realise it, so the status of each node is a matter of record rather than of estimate. Every node in Chapter 10 is formalised. There is one place where the Lean is deliberately shaped differently from the prose; it is flagged in the blueprint text itself and collected here so that it is not discovered by surprise. The project contains no `sorry`. **Recently completed: Stone's Theorem.** The new [§10.4](sec10-4-stone.html) (Definition 289 through Theorem 329, pp. 235–249) proves Stone's Theorem, the correspondence between strongly continuous one-parameter unitary groups and self-adjoint operators, and four new §10.3 nodes supply what it needs: a self-adjoint operator has no proper symmetric extension (Lemma 189), the spectral measure of a self-adjoint operator (Definition 286), its functional calculus (Definition 287), and the agreement of that calculus with the bounded one for bounded functions (Lemma 288). All 39 nodes are formalised and proved; the theorem itself is `Physicslib4.Spectral.Stone.stone` in `Physicslib4/Spectral/Stone/Theorem.lean`. With Stone's Theorem in Lean, positive energy (the spectrum condition behind vacuum and ground states) is now stated with a genuine unbounded generator: a one-parameter unitary group has positive energy when it is strongly continuous and its generator is a positive operator, equivalently $$V(t) = e^{itA}$$ with $$A$$ positive and self-adjoint (Theorem 602, `Physicslib4.AQFT.isPositiveEnergy_iff_exists_exp`). The former bounded-generator restriction is gone, and the project records no remaining restrictions. -**Not yet formalised (one node).** - -- **Lemma 358, "Smoothness of the Inverse Musical Isomorphism."** The node sits in §10.5 (p. 255), in the pseudo-Riemannian layer that precedes the definition of geodesics. It states that the pointwise inverse $$x \mapsto \flat_x^{-1}$$ of the musical isomorphism (Lemma 357) is a smooth section of $$\mathrm{Hom}(T^*M, TM)$$, and the blueprint gives a written proof (in a local trivialisation, inversion of continuous linear equivalences is smooth). It carries no Lean declaration yet. No other node depends on it: the existence and uniqueness of the Levi-Civita connection are formalised without it. +**Recently completed: smoothness of the inverse musical isomorphism.** Lemma 358 (§10.5, p. 255), the last unformalised node, states that $$x \mapsto \flat_x^{-1}$$ is a smooth section of $$\mathrm{Hom}(T^*M, TM)$$. It is formalised as `Physicslib4.Geometry.PseudoRiemannianMetric.contMDiff_flatEquiv_symm` in `Physicslib4/Geometry/PseudoRiemannian/Basic.lean`, following the blueprint: in local trivialisations the coordinate form of $$\flat_x^{-1}$$ is the inverse of the coordinate form of the metric, and inversion of continuous linear maps is smooth. **Recently completed: the von Neumann density theorem.** Theorem 505, "Quasilocal Observables are Strongly Dense in the Bicommutant" (§10.6.2, p. 305), formalised as `Physicslib4.AQFT.HaagKastler.dense_range_in_bicommutant` in `Physicslib4/AQFT/HaagKastler/StrongDensity.lean`, is now proved. Mathlib has the strong operator topology (`PointwiseConvergenceCLM`) and the double commutant property of bundled von Neumann algebras, but not the density theorem itself, so the project proves it locally, following Murphy, Lemma 4.1.4, in the new §10.6.2 (Lemmas 495–504, Definition 498): a closed subspace invariant under an operator and its adjoint has a commuting projection (Lemma 495, in `Physicslib4/Operators/ReducingSubspace.lean`), so the closed cyclic subspace of a vector reduces the representation (Lemma 496) and the one-vector case follows (Lemma 497); a finite amplification $$\pi^\iota$$ on $$\ell^2(\iota; H)$$ (Definition 498, Lemmas 499–502, in `Physicslib4/Operators/DensityTheorem.lean`) carries the bicommutant diagonally into its own bicommutant, which upgrades the one-vector case to finitely many vectors (Lemma 503); and a neighbourhood basis for the strong operator topology (Lemma 504) turns that into density. The Kaplansky density theorem, which would additionally keep approximants self-adjoint and norm-bounded, remains out of scope; nothing in the project needs it. diff --git a/home_page/sec10-3-unbounded.md b/home_page/sec10-3-unbounded.md index 95b16c6..b2e499e 100644 --- a/home_page/sec10-3-unbounded.md +++ b/home_page/sec10-3-unbounded.md @@ -55,7 +55,7 @@ Each blueprint subsection below is collapsed; click a heading to see its items. §10.3.1 · Unbounded Operators › Elementary Properties of Adjoints and Closed Operators (p. 164) — 14 items - [**Definition 185**](https://physicslib.github.io/physicslib4/blueprint/chptr-haag-kastler-axioms-blueprint.html#def:closed-linear-map-on-a-subspace) — Closed Linear Map on a Subspace · `LinearPMap.IsClosed` (+1 more) -- [**Proposition 186**](https://physicslib.github.io/physicslib4/blueprint/chptr-haag-kastler-axioms-blueprint.html#prpstn:hall-9.8) — Closedness of the Adjoint's Graph; Closability of Symmetric Operators · `Physicslib4.Spectral.Unbounded.isClosable_of_isSymmetric` (+1 more) +- [**Proposition 186**](https://physicslib.github.io/physicslib4/blueprint/chptr-haag-kastler-axioms-blueprint.html#prpstn:hall-9.8) — Closed Graph of the Adjoint; Closability of Symmetric Operators · `Physicslib4.Spectral.Unbounded.isClosable_of_isSymmetric` (+1 more) - [**Proposition 187**](https://physicslib.github.io/physicslib4/blueprint/chptr-haag-kastler-axioms-blueprint.html#prpstn:hall-9.10) — The Adjoint of a Closure · `Physicslib4.Spectral.Unbounded.adjoint_closure_eq_adjoint` - [**Lemma 188**](https://physicslib.github.io/physicslib4/blueprint/chptr-haag-kastler-axioms-blueprint.html#lmm:extension-reverses-adjoint-domains) — Extension Reverses Adjoint Domains · `Physicslib4.Spectral.Unbounded.adjoint_le_adjoint_of_le` - [**Lemma 189**](https://physicslib.github.io/physicslib4/blueprint/chptr-haag-kastler-axioms-blueprint.html#lmm:self-adjoint-maximally-symmetric) — A Self-Adjoint Operator has no Proper Symmetric Extension · `Physicslib4.Spectral.Unbounded.eq_of_isSelfAdjoint_of_isSymmetric_of_le` diff --git a/home_page/sec10-5-spacetime.md b/home_page/sec10-5-spacetime.md index 0a03dd6..54f2beb 100644 --- a/home_page/sec10-5-spacetime.md +++ b/home_page/sec10-5-spacetime.md @@ -12,7 +12,7 @@ usemathjax: true 137 items (Definitions 330–466), building the entire causal and topological apparatus the axioms are indexed on. The trips underlying the chronological and causal relations $$\ll$$ and $$\prec$$ are genuine geodesics of the Levi-Civita connection of the metric, which the section constructs for an arbitrary pseudo-Riemannian metric on top of Mathlib's covariant derivatives (Mathlib itself has only a Riemannian Levi-Civita connection and no geodesics). It proceeds in nine layers. - *Spacetime, tangent-vector causality, and curves (pp. 249–254, items 330–353).* Gives precise definitions of spacetime (Definition 330) and standard Minkowski spacetime (Definition 331); classifies tangent vectors as timelike, spacelike, or null (Definition 332) and proves the trichotomy (Lemma 333), the reverse Cauchy–Schwarz and reverse triangle inequalities for timelike vectors (Lemmas 334–335), and the cone geometry—orientation of pointing vectors, the sign lemma, definiteness of the spacelike complement of a timelike vector, and convexity of the cones (Lemmas 338–341)—alongside time orientations (Definition 336) and future- and past-pointing vectors (Definition 337). Then paths, curves, and oriented curves are defined as equivalence classes of paths up to reparametrisation (Definitions 342–347), with causal type and future/past orientation each shown well-defined on the quotient (Theorems 346 and 348) and a forgetful projection from oriented to unoriented curves (Theorem 349). Endpoints (Definition 350), shown to be well defined on curves and smooth curves (Lemma 351), come with two point-set lemmas—an extremal parameter lies in the frontier, and two endpoints force a compact parameter interval (Lemmas 352–353). -- *The Levi-Civita connection and geodesics (pp. 254–258, items 354–369).* A new layer. Pseudo-Riemannian metrics (Definition 354) are smooth, symmetric, non-degenerate families of bilinear forms, with no signature condition, so everything here applies to every spacetime. Covariant derivatives are Mathlib's `IsCovariantDerivativeOn`; metric compatibility and the Levi-Civita condition (compatible and torsion-free) are defined on top of them (Definitions 355–356). The musical isomorphism $$v \mapsto g_x(v, \cdot)$$ is a linear isomorphism at each point (Lemma 357); the smoothness of its inverse (Lemma 358) is stated and proved in the blueprint but is the one node of the layer not yet formalised, and nothing depends on it. The Koszul formula (Lemma 359), the tensoriality of the Koszul expression (Lemma 360), and the verification that the Koszul connection is a covariant derivative (Lemma 361) that is Levi-Civita (Lemma 362) give existence and uniqueness of the Levi-Civita connection (Theorem 363). Five lemmas about smooth paths—a function vanishing along a path has zero derivative along it, the covariant derivative along a curve is local, local vector fields globalise, a smooth path has a local left inverse, and its velocity extends to a smooth vector field (Lemmas 364–368)—make the geodesic condition chart-free, well defined and non-vacuous. A geodesic (Definition 369) is then an affinely parametrised smooth path $$\mu$$ with $$(\nabla_X X)(\mu(s)) = 0$$ at every interior parameter, for every smooth vector field $$X$$ extending the velocity near $$s$$. +- *The Levi-Civita connection and geodesics (pp. 254–258, items 354–369).* A new layer. Pseudo-Riemannian metrics (Definition 354) are smooth, symmetric, non-degenerate families of bilinear forms, with no signature condition, so everything here applies to every spacetime. Covariant derivatives are Mathlib's `IsCovariantDerivativeOn`; metric compatibility and the Levi-Civita condition (compatible and torsion-free) are defined on top of them (Definitions 355–356). The musical isomorphism $$v \mapsto g_x(v, \cdot)$$ is a linear isomorphism at each point (Lemma 357), and its inverse is a smooth section of $$\mathrm{Hom}(T^*M, TM)$$ (Lemma 358). The Koszul formula (Lemma 359), the tensoriality of the Koszul expression (Lemma 360), and the verification that the Koszul connection is a covariant derivative (Lemma 361) that is Levi-Civita (Lemma 362) give existence and uniqueness of the Levi-Civita connection (Theorem 363). Five lemmas about smooth paths—a function vanishing along a path has zero derivative along it, the covariant derivative along a curve is local, local vector fields globalise, a smooth path has a local left inverse, and its velocity extends to a smooth vector field (Lemmas 364–368)—make the geodesic condition chart-free, well defined and non-vacuous. A geodesic (Definition 369) is then an affinely parametrised smooth path $$\mu$$ with $$(\nabla_X X)(\mu(s)) = 0$$ at every interior parameter, for every smooth vector field $$X$$ extending the velocity near $$s$$. - *Trips, futures and pasts (pp. 258–260, items 370–378).* Trips and causal trips (Definitions 370–371) are finite chains of future-oriented timelike (respectively causal) geodesic segments, geodesic in the sense of Definition 369, with matching past and future endpoints. Chronological and causal precedence are transitive (Theorem 372); the causality condition (Definition 373) makes them a strict partial order (Theorem 374); and chronological and causal futures and pasts (Definitions 375–376) come with their basic inclusion and monotonicity properties (Lemmas 377–378). - *§10.5.1 Causal diamonds (p. 260, items 379–393).* Introduces the causal diamond $$J^+(p) \cap J^-(q)$$ and the chronological (Alexandrov) diamond $$I^+(p) \cap I^-(q)$$ (Definition 379), with the structural properties of the causal diamond—monotonicity under endpoint spread, causal convexity, and that nonemptiness forces $$p \prec q$$ (Lemma 380)—and the containment of chronological diamonds in causal ones, together with the identification of the Alexandrov basis as exactly the chronological diamonds (Theorem 381). It then develops spacelike separation of points and of regions (Definitions 382–383, Lemmas 384–385), the spacelike complement $$\mathbf{B}^\perp$$ (Definition 386) and its order structure—antitone, extensive on the double complement, with the triple complement collapsing, making complementation the Galois connection attached to the spacelike-separation relation (Lemma 387). The double complement is packaged as the causal closure operator (Definition 388, Lemma 389), whose fixed points are the causally complete regions (Definition 390). These form a complete lattice—meets are intersections, joins are causal closures of unions—on which the causal complement is an order-reversing involution (Theorem 391); the set-level De Morgan laws (Lemma 392) then lift to full binary and infinitary De Morgan laws on the lattice (Theorem 393). The blueprint is careful to record 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. - *§10.5.2 Causal convexity (p. 264, items 394–396).* Defines a causally convex region as one containing every point causally between two of its own points (Definition 394), shows causal diamonds are causally convex (Lemma 395), and shows every spacelike complement—hence every causally complete region—is causally convex (Theorem 396). @@ -58,7 +58,7 @@ Each blueprint subsection below is collapsed; click a heading to see its items. - [**Definition 355**](https://physicslib.github.io/physicslib4/blueprint/chptr-haag-kastler-axioms-blueprint.html#def:metric-compatible-connection) — Covariant Derivative; Metric Compatibility · `Physicslib4.Geometry.CovariantDerivative.IsMetricCompatibleWith` - [**Definition 356**](https://physicslib.github.io/physicslib4/blueprint/chptr-haag-kastler-axioms-blueprint.html#def:levi-civita-connection) — Levi-Civita Connection · `Physicslib4.Geometry.CovariantDerivative.IsLeviCivitaFor` - [**Lemma 357**](https://physicslib.github.io/physicslib4/blueprint/chptr-haag-kastler-axioms-blueprint.html#lmm:musical-isomorphism) — Musical Isomorphism · `Physicslib4.Geometry.PseudoRiemannianMetric.bijective_val` -- [**Lemma 358**](https://physicslib.github.io/physicslib4/blueprint/chptr-haag-kastler-axioms-blueprint.html#lmm:musical-inverse-smooth) — Smoothness of the Inverse Musical Isomorphism *(not yet formalised: no Lean declaration — see [Formalisation status](./#formalisation-status))* +- [**Lemma 358**](https://physicslib.github.io/physicslib4/blueprint/chptr-haag-kastler-axioms-blueprint.html#lmm:musical-inverse-smooth) — Smoothness of the Inverse Musical Isomorphism · `Physicslib4.Geometry.PseudoRiemannianMetric.contMDiff_flatEquiv_symm` (+1 more) - [**Lemma 359**](https://physicslib.github.io/physicslib4/blueprint/chptr-haag-kastler-axioms-blueprint.html#lmm:koszul-formula) — Koszul Formula · `Physicslib4.Geometry.CovariantDerivative.IsLeviCivitaFor.koszul` - [**Lemma 360**](https://physicslib.github.io/physicslib4/blueprint/chptr-haag-kastler-axioms-blueprint.html#lmm:koszul-expression-tensorial) — Tensoriality of the Koszul Expression · `Physicslib4.Geometry.PseudoRiemannianMetric.tensorialAt_koszulAux₁` (+2 more) - [**Lemma 361**](https://physicslib.github.io/physicslib4/blueprint/chptr-haag-kastler-axioms-blueprint.html#lmm:koszul-connection-is-covariant-derivative) — The Koszul Connection is a Covariant Derivative · `Physicslib4.Geometry.PseudoRiemannianMetric.isCovariantDerivativeOn_leviCivitaAux`