Timelike tube theorem

[kencyke]

Timelike Tube Theorem — formalization prerequisites

Survey of the mathematical tools needed to formalize the timelike tube theorem
in Lean 4 + Mathlib, checked against three sources:

code	source	status
ML	Mathlib (already in this lake project, .lake/packages/mathlib)	active
QS	QuantumSystem (this repository, QuantumSystem/)	active
OSR	xiyin137/OSreconstruction — Lean 4, OS reconstruction (Euclidean → Wightman)	active, ~55 sorries / 11 axioms

Symbols: ✓ available, ◐ partial / scaffolding only, ✗ absent.

Two flavours of "timelike tube theorem"

The phrase "timelike tube theorem" refers to two mathematically distinct
statements that share the name:

flavour	sources	setting	proof technique
Minkowski (flat)	Borchers 1961 [Bor61], Araki 1963 [Ara63]	ℝ^{1,3} + quadratic form η = diag(-1,+1,+1,+1), Wightman fields	tube domains in ℂ⁴ + Bargmann–Hall–Wightman + edge-of-wedge + Asgeirsson mean-value
Curved (Lorentzian)	Strohmaier 2000 [Str00] (Klein–Gordon), Strohmaier–Witten 2023 [arXiv:2302.02709] (analytic states)	globally hyperbolic Lorentzian manifold (M, g) with metric locally analytic in time	analytic wavefront set + microlocal Holmgren unique continuation

The flat-Minkowski Borchers statement is

Let Φ be a Wightman field on ℝ^{1,3} and O ⊂ ℝ^{1,3} open with non-empty
causal complement. Then R(O) = R(causal-completion(O)), where
R(O) = π(A(O))″ is the local von Neumann algebra.

The curved Strohmaier–Witten statement (Theorem 5.3) is

Let (Φ, D ⊂ H) be a QFT on a real-analytic globally hyperbolic spacetime
and Ω an analytic vector with AΩ dense (graph topology). Then for every
open O ⊂ M, R(E_T(O)) = R(O), where E_T(O) is the timelike tube
envelope of O.

Crucially, the flat case does not need Lorentzian manifold theory.
"Lorentz invariance" in Borchers/Araki refers to O(1,3) ⊂ GL(4,ℝ) acting
linearly on ℝ⁴; it is not a frame-bundle / pseudo-Riemannian-manifold
construct. This separates the prerequisite stacks of the two flavours.

Layer 1a — Flat Minkowski geometry (Borchers/Araki path)

primitive	ML	QS	OSR	notes
ℝ^{1,3} as inner-product space	✓ via EuclideanSpace, BilinForm	✗	✓ Wightman/Spacetime/MinkowskiGeometry.lean	OSR has explicit Lorentzian quadratic form
Minkowski quadratic form η (signature −+++)	✗ as named class	✗	✓	OSR MinkowskiGeometry.Metric
Lorentz group O(1,3)	✗	✗	✓ via ComplexLieGroups	OSR develops complex Lorentz too
Poincaré group O(1,3) ⋉ ℝ⁴	✗	✗	✓	OSR Wightman covariance
timelike / spacelike / null separation predicates	✗	✗	✓	quadratic-form sign
forward / backward light cone V^±	✗	✗	✓ BHWCore.ForwardTube (cone in ℝ⁴ + tube in ℂ⁴)	OSR core
forward tube T_+ = ℝ⁴ + iV^+ ⊂ ℂ⁴	✗	✗	✓ BHWCore.ForwardTube	OSR core
extended tube T'_+ = ⋃_{Λ ∈ L_+(ℂ)} Λ T_+	✗	✗	✓ BHWCore	Bargmann–Hall–Wightman
permuted extended tube	✗	✗	✓	Wightman analytic continuation
edge-of-wedge theorem (distributional)	✗	✗	✓ SCV/EdgeOfWedge.lean + LocalContinuousEOW, LocalDistributionalEOW	OSR substantial
tube boundary values	✗	✗	✓ SCV/TubeBoundaryValues.lean, TubeDomainExtension.lean	OSR substantial
Bargmann–Hall–Wightman	✗	✗	✓ BHWCore.lean	OSR substantial
causal complement O^⊥ (flat)	✗	✗	✓ via O(1,3)-invariant quadratic form	derivable directly from η
Asgeirsson mean-value theorem	✗	✗	✗	classical, but not yet in Lean — needed for Borchers's wedge argument

Verdict (1a). OSR is substantially populated for the flat-Minkowski
flavour. The blocker on Route B is Asgeirsson mean-value theorem (a
PDE result on the wave equation in ℝ^{1,d-1}) plus stitching the existing
OSR pieces into a Borchers timelike-tube statement.

Layer 1b — Curved Lorentzian / causal geometry (Strohmaier–Witten path)

primitive	ML	QS	OSR	notes
smooth manifold	✓ IsManifold (Mathlib.Geometry.Manifold.IsManifold.Basic)	✗	✗	base infrastructure exists
Lorentzian metric (variable)	✗	✗	✗	green field; pseudo-Riemannian absent
time orientation	✗	✗	✗	absent
causal / timelike / null tangent vector	✗	✗	✗	follows from metric
chronological future I^±(S)	✗	✗	✗	required for §2 of math-ph/0008043
causal future J^±(S)	✗	✗	✗	core primitive
domain of dependence D(S), D^±(S)	✗	✗	✗	core primitive
causal complement O^⊥ (curved)	✗	✗	✗	required by Sanders 0801.4676 §2
Cauchy surface	✗	✗	✗	central; Bernal–Sánchez smoothness theorem also absent
globally hyperbolic spacetime	✗	✗	✗	central; carries the entire curved theorem
causally convex (cc-) region	✗	✗	✗	needed for BFV (math-ph/0112041) categorical setup
smooth timelike curve segment	◐ ContDiffOn only	✗	✗	once metric exists, definable directly
C^1 topology on curve space C(p,q)	✗	✗	✗	math-ph/0008043 §2.3 — sup-metric on γ̇
connected component C_0(p,q,γ)	◐ generic ConnectedComponents ✓	✗	✗	reuses topological machinery
deformation set I_0(p,q,γ)	✗	✗	✗	union of γ̃((0,1)) over C_0(p,q,γ)
envelope E(O) (math-ph/0008043)	✗	✗	✗	smallest set closed under (1) Cauchy development (2) timelike-deformation closure
timelike tube envelope E_T(O) (Strohmaier–Witten)	✗	✗	✗	curve-space variant of E(O)
causal envelope E_c(O)	✗	✗	✗	smallest set ⊇ E_T(O) ∪ D(O)

Verdict (1b). Layer 1b is virtually empty across all three sources.
This is the principal blocker for the curved flavour. OSR's BHWCore
tube-domain machinery sits in ℂⁿ (several complex variables) and does
not transfer to curved Lorentzian manifolds.

Layer 2 — Wave equation / propagators on (M, g)

Mathematical layer between geometry and algebra. The Klein–Gordon Cauchy
problem and the propagators E^±, E produce the symplectic space (R, σ)
that gets quantised. Required by both flavours: in the flat case,
the same R = E(C₀^∞) underlies the CCR algebra of the Klein–Gordon
field on Minkowski; in the curved case, on (M, g).

primitive	ML	QS	OSR	notes
distributions D'(M) (manifold)	◐ Distribution (abstract dual)	✗	◐ on S(ℝⁿ)	OSR uses Schwartz tempered distributions
Schwartz space S(ℝⁿ)	✓ SchwartzMap	✗	✓	mathlib infrastructure mature
nuclear topology / Minlos	✗	✗	✓	needed for some state constructions
flat Klein–Gordon (□ + m²) on Minkowski	✗	✗	◐ via Wightman 2-pt function	needed by Phase 1 (Minkowski)
curved Klein–Gordon (□_g + m² + ξR)	✗	✗	✗	needs scalar curvature R and covariant derivative — Mathlib has LeviCivita for Riemannian only
wave-equation Cauchy problem (flat)	✗	✗	✗	constant-coefficient, comparatively tractable
wave-equation Cauchy problem (curved)	✗	✗	✗	hyperbolic PDE Cauchy theory absent
advanced / retarded fundamental solutions E^± (flat)	✗	✗	✗	explicit formula on Minkowski
advanced / retarded fundamental solutions E^± (curved)	✗	✗	✗	central; constructively requires PDE Cauchy theory
Pauli–Jordan commutator E = E^+ − E^-	✗	✗	✗	required as covariance of CCR algebra
symplectic form σ(Ef, Eh) = ∫ f·Eh dμ_g on R = E(C₀^∞)	✗	✗	✗	Mathlib has bilinear forms but no SymplecticForm class
Asgeirsson mean-value theorem (flat wave eq)	✗	✗	✗	needed for Borchers's flat proof
Holmgren uniqueness theorem (analytic)	✗	✗	✗	absent — needed for math-ph/0008043 Theorem 3.2
Tataru / Hörmander partial-analyticity unique continuation	✗	✗	✗	the heart of math-ph/0008043 proof — out of reach

Verdict (2). Mathlib provides the Schwartz / distribution scaffolding,
but neither the Lorentzian PDE side nor the unique-continuation theorems
exist. Asgeirsson (flat wave equation) is the simplest gap to close
for Phase 1.

Layer 3 — Microlocal analysis (the proof technique of arXiv:2302.02709)

Layer the Strohmaier–Witten paper introduces specifically to bypass modular
theory for the curved flavour. Not needed for the Minkowski flavour
(Borchers/Araki use tube-domain analytic continuation instead).

primitive	ML	QS	OSR	notes
FBI transform T_h	✗	✗	✗	Hörmander Vol I material
smooth wavefront set WF(u)	✗	✗	✗	needed even for Hadamard
analytic wavefront set WF_a(u)	✗	✗	✗	central; controls singularity propagation
microsupport (semi-classical)	✗	✗	✗	parameter-h family version
Hörmander product theorem WF(u·v) ⊂ WF(u) + WF(v)	✗	✗	✗	absent
microlocal Holmgren unique continuation (Prop. D.1, D.2 of 2302.02709)	✗	✗	✗	central — yields R(E_T(O)) = R(O) in the curved case
microlocal spectrum condition / Hadamard via WF	✗	✗	✗	Radzikowski 1996

Verdict (3). Microlocal analysis is completely missing from all three
sources. This is a Hörmander-style analysis library that does not yet
exist in any Lean ecosystem. Phase 2 only.

Layer 4 — Operator algebras

The strongest existing layer. The bicommutant R(O) = π_ω(A(O))″ and the
GNS Hilbert space are needed to state both flavours of the theorem at all.

primitive	ML	QS	OSR	notes
C*-algebra	✓ CStarAlgebra (Mathlib.Analysis.CStarAlgebra.Classes)	✓ extended	—	reuse mathlib
*-algebra	✓ StarAlgebra	✓	—
Hilbert space	✓ HilbertSpace (Mathlib.Analysis.InnerProductSpace.Defs)	✓	—
von Neumann algebra	✓ VonNeumannAlgebra (Mathlib.Analysis.VonNeumannAlgebra.Basic)	✓	✓ extended	OSR has its own development
commutant / bicommutant A″	✓ commutant_commutant	✓ hard half via WOT	✓	QS has WOTClosedSubalgebra.doubleCommutant_eq_of_isWOTClosed
WOT / SOT topology	✗	✓ WOTClosedSubalgebra etc.	✗	QS-original, candidate for upstreaming
GNS construction	✗	✓ GNS.Representation, faithfulness, direct sum, Gelfand–Naimark	✗	QS-original
cyclic vector	✗	◐ cyclicVector_decomp_of_isClosed	✗	property; explicit IsCyclic predicate not yet abstracted
separating vector	✗	✗	✓ via Tomita	needed for Reeh–Schlieder
CCR / Weyl algebra	✗	✗	✗	needed for Klein–Gordon quantisation
Bogoliubov automorphism	✗	✗	✗	symplectomorphism → CCR *-iso
one-particle structure (K_μ, H_μ)	✗	✗	✗	Araki–Yamagami construction (math-ph/0008043 §4)
bosonic Fock space (analytic)	◐ algebraic SymmetricAlgebra only	✗	✗	analytic Fock = L² completion absent
creation / annihilation operators	✗	✗	✗	unbounded operators on Fock

Verdict (4). Layer 4 is the most mature stratum. Mathlib +
QuantumSystem together cover the universal machinery (C* / vN / GNS /
bicommutant); OSReconstruction extends with modular theory. The CCR /
Fock-quantisation side is the open subgap, shared by both flavours.

Layer 5 — AQFT framework

Categorical / algebraic structure that ties Layer 4 to Layer 1.

primitive	ML	QS	OSR	notes
local net O ↦ A(O) (lattice)	✗	✓ QuantumSystem.Algebra.LocalNet	✗	finite-dim lattice; Finset regions
local net (Minkowski open sets)	✗	✗	◐ via Wightman fields Φ(C₀^∞(O))	needed for Phase 1
local net (curved spacetime open sets)	✗	✗	✗	needed for Phase 2
isotony axiom	✗	✓ LocalNet.includeAlgebra	✓ in Wightman framework
locality / Einstein causality	✗	✓ lattice form	✓ Minkowski via [Φ(f), Φ(g)] = 0 for spacelike
time-slice axiom	✗	✗	✗	required by Sanders + BFV
categorical Man / Alg	✗	✗	✗	CategoryTheory infrastructure ✓ in Mathlib but no Man / Alg instances
locally covariant QFT functor A : Man → Alg (BFV)	✗	✗	✗	central definitional layer for Phase 2
state space functor S : Man → States	✗	✗	✗	BFV §3
relative Cauchy evolution	✗	✗	✗	BFV §4
Wightman axioms (W1–W6)	✗	✗	✓ W1–W4 fully formalised, W5–W6 partial	OSR Wightman/Axioms/
Schwinger / OS axioms	✗	✗	✓ OS I, II	OSR Euclidean side
Hadamard state	✗	✗	✗	Radzikowski microlocal characterisation absent
quasifree state	✗	✗	◐ Gaussian states
Reeh–Schlieder property (general)	✗	✗	◐ partial in Wightman/Reconstruction/	core statement
Reeh–Schlieder theorem (Wightman, Minkowski)	✗	✗	◐ scaffolding via GNS	OSR reconstruction would in principle yield this from OS axioms

Layer 6 — Modular theory (peripheral / optional)

Strohmaier–Witten 2302.02709 bypasses modular theory by using analytic
wavefront sets (Layer 3). The Klein–Gordon predecessor (math-ph/0008043) does
not use it either. Borchers/Araki Minkowski version uses tube domains. So
Layer 6 is not on either critical path, but is listed because OSR
develops it and it provides a fallback proof strategy.

primitive	ML	QS	OSR	notes
modular operator Δ_ω	✗	✗	✓	OSR has Tomita–Takesaki
modular conjugation J_ω	✗	✗	✓
modular flow σ_t	✗	✗	✓
KMS condition	✗	✗	✓
Bisognano–Wichmann	✗	✗	◐
Borchers' theorem (modular inclusions)	✗	✗	◐

If Phase 2 (curved Strohmaier–Witten) turns out infeasible because Layer 3
(microlocal) is too deep, modular theory becomes a fallback proof strategy
and OSR's Tomita–Takesaki development becomes valuable.

Prioritisation when primitives overlap

Same primitive sometimes appears in more than one source. Default priority
is ML > QS > OSR with the following rationale:

level	rationale
Mathlib first	most stable, strictest review, no external dependency, richest ecosystem tooling (Loogle, hover, lean_local_search); QS already depends on ML
QuantumSystem next	local additions on top of ML (WOTClosedSubalgebra bicommutant hard half, GNS.Representation, Gelfand–Naimark direct sum) — eventually upstream candidates
OSR last, scoped	reserved for what ML+QS jointly lack (Minkowski geometry, tube domains in ℂ⁴, Wightman axioms, Tomita–Takesaki)

Concrete overlap rulings

primitive	sources providing it	rule
VonNeumannAlgebra, commutant, commutant_commutant (easy half)	ML + QS (uses ML) + OSR (extends ML)	ML type is canonical; OSR's extensions are imported only at the Wightman/local-net interface, never to redefine the underlying type
commutant_commutant hard half (WOT-closed ⊆ A″)	QS only	QS WOTClosedSubalgebra.doubleCommutant_eq_of_isWOTClosed; ML lacks this direction
CStarAlgebra, StarAlgebra, *-algebra basics	ML + QS extends	ML canonical; QS extensions only where ML API is too lean (e.g. CStarAlgebraIdeal in QuantumSystem/ForMathlib/)
Hilbert space / InnerProductSpace	ML + QS	ML
SchwartzMap, Distribution	ML + OSR uses ML	ML as the type; OSR's Wightman-side wrappers only when calculations need them
IsManifold, smooth-manifold infrastructure	ML	ML
GNS construction, cyclic vector decomp	QS only	QS
Wightman axioms (W1–W4)	OSR only	OSR
MinkowskiGeometry, BHWCore.ForwardTube/ExtendedTube, EdgeOfWedge, TubeDomainExtension, BHW theorem	OSR only	OSR — Phase 1 entry points
Tomita–Takesaki (Δ_ω, J_ω, σ_t, KMS)	OSR only	OSR, Layer 6 fallback only
isotony / Einstein causality axiom	QS lattice + OSR Minkowski continuum	different settings, not actual overlap — QS is a Finset-region net (finite-dim), OSR is a continuum Wightman net; Phase 1 introduces a new QuantumSystem.Algebra.LocalNet.Minkowski that mediates between them, reusing QS's axiom names but with continuum-region carriers

Operational consequence

• Imports in new Phase 1 modules look like
  import Mathlib.Analysis.VonNeumannAlgebra.Basic (canonical type) plus
  import QuantumSystem.Algebra.CStarAlgebra.WOT (hard-half bicommutant),
  with OSR imports only when the Wightman / tube-domain infrastructure is
  needed.
• We never introduce a parallel VonNeumannAlgebra' etc. that ignores ML.
  If OSR carries its own version, we either translate at the interface or
  patch OSR upstream — never duplicate the type in QS.
• QuantumSystem/ForMathlib/ is reserved for QS-original extensions of
  ML (upstream candidates) and Apache-2.0-licensed ports of OSR (only
  if the [[require]] route fails).

Reusability assessment of xiyin137/OSreconstruction — central to Phase 1

Reusable components for the flat-Minkowski (Borchers/Araki) flavour:

• Minkowski geometry — Wightman/Spacetime/MinkowskiGeometry.lean
  provides ℝ⁴ + η with explicit signature, plus the Lorentz group action.
• Tube domains in ℂ⁴ — ComplexLieGroups/BHWCore.lean provides
  ForwardTube, ExtendedTube, complex Lorentz group action, openness +
  group-action continuity. Directly reusable for Borchers's analytic-
  continuation argument.
• Edge-of-Wedge theorem — SCV/EdgeOfWedge.lean plus
  LocalContinuousEOW.lean, LocalDistributionalEOW.lean. Both
  continuous and distributional versions formalised.
• Tube boundary values — SCV/TubeDomainExtension.lean and
  TubeBoundaryValues.lean give the analytic-continuation infrastructure.
• Wightman axioms (W1–W4) — Wightman/Axioms/ covers Hilbert space,
  Poincaré unitary representation, spectrum condition on forward cone,
  Schwartz test functions, vacuum cyclicity, spacelike commutativity,
  vacuum uniqueness. W5–W6 partial.
• Bridge module — Bridge/AxiomBridge.lean for OS ↔ Wightman
  equivalence (axiom-replacement guides, not full sorry-free proof).
• Tomita–Takesaki + KMS — relevant only as Layer-6 fallback.

Caveats. The repository carries 55 production sorries and 11 deferred
axioms, including foundational functional analysis. Borchers timelike tube
theorem itself is not yet formalised in OSR; Reeh–Schlieder is partial.
Phase 1 micro-task must grep -rn sorry the transitive closure of the
modules above to decide between lakefile require and porting.

Chosen route — Route C (sequential B → A)

User confirmed (2026-05-05) that both the Minkowski Borchers/Araki
theorem and the curved Strohmaier–Witten theorem are formalisation goals.
The plan is sequential:

Phase 1 (months) — flat-Minkowski Borchers/Araki

Target theorems:

• Borchers.timelikeTubeTheorem — R(O) = R(causal-completion(O)) for
  Minkowski timelike tubes.
• Araki.timelikeTubeTheorem — generalisation to arbitrary open sets.

Stack (bottom-up):

1. Reuse OSR MinkowskiGeometry, BHWCore.ForwardTube/ExtendedTube,
   EdgeOfWedge, TubeDomainExtension, WightmanAxioms.
2. Lift QuantumSystem's WOTClosedSubalgebra.doubleCommutant_eq_of_isWOTClosed
   into an R(O) = π(A(O))″ definition for Wightman fields.
3. Complete OSR's partial Reeh–Schlieder via the GNS construction.
4. Define Borchers timelike tube envelope.
5. Prove Asgeirsson mean-value theorem for the flat wave equation
   (the only PDE prerequisite — much simpler than curved Cauchy theory).
6. Stitch (1)–(5) into the Borchers proof, then specialise to Araki.

OSR usage decision (Phase 1 micro-task at start): grep -rn sorry
the transitive closure of OSR's MinkowskiGeometry, BHWCore,
EdgeOfWedge, TubeDomainExtension, Wightman/Axioms/*. If clean,
add [[require]] to lakefile.toml. Otherwise port the necessary subset
to QuantumSystem/ForMathlib/QFT/ (Apache 2.0 with LICENSE +
ATTRIBUTION.md).

Phase 2 (year+) — curved Strohmaier–Witten

Target theorem:

• StrohmaierWitten.timelikeTubeTheorem — R(E_T(O)) = R(O) on
  real-analytic globally hyperbolic spacetimes, with analytic states.

Re-evaluated after Phase 1 completion. Requires green-field
construction of Layer 1b (Lorentzian manifold theory), Layer 2 curved
PDE, and Layer 3 microlocal analysis. Mathlib upstream PRs may move
the floor in the meantime.

Critical-path summary

Phase 1 (Minkowski Borchers/Araki) — feasible now, months of work:

1. Layer 1a (flat Minkowski + tube domains) — substantially in OSR.
   Reuse, no green field.
2. Layer 4 (algebraic plumbing: C*, vN, GNS, bicommutant) —
   substantially in Mathlib + QuantumSystem.
3. Layer 5 (Wightman axioms + local net for Minkowski open sets) —
   substantially in OSR (W1–W4); W5–W6 + Reeh–Schlieder need finishing.
4. Asgeirsson mean-value theorem + flat Klein–Gordon — small green
   field work in Layer 2.
5. Borchers / Araki proof itself — new theorem statements + proofs
   stitched from (1)–(4).

Phase 2 (curved Strohmaier–Witten) — green field across multiple layers,
year+ scale:

1. Layer 1b (Lorentzian metric → time orientation → causal structure
   → Cauchy surface → globally hyperbolic) — none of the three sources
   provide this. Roughly the size of Mathlib's Riemannian geometry
   stack but for indefinite signature.
2. Layer 2 curved (Klein–Gordon Cauchy problem on (M, g) +
   advanced/retarded propagators) — depends on Layer 1b. Absent.
3. Layer 3 (analytic wavefront set + microlocal Holmgren) — Hörmander
   Vol I-style analysis library. Absent everywhere.
4. Layer 5 curved (BFV functor A : Man → Alg, Hadamard states,
   curved Reeh–Schlieder) — depends on Layer 1b. Absent.
5. Strohmaier–Witten proof itself — final step.

The flat / curved separation makes the difference: Phase 1 is leveraged
formalisation work (mostly stitching existing Lean), Phase 2 is genuine
green field across geometry, analysis, and microlocal layers.

References

• arXiv:2302.02709 — Strohmaier & Witten, Analytic States in Quantum Field Theory on Curved Spacetimes (curved timelike tube theorem, Theorem 5.3)
• arXiv:math-ph/0008043 — Strohmaier, On the local structure of the Klein–Gordon field on curved spacetimes (Klein–Gordon predecessor)
• arXiv:0801.4676 — Sanders, On the Reeh–Schlieder property in curved spacetime (LCQFT framework + spacetime deformation)
• arXiv:math-ph/0112041 — Brunetti–Fredenhagen–Verch, The generally covariant locality principle (A : Man → Alg functor
• arXiv:2507.00900 — Verch, Lecture Notes on Operator Algebras and QFT (modular theory in AQFT)
• Borchers 1961 (Bor61), Über die Vollständigkeit Lorentz-invarianter Felder in einer zeitartigen Röhre, Nuovo Cimento 19:787
• Araki 1963 (Ara63), A generalization of Borchers theorem, Helv. Phys. Acta 36:132–139