commit
plain-language theorem explainer
The commit definition selects one branch from an uncommitted ledger and returns a committed ledger carrying the chosen outcome together with a unit-norm amplitude. Quantum modelers working in Recognition Science cite it to realize wavefunction collapse as ledger commitment. The body locates the matching branch via list find, normalizes its amplitude when nonzero, and defaults to unit amplitude otherwise.
Claim. Let $L$ be an uncommitted ledger over $n$ outcomes whose branches are normalized to total weight 1, and let $i$ be an index for which at least one branch has outcome $i$. Then commit$(L,i)$ produces a committed ledger whose selected outcome is $i$ and whose amplitude satisfies unit norm.
background
UncommittedLedger $n$ is the structure whose branches field holds a list of LedgerBranch $n$ entries with weights summing to 1; it encodes superposition before measurement. CommittedLedger $n$ is the structure that records a single outcome in Fin $n$ together with an Amplitude of norm 1. The module frames the measurement problem as the transition from uncommitted to committed ledger, with probabilities arising from recognition weights $|$amplitude$|^2$.
proof idea
The definition performs a list find on branches for the outcome $i$. On a successful match it applies norm_div_norm_eq_one to normalize a nonzero amplitude or returns unit amplitude; the none case also returns unit amplitude. The supplied existence hypothesis guarantees the branch is present.
why it matters
This supplies the concrete commitment map that measurement_postulate_derived invokes to obtain the measurement postulate from ledger structure. It realizes the RS resolution in which superposition is an uncommitted ledger and collapse is forced commitment, feeding the Zeno-effect lemmas that interpret frequent commits as state freezing. The step sits inside the T5–T8 forcing chain and the J-cost probability derivation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.