UncommittedLedger

formal source

  85  weight_eq : weight = ‖amplitude‖^2
  86
  87/-- An uncommitted ledger: a superposition of branches. -/
  88structure UncommittedLedger (n : ℕ) where
  89  /-- The branches (potential outcomes). -/
  90  branches : List (LedgerBranch n)
  91  /-- Weights sum to 1 (normalization). -/
  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