UnitaryOperator

formal source

  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
  77/-! ## Ledger Conservation -/
  78
  79/-- In RS, the ledger is conserved:
  80
  81    1. Total "ledger content" is constant