IndisputableMonolith.Quantum.Observables

   1import IndisputableMonolith.Quantum.HilbertSpace
   2import Mathlib.Analysis.InnerProductSpace.Basic
   3import Mathlib.Analysis.InnerProductSpace.Adjoint
   4
   5/-! # Observable Algebra for Recognition Science QM Bridge -/
   6
   7namespace IndisputableMonolith.Quantum
   8
   9open scoped InnerProductSpace
  10
  11/-- Self-adjoint operator (observable) -/
  12structure Observable (H : Type*) [RSHilbertSpace H] where
  13  /-- Bounded linear operator -/
  14  op : H →L[ℂ] H
  15  /-- Self-adjoint condition -/
  16  self_adjoint : ∀ x y : H, ⟪op x, y⟫_ℂ = ⟪x, op y⟫_ℂ
  17
  18/-- Projection operator -/
  19structure Projector (H : Type*) [RSHilbertSpace H] extends Observable H where
  20  /-- Idempotent property -/
  21  idempotent : op.comp op = op
  22
  23/-- Hamiltonian operator -/
  24structure Hamiltonian (H : Type*) [RSHilbertSpace H] extends Observable H where
  25  /-- Energy must be bounded below -/
  26  bounded_below : ∃ E₀ : ℝ, ∀ ψ : NormalizedState H,
  27    (⟪op ψ.vec, ψ.vec⟫_ℂ).re ≥ E₀
  28
  29end IndisputableMonolith.Quantum
  30