UncommittedLedger
UncommittedLedger models a pre-measurement quantum state as a list of LedgerBranch entries whose weights sum to one. Physicists deriving the measurement postulate from Recognition Science would cite it to replace the ad-hoc collapse axiom with ledger commitment. The declaration is a direct structure definition that pairs the branch list with an explicit normalization field.
claimAn uncommitted ledger for dimension $n$ consists of a list of branches, each a LedgerBranch carrying an outcome index in Fin $n$, a complex amplitude, and a real weight equal to the squared norm of that amplitude, together with the axiom that the sum of all weights equals 1.
background
In the Recognition Science treatment of quantum measurement (module QF-001), a superposition is identified with an uncommitted ledger entry: multiple branches coexist before measurement. The module states that measurement corresponds to ledger commitment, which forces selection of one definite outcome while the remaining branches are cancelled. Probabilities follow from J-cost, with lower-cost branches more probable, recovering the Born rule $P ∝ |ψ|^2$ as relative recognition weight.
proof idea
The declaration is a structure definition. It introduces the field branches : List (LedgerBranch n) and the field normalized : (branches.map LedgerBranch.weight).sum = 1, with no further proof obligations.
why it matters in Recognition Science
UncommittedLedger supplies the formal object on which the commit operation acts to produce a CommittedLedger, and it is referenced by commit_is_definite, decoherence_gives_classicality, isEffectivelyClassical, and stateToLedger. It realizes the central claim of QF-001 that the measurement postulate emerges from ledger balance rather than being postulated. The structure therefore sits at the interface between the Recognition Composition Law and the eight-tick octave used to count branches.
scope and limits
- Does not specify the selection rule that chooses which branch to commit.
- Does not compute J-costs or derive explicit probabilities.
- Does not model entanglement or decoherence dynamics.
- Does not link to the forcing chain T0-T8 or spatial dimension D=3.
formal statement (Lean)
88structure UncommittedLedger (n : ℕ) where
89 /-- The branches (potential outcomes). -/
90 branches : List (LedgerBranch n)
91 /-- Weights sum to 1 (normalization). -/
92 normalized : (branches.map LedgerBranch.weight).sum = 1
93
94/-- A committed ledger: exactly one branch selected. -/