def
definition
isSuperposition
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Quantum.Measurement.WavefunctionCollapse on GitHub at line 67.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
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)
91 /-- Weights sum to 1 (normalization). -/
92 normalized : (branches.map LedgerBranch.weight).sum = 1
93
94/-- A committed ledger: exactly one branch selected. -/
95structure CommittedLedger (n : ℕ) where
96 /-- The selected outcome. -/
97 outcome : Fin n