LedgerUpdate
plain-language theorem explainer
LedgerUpdate packages two ledger entries whose ratios are exact reciprocals with distinct identifiers, so their contributions to total balance cancel. Quantum modelers in Recognition Science cite it when constructing updates that preserve ledger invariants during state evolution. The declaration is a direct four-field structure with no computation or lemmas.
Claim. A pair of ledger entries $e_1$ and $e_2$ such that the ratio of $e_2$ equals the reciprocal of the ratio of $e_1$ and the identifiers of $e_1$ and $e_2$ are unequal.
background
LedgerEntry records a single recognition event by an identifier in natural numbers, a positive real ratio, and the associated J-cost. The QuantumLedger module treats quantum states as superpositions over such ledger configurations, with the Born rule emerging from J-cost minimization rather than being postulated. Upstream, the reciprocal construction in LedgerForcing produces the inverse-ratio event, while CostAlgebra supplies the identity and reciprocal automorphisms that underwrite the cancellation condition.
proof idea
The declaration is a plain structure definition that directly assembles the two entries together with the reciprocal-ratio equality and the distinct-identifier inequality as fields.
why it matters
LedgerUpdate supplies the atomic canceling pair required by the conservation theorems that follow it. It is used by applyUpdate to extend a ledger while keeping balance unchanged, and by the subsequent lemmas ledger_balance_conserved and ledger_cost_additive. Within the Recognition Science framework it implements the reciprocal cancellation needed for the eight-tick octave and the forcing chain, allowing net-zero cost evolution of ledger superpositions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.