theorem
proved
born_rule_normalized
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 157.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
-
of -
of -
is -
of -
QuantumState -
is -
of -
for -
is -
QuantumState -
of -
is -
born_rule_normalized -
born_rule_normalized -
born_rule_normalized -
normalized -
QuantumState -
amplitude -
QuantumState -
amplitude -
measurementProbability -
QuantumState
used by
formal source
154 exact sq_nonneg _
155
156/-- **THEOREM (Born Rule Normalization)**: Probabilities sum to 1. -/
157theorem born_rule_normalized {n : ℕ} (ψ : QuantumState n) :
158 (Finset.univ.sum fun i => measurementProbability ψ i) = 1 := by
159 unfold measurementProbability
160 exact ψ.normalized
161
162/-! ## Ledger Commitment = Wavefunction Collapse -/
163
164/-- The norm of a normalized amplitude is 1.
165 |z / |z|| = |z| / |z| = 1 for z ≠ 0. -/
166theorem norm_div_norm_eq_one : ∀ (z : ℂ), z ≠ 0 → ‖z / ‖z‖‖ = 1 := by
167 intro z hz
168 rw [norm_div]
169 have h1 : ‖(‖z‖ : ℂ)‖ = ‖z‖ := by simp [Complex.norm_real]
170 rw [h1]
171 exact div_self (norm_ne_zero_iff.mpr hz)
172
173/-- Commit a ledger to a specific outcome.
174 This is the formal model of wavefunction collapse. -/
175noncomputable def commit {n : ℕ} (L : UncommittedLedger n) (i : Fin n)
176 (_h : ∃ b ∈ L.branches, b.outcome = i) : CommittedLedger n :=
177 let b := L.branches.find? (fun b => b.outcome = i)
178 match b with
179 | some branch =>
180 if hz : branch.amplitude ≠ 0 then
181 ⟨i, branch.amplitude / ‖branch.amplitude‖, norm_div_norm_eq_one branch.amplitude hz⟩
182 else
183 ⟨i, 1, by simp⟩ -- Branch has zero amplitude, use unit
184 | none => ⟨i, 1, by simp⟩ -- Should not happen given h
185
186/-- **THEOREM (Collapse is Projection)**: After commitment, the state is definite. -/
187theorem commit_is_definite {n : ℕ} (L : UncommittedLedger n) (i : Fin n)