stateToLedger

formal source

 138  exact ψ.normalized
 139
 140/-- Convert a quantum state to an uncommitted ledger. -/
 141noncomputable def stateToLedger {n : ℕ} (ψ : QuantumState n) : UncommittedLedger n :=
 142  ⟨(Finset.univ.filter (fun i => ψ.amplitudes i ≠ 0)).toList.map
 143    (fun i => ⟨i, ψ.amplitudes i, ‖ψ.amplitudes i‖^2, rfl⟩),
 144   filter_map_weight_sum ψ⟩
 145
 146/-- Probability of measuring outcome i from state ψ (Born rule). -/
 147noncomputable def measurementProbability {n : ℕ} (ψ : QuantumState n) (i : Fin n) : ℝ :=
 148  ‖ψ.amplitudes i‖^2
 149
 150/-- **THEOREM (Born Rule)**: Probabilities are non-negative. -/
 151theorem born_rule_nonneg {n : ℕ} (ψ : QuantumState n) (i : Fin n) :
 152    measurementProbability ψ i ≥ 0 := by
 153  unfold measurementProbability
 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)