commit
The commit definition takes an uncommitted ledger of quantum branches and a chosen outcome index, then produces the corresponding committed ledger with unit-norm amplitude. Researchers deriving the measurement postulate inside Recognition Science cite this step as the formal model of wavefunction collapse. The definition locates the matching branch and normalizes its amplitude, defaulting to the unit value when the amplitude vanishes.
claimLet $L$ be an uncommitted ledger over $n$ outcomes (a list of branches whose weights sum to 1) and let $i$ be a chosen index in $0..n-1$. Given the hypothesis that at least one branch records outcome $i$, the operation yields a committed ledger whose selected outcome is $i$ and whose amplitude is the original branch amplitude divided by its norm (or the unit amplitude when the branch amplitude is zero).
background
UncommittedLedger n is the structure holding a list of LedgerBranch entries together with the normalization condition that the sum of their weights equals 1; each branch carries an outcome index and a complex amplitude. CommittedLedger n is the structure that records exactly one selected outcome together with a unit-norm amplitude. The module frames the measurement problem as the transition from an uncommitted ledger (superposition) to a committed ledger (definite state), with probabilities supplied by recognition weights |amplitude|².
proof idea
The definition is a direct construction: it searches the branch list for the entry whose outcome equals the supplied index, then matches on the result. When a branch is found and its amplitude is nonzero the normalized value is obtained via division by the norm; otherwise the unit amplitude is inserted. The supplied hypothesis guarantees the search succeeds.
why it matters in Recognition Science
This definition supplies the concrete map from uncommitted to committed ledger that the downstream theorem measurement_postulate_derived invokes to obtain the measurement postulate. It therefore realizes the RS resolution of the measurement problem stated in the module header: superposition becomes ledger commitment, and the Born rule emerges from recognition weights. The construction sits inside the eight-tick ledger framework and feeds the Zeno-effect derivations that treat repeated commitment as the mechanism for state freezing.
scope and limits
- Does not select which branch is committed; that choice remains external.
- Does not derive the probability measure over outcomes.
- Does not encode the continuous-time evolution between commitments.
- Does not enforce ledger balance beyond the supplied hypothesis.
Lean usage
def use_commit {n : ℕ} (L : UncommittedLedger n) (i : Fin n) (h : ∃ b ∈ L.branches, b.outcome = i) : CommittedLedger n := commit L i hformal statement (Lean)
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. -/