LedgerBranch
LedgerBranch packages one potential measurement outcome as a basis index in Fin n, a complex amplitude, and a real weight fixed equal to the squared modulus. Quantum measurement researchers formalizing collapse via ledger commitment would cite this when building superpositions. The declaration is a direct structure that encodes the Born weight condition by field construction with no separate proof.
claimA ledger branch for dimension $n$ consists of an outcome index $k$ in the finite set Fin $n$, a complex amplitude $a$, a real weight $w$, and the equality $w = |a|^2$.
background
The module derives the measurement postulate from Recognition Science ledger structure, where superposition is an uncommitted ledger of multiple branches and measurement forces commitment to one outcome. Amplitude is the type of complex numbers. Upstream results supply the superposition theorem (J-cost positive for ratios away from 1), ledger factorization, phi-forcing structures that calibrate J, and spectral emergence that fixes the finite basis dimension.
proof idea
This is a structure definition. It directly declares the four fields and embeds the weight-equality constraint as a field; no tactics or lemmas are applied.
why it matters in Recognition Science
LedgerBranch is the atomic unit for UncommittedLedger (a normalized list of branches) and is used in the filter_map_weight_sum theorem that preserves total weight 1. It fills the QF-001 target of representing superposition branches before ledger commitment, connecting to J-cost minimization and the eight-tick octave from upstream phi-forcing. It leaves the actual commitment rule for later declarations.
scope and limits
- Does not select or commit any branch during measurement.
- Does not derive amplitudes from the Schroedinger equation.
- Does not incorporate explicit J-cost values into weights.
- Does not extend to infinite-dimensional Hilbert spaces.
Lean usage
def ex : LedgerBranch 2 := { outcome := 0, amplitude := 1, weight := 1, weight_eq := rfl }formal statement (Lean)
77structure LedgerBranch (n : ℕ) where
78 /-- The basis state index. -/
79 outcome : Fin n
80 /-- The amplitude (complex). -/
81 amplitude : Amplitude
82 /-- Recognition weight (proportional to |amplitude|²). -/
83 weight : ℝ
84 /-- Weight equals squared norm. -/
85 weight_eq : weight = ‖amplitude‖^2
86
87/-- An uncommitted ledger: a superposition of branches. -/