LedgerBranch
plain-language theorem explainer
LedgerBranch defines a record pairing a basis index in Fin n with a complex amplitude and its squared modulus as recognition weight, modeling one term in an uncommitted superposition. Quantum theorists deriving the measurement postulate from ledger commitment in Recognition Science would cite this when constructing normalized branch lists. It is introduced as a direct structure definition with a single equality field constraint.
Claim. A ledger branch for dimension $n$ consists of an outcome index $k$ in the finite set of size $n$, a complex amplitude $a$, a real weight $w$, and the constraint $w = |a|^2$.
background
The module derives the measurement postulate by identifying superposition with uncommitted ledger entries whose branches carry recognition weights. Amplitude is the type of complex numbers. J-cost minimization supplies the probabilities via the upstream result that Jcost r > 0 whenever r ≠ 1 and r > 0.
proof idea
Direct structure definition introducing the four fields outcome, amplitude, weight, and weight_eq; no lemmas or tactics are invoked.
why it matters
The structure supplies the building block for UncommittedLedger and the normalization theorem filter_map_weight_sum that preserves total weight equal to 1. It fills the QF-001 step from superposition (J > 0) to ledger commitment, linking to the J-cost and eight-tick dynamics in the Recognition Science chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.