CommittedLedger

formal source

  92  normalized : (branches.map LedgerBranch.weight).sum = 1
  93
  94/-- A committed ledger: exactly one branch selected. -/
  95structure CommittedLedger (n : ℕ) where
  96  /-- The selected outcome. -/
  97  outcome : Fin n
  98  /-- The final amplitude (phase factor). -/
  99  amplitude : Amplitude
 100  /-- The amplitude has unit norm (after normalization). -/
 101  unit_norm : ‖amplitude‖ = 1
 102
 103/-! ## The Measurement Process -/
 104
 105/-- Helper: sum over filter equals sum over all for norm-squared (zeros contribute nothing). -/
 106private lemma sum_filter_eq_sum_all {n : ℕ} (f : Fin n → ℂ) :
 107    (Finset.univ.filter (fun i => f i ≠ 0)).sum (fun i => ‖f i‖^2) =
 108    Finset.univ.sum (fun i => ‖f i‖^2) := by
 109  have h : (Finset.univ.filter (fun i => f i = 0)).sum (fun i => ‖f i‖^2) = 0 := by
 110    apply Finset.sum_eq_zero
 111    intro i hi
 112    simp only [Finset.mem_filter, Finset.mem_univ, true_and] at hi
 113    simp [hi]
 114  have hsplit := Finset.sum_filter_add_sum_filter_not (s := Finset.univ)
 115    (p := fun i => f i ≠ 0) (f := fun i => ‖f i‖^2)
 116  simp only [not_not] at hsplit
 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