applyUpdate
plain-language theorem explainer
Physicists modeling quantum states as superpositions over ledger configurations invoke applyUpdate to evolve a ledger by prepending a reciprocal entry pair while keeping the total balance fixed. The operation realizes the conservation step needed for unitary evolution in the Recognition Science ledger. Its definition proceeds by direct record construction together with an algebraic cancellation that uses the reciprocal hypothesis to show the added log terms sum to zero.
Claim. Given a ledger $L$ and an update $u$ consisting of entries $e_1$ and $e_2$ satisfying $e_2.ratio = e_1.ratio^{-1}$, the updated ledger has entry list $e_1 :: e_2 :: L.entries$ and balance equal to $L.balance$.
background
In the QuantumLedger module a Ledger is a structure holding a list of LedgerEntry objects, a real balance, and an equality proof that the balance equals the sum of the logarithms of the entry ratios. A LedgerUpdate is a pair of entries whose ratios are reciprocals, so their logarithmic contributions cancel exactly. The module formalizes the identification of quantum states with superpositions over ledger configurations, with the Born rule emerging from J-cost minimization and conservation required for unitary evolution. Upstream the reciprocal operation supplied by CostAlgebra and LedgerForcing guarantees the inverse-ratio relation used in the balance proof.
proof idea
The definition builds the new Ledger record by setting entries to the cons of the two update entries onto the original list and balance to the original balance. The balance_eq field is discharged by simplifying the summed logs, rewriting via the reciprocal hypothesis and Real.log_inv to obtain exact cancellation, then applying linarith after rewriting the original balance_eq.
why it matters
applyUpdate supplies the concrete construction used by ledger_balance_conserved, ledger_cost_additive, and the quantum_ledger_fundamentals summary theorem. It realizes the conservation property required for the ledger to model unitary evolution, closing one step in the connection between recognition events and quantum interference within the eight-tick framework. The definition thereby supports the broader claim that ledger balance is preserved under updates that correspond to reciprocal recognition pairs.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.