ledger_balance_conserved
plain-language theorem explainer
The theorem establishes that applying a LedgerUpdate to a Ledger leaves its balance unchanged, a basic invariance in the Recognition Science quantum ledger. Researchers modeling quantum states as ledger superpositions or deriving the Born rule from J-cost would cite it when proving evolution preserves total log-ratio sum. The proof is a direct reflexivity step that follows from the definition of applyUpdate on reciprocal entry pairs.
Claim. Let $L$ be a ledger whose balance equals the sum of the logarithms of the ratios of its entries. Let $u$ be an update consisting of two entries whose ratios are reciprocals. Then the balance of the ledger obtained by applying the update equals the original balance: $(applyUpdate L u).balance = L.balance$.
background
In the Quantum Ledger module a Ledger is a structure holding a list of LedgerEntry objects together with a balance field required to equal the sum of the logarithms of the entry ratios. A LedgerUpdate is a pair of LedgerEntry objects whose ratios satisfy the reciprocal relation, together with distinctness of their identifiers. This formalization treats quantum states as superpositions over ledger configurations, with the Born rule emerging from J-cost minimization and conservation holding under evolution.
proof idea
The proof is a one-line wrapper that applies reflexivity (rfl). It follows immediately once applyUpdate is expanded: the new ledger is formed by adjoining the reciprocal pair, whose log-ratios sum to zero and therefore leave the balance field invariant by the Ledger balance_eq field.
why it matters
The result supplies the conservation property required by the downstream theorem quantum_ledger_fundamentals, which lists ledger balance conservation among the five core facts establishing the quantum ledger model. It fills the conservation step in the RS formalization plan and connects to the eight-tick octave through the underlying LedgerForcing and EightTick imports. No open scaffolding remains for this invariance.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.