commit_is_definite
plain-language theorem explainer
The declaration establishes that if an outcome i appears among the branches of an uncommitted ledger, the state is definite after commitment. Physicists deriving the measurement postulate from ledger mechanics would cite it as the basic projection step. The proof is a one-line term that applies the trivial constructor.
Claim. If an uncommitted ledger $L$ over $n$ outcomes contains a branch with outcome $i$, then the state after commitment is definite.
background
An uncommitted ledger is a structure whose branches list potential outcomes with weights summing to one, representing superposition before measurement. Commitment selects exactly one branch, rendering the state definite. The module derives the measurement postulate from Recognition Science ledger structure, where superposition equals multiple coexisting branches in working memory and measurement equals forced commitment that cancels the others.
proof idea
The proof is a one-line term that applies the trivial constructor.
why it matters
This theorem supplies the elementary projection fact needed for the module's target derivation of the measurement postulate from ledger commitment. It aligns with the framework step that converts uncommitted superposition into a definite outcome, consistent with the eight-tick octave and J-cost weighting of branches. No downstream uses are recorded, leaving its role as an interface lemma for later probability derivations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.