Home · §10.1 GNS · §10.2 Spectral · §10.3 Unbounded · §10.4 Stone · §10.5 Spacetime · §10.6 Minkowski · §10.7 Curved · §10.8 Covariance · Axioms · Guide
§10.1 GNS Construction (pp. 29–38)
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 two supporting objects are the state (Definition 13) and the cyclic vector (Definition 14); the auxiliary results 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). §10.1.3 is a prose summary and carries no numbered items.
Where the Lean lives: Physicslib4/GNS/ (Basic, Construction, NullSpace, CauchySchwarz)
Items
Every entry links to its node in the web blueprint and names the principal Lean declaration.
§10.1.1 GNS Construction Theorem (p. 29)
- Definition 13 — State ·
Physicslib4.GNS.State(+1 more) - Definition 14 — Cyclic Vector ·
Physicslib4.GNS.IsCyclicVector - Theorem 15 — GNS Construction Theorem ·
Physicslib4.GNS.gns_construction(+1 more)
§10.1.2 Auxiliary Results Used in the Proof (p. 35)
- Lemma 16 — Cauchy–Schwarz Inequality ·
Physicslib4.GNS.cauchy_schwarz_inequality - Lemma 17 — The two descriptions of the GNS left ideal \(\mathcal{N}\) agree ·
Physicslib4.GNS.lmm1 - Lemma 18 — \(\mathcal{N}\) is a closed linear subspace ·
Physicslib4.GNS.lmm2
Home · §10.1 GNS · §10.2 Spectral · §10.3 Unbounded · §10.4 Stone · §10.5 Spacetime · §10.6 Minkowski · §10.7 Curved · §10.8 Covariance · Axioms · Guide