`Amplitude`

definition

show as: view math explainer →

module: IndisputableMonolith.Quantum.Measurement.WavefunctionCollapse
domain: Quantum
line: 56 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Quantum.Measurement.WavefunctionCollapse on GitHub at line 56.

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

  53/-! ## Quantum State Representation -/
  54
  55/-- A quantum amplitude (complex number). -/
  56abbrev Amplitude := ℂ
  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

papers checked against this theorem

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