UncommittedLedger
plain-language theorem explainer
An uncommitted ledger models a quantum superposition as a normalized list of potential measurement outcomes. Researchers deriving the measurement postulate from Recognition Science ledger commitment would cite this structure when formalizing wavefunction collapse. It is introduced directly as a structure definition that enforces a sum-to-one condition on branch weights.
Claim. An uncommitted ledger in dimension $n$ consists of a list of ledger branches, each carrying an outcome index in Fin $n$, a complex amplitude, and a weight equal to the squared norm of that amplitude, such that the sum of all weights equals 1.
background
The module derives the measurement postulate from Recognition Science by treating superposition as an uncommitted ledger entry and measurement as ledger commitment. A ledger branch records one potential outcome together with its amplitude and recognition weight (equal to the squared norm). The local setting is given by the module documentation: superposition equals an uncommitted ledger, measurement equals commitment, and outcome probabilities follow from J-cost, reproducing the Born rule.
proof idea
This is a structure definition. The two fields are the list of branches and the explicit normalization predicate that the sum of mapped weights equals one.
why it matters
The structure supplies the starting object for the commit operation that models wavefunction collapse and for the theorems commit_is_definite and decoherence_gives_classicality. It fills the QF-001 derivation of the measurement postulate stated in the module documentation and supplies the ledger mechanism that realizes actualization in the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.