filter_map_weight_sum

formal source

 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. -/
 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