ledger_cost_additive
plain-language theorem explainer
Ledger cost additivity asserts that the total J-cost of a ledger after applying a reciprocal entry pair equals the sum of the two entry costs plus the prior total cost. Quantum ledger researchers in Recognition Science cite this when showing that updates preserve the cost structure underlying Born-rule probabilities derived from J-minimization. The proof is a direct term-mode simplification that unfolds the totalCost definition and applies ring arithmetic to the list sum.
Claim. Let $L$ be a ledger (a list of entries with balance equal to the sum of log-ratios) and let $u$ be a ledger update (a pair of entries whose ratios are reciprocals). Then the total J-cost of the updated ledger satisfies $totalCost(applyUpdate(L,u)) = cost(u.entry1) + cost(u.entry2) + totalCost(L)$.
background
A Ledger is a finite list of LedgerEntry records together with a real balance that equals the sum of the logarithms of the entry ratios, enforcing conservation. A LedgerUpdate is a pair of entries whose ratios are exact reciprocals and whose identifiers differ, representing a minimal recognition event that cancels in the balance. The totalCost function on a ledger is the sum of the individual J-costs of its entries, where each entry cost is given by the J-function applied to the ratio (J(x) = (x + x^{-1})/2 - 1). The module QuantumLedger formalizes the identification of quantum states with superpositions of such ledgers, with the Born rule emerging from cost minimization rather than being postulated.
proof idea
The proof is a one-line term-mode wrapper. It invokes simp only on the definitions of totalCost and applyUpdate together with the list constructors map_cons and sum_cons, then closes with the ring tactic that reduces the resulting arithmetic identity on real numbers.
why it matters
This additivity supplies the algebraic step needed to prove ledger_balance_conserved and to derive the conservation law that appears in the quantum-ledger interpretation of Recognition Science. It directly supports the claim that measurement collapses to the minimum-J-cost configuration by showing that each update adds a non-negative increment without disturbing prior costs. The result sits inside the forcing chain after T5 (J-uniqueness) and before the eight-tick octave (T7), ensuring that ledger evolution remains compatible with the D=3 spatial structure and the alpha band constants.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.