empty_ledger_balance
plain-language theorem explainer
The empty ledger is defined with balance zero. Researchers establishing ledger conservation before linking to quantum states cite this base fact. The proof is a direct reflexivity step on the explicit definition of emptyLedger.
Claim. The balance of the empty ledger equals zero: $balance(emptyLedger) = 0$.
background
The Quantum Ledger module connects the Recognition Science ledger to quantum states, with a Ledger as a structure holding entries and a balance. The emptyLedger is the initial ledger with no entries. Its definition explicitly sets balance to zero, as stated in the upstream result: 'Empty ledger has zero balance.'
proof idea
One-line wrapper that applies reflexivity to the definition of emptyLedger.
why it matters
This supplies the zero-balance base case inside quantum_ledger_fundamentals, which lists empty ledger balance zero among the core ledger properties before deriving conservation under updates and the Born rule from J-cost. It anchors the conservation principle that runs through ledger evolution in the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.