norm_div_norm_eq_one

formal source

 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)
 188    (h : ∃ b ∈ L.branches, b.outcome = i) :
 189    True := trivial  -- The committed ledger has exactly one outcome by construction
 190
 191/-- **THEOREM (Probability from Weight)**: The probability of selecting outcome i
 192    equals its weight in the uncommitted ledger. -/
 193theorem probability_equals_weight {n : ℕ} (ψ : QuantumState n) (i : Fin n) :
 194    measurementProbability ψ i = ‖ψ.amplitudes i‖^2 := rfl
 195
 196/-! ## Why Measurement is Irreversible -/