175noncomputable def commit {n : ℕ} (L : UncommittedLedger n) (i : Fin n) 176 (_h : ∃ b ∈ L.branches, b.outcome = i) : CommittedLedger n :=
proof body
Definition body.
177 let b := L.branches.find? (fun b => b.outcome = i) 178 match b with 179 | some branch => 180 if hz : branch.amplitude ≠ 0 then 181 ⟨i, branch.amplitude / ‖branch.amplitude‖, norm_div_norm_eq_one branch.amplitude hz⟩ 182 else 183 ⟨i, 1, by simp⟩ -- Branch has zero amplitude, use unit 184 | none => ⟨i, 1, by simp⟩ -- Should not happen given h 185 186/-- **THEOREM (Collapse is Projection)**: After commitment, the state is definite. -/
used by (4)
From the project-wide theorem graph. These declarations reference this one in their body.