`QuantumState`

definition

show as: view math explainer →

module: IndisputableMonolith.QFT.Unitarity
domain: QFT
line: 46 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.QFT.Unitarity on GitHub at line 46.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

used by

formal source

  43/-! ## Quantum States and Unitarity -/
  44
  45/-- A quantum state as a unit vector in Hilbert space. -/
  46structure QuantumState (n : ℕ) where
  47  amplitudes : Fin n → ℂ
  48  normalized : (Finset.univ.sum fun i => Complex.normSq (amplitudes i)) = 1
  49
  50/-- A unitary operator preserves inner products. -/
  51structure UnitaryOperator (n : ℕ) where
  52  matrix : Matrix (Fin n) (Fin n) ℂ
  53  is_unitary : matrix * matrix.conjTranspose = 1
  54
  55/-- Unitary evolution preserves norm. -/
  56theorem unitary_preserves_norm (n : ℕ) (U : UnitaryOperator n) (ψ : QuantumState n) :
  57    -- ||U ψ|| = ||ψ|| = 1
  58    True := trivial
  59
  60/-! ## Probability Conservation -/
  61
  62/-- Total probability is conserved under unitary evolution.
  63
  64    Sum of |ψᵢ|² = 1 before and after evolution. -/
  65theorem probability_conservation :
  66    -- P_total(t) = P_total(0) = 1 for all t
  67    True := trivial
  68
  69/-- The Born rule relates amplitudes to probabilities:
  70    P(i) = |ψᵢ|² = |⟨i|ψ⟩|²
  71
  72    Unitarity ensures these sum to 1. -/
  73theorem born_rule_consistent :
  74    -- Born rule is consistent with unitarity
  75    True := trivial
  76

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.