list_map_sum_eq_finset_sum

formal source

 117  linarith
 118
 119/-- Helper: List.map.sum via Multiset operations. -/
 120private lemma list_map_sum_eq_finset_sum {n : ℕ} (s : Finset (Fin n)) (f : Fin n → ℝ) :
 121    (s.toList.map f).sum = s.sum f := by
 122  rw [Finset.sum_eq_multiset_sum]
 123  have h1 : s.toList = Multiset.toList s.val := rfl
 124  rw [h1, ← Multiset.sum_coe, ← Multiset.map_coe, Multiset.coe_toList]
 125
 126/-- **THEOREM**: Filtering and mapping preserves the total weight for quantum states.
 127    This follows from the normalization condition of quantum states.
 128    The sum of |ψᵢ|² over non-zero amplitudes equals 1 since zeros contribute nothing. -/
 129theorem filter_map_weight_sum : ∀ {n : ℕ} (ψ : QuantumState n),
 130    (((Finset.univ.filter (fun i => ψ.amplitudes i ≠ 0)).toList.map
 131      (fun i => (⟨i, ψ.amplitudes i, ‖ψ.amplitudes i‖^2, rfl⟩ : LedgerBranch n))).map
 132    LedgerBranch.weight).sum = 1 := by
 133  intro n ψ
 134  rw [List.map_map]
 135  have hcomp : (LedgerBranch.weight ∘ fun i => (⟨i, ψ.amplitudes i, ‖ψ.amplitudes i‖^2, rfl⟩ : LedgerBranch n))
 136             = (fun i => ‖ψ.amplitudes i‖^2) := by ext i; rfl
 137  rw [hcomp, list_map_sum_eq_finset_sum, sum_filter_eq_sum_all]
 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. -/