emptyLedger
plain-language theorem explainer
The empty ledger is the Ledger structure instantiated with an empty entry list and balance zero. It serves as the base case for conservation and cost theorems in the quantum ledger formalization. The definition is a direct structure literal whose balance equality is discharged by simplification.
Claim. The empty ledger is the structure with entries the empty list and balance $0$, satisfying the constraint that the balance equals the sum of the logarithms of the entry ratios (vacuously true for the empty list).
background
A Ledger is a structure with a list of LedgerEntry items, a real balance, and a proof that the balance equals the sum of logarithms of the ratios in those entries. The QuantumLedger module formalizes the link between recognition science ledgers and quantum states, where states are superpositions over ledger configurations and the Born rule emerges from J-cost minimization. No upstream lemmas are required; the definition stands alone as the zero element.
proof idea
The definition constructs the Ledger structure directly by setting entries to the empty list and balance to zero. The balance_eq field is filled by the simp tactic, which confirms the empty sum equals zero.
why it matters
This definition supplies the zero ledger required by downstream results including empty_ledger_balance, empty_ledger_cost, empty_ledger_phase, and quantum_ledger_fundamentals. The latter states that entry costs are non-negative, balance is conserved, and 8-tick phases enable interference. It anchors the formal connection between ledger conservation and quantum superposition in the Recognition Science framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.