tensor-sieve/PTSymmetry.lean at main · ryanncode/tensor-sieve · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
import PTSymmetry.MathlibCore.IndefiniteMetric
import PTSymmetry.MathlibCore.KreinSpace
import PTSymmetry.MathlibCore.Minkowski
import PTSymmetry.MathlibCore.KreinBundle
import PTSymmetry.Physics.MajorantTopology
import PTSymmetry.Physics.JAdjointHamiltonian
import PTSymmetry.Physics.GuptaBleuler
import PTSymmetry.Physics.MajorantBundle
import PTSymmetry.Physics.WaveOperator

/-!
# PT-Symmetric Quantum Mechanics (WIP)

This project formalizes the foundational mathematics required for
PT-Symmetric Quantum Mechanics and generalized indefinite metric spaces
(such as Gupta-Bleuler quantization).

It provides a clean, abstract mathematical interface (Krein Spaces,
Indefinite Metrics) separated from specific applications, allowing
the algebraic definitions to be proposed to Mathlib cleanly.
-/