QuantumState

formal source

  57
  58/-- A quantum state in a finite-dimensional Hilbert space.
  59    Represented as a function from basis states to amplitudes. -/
  60structure QuantumState (n : ℕ) where
  61  /-- Amplitude for each basis state. -/
  62  amplitudes : Fin n → Amplitude
  63  /-- Normalization: |ψ|² = 1. -/
  64  normalized : (Finset.univ.sum fun i => ‖amplitudes i‖^2) = 1
  65
  66/-- A superposition state: multiple basis states with non-zero amplitude. -/
  67def isSuperposition {n : ℕ} (ψ : QuantumState n) : Prop :=
  68  ∃ i j : Fin n, i ≠ j ∧ ψ.amplitudes i ≠ 0 ∧ ψ.amplitudes j ≠ 0
  69
  70/-- A definite state: exactly one basis state has non-zero amplitude. -/
  71def isDefinite {n : ℕ} (ψ : QuantumState n) : Prop :=
  72  ∃! i : Fin n, ψ.amplitudes i ≠ 0
  73
  74/-! ## Ledger Model of Quantum States -/
  75
  76/-- A ledger branch represents a potential measurement outcome. -/
  77structure LedgerBranch (n : ℕ) where
  78  /-- The basis state index. -/
  79  outcome : Fin n
  80  /-- The amplitude (complex). -/
  81  amplitude : Amplitude
  82  /-- Recognition weight (proportional to |amplitude|²). -/
  83  weight : ℝ
  84  /-- Weight equals squared norm. -/
  85  weight_eq : weight = ‖amplitude‖^2
  86
  87/-- An uncommitted ledger: a superposition of branches. -/
  88structure UncommittedLedger (n : ℕ) where
  89  /-- The branches (potential outcomes). -/
  90  branches : List (LedgerBranch n)