ledgerJlogCost
plain-language theorem explainer
The definition computes the aggregate Jlog cost of a transition between two d-dimensional ledger states by summing Jlog over all integer debit deltas and all integer credit deltas. It is invoked in downstream results establishing non-negativity of the cost and characterizing minimal posting steps under monotonicity. The body is realized as two separate Finset summations, each applying Cost.Jlog to the real cast of an integer difference.
Claim. For natural number $d$ and ledger states $L,L'$ in dimension $d$, the cost equals $Jlog(L'.debit_i - L.debit_i) + Jlog(L'.credit_i - L.credit_i)$ summed over all $i$ in Fin $d$, where each difference is taken as an integer and cast to a real, and $Jlog$ is the cost function $Jcost(e^t)$.
background
LedgerState $d$ is the abbreviation Recognition.Ledger (AccountRS $d$), representing a state whose debit and credit vectors are indexed by Fin $d$. The module develops posting-style updates in which a single post increments exactly one entry by one unit, thereby changing the induced parity pattern by exactly one bit. Jlog is supplied by the Cost module as the composition Jcost composed with the exponential map, equivalently $((e^t + e^{-t})/2) - 1$. Upstream LedgerState structures appear in VariationalDynamics (conserved log-ratio charge), InformationIsLedger (list of recognition events), and Thermodynamics (active bonds with multipliers), each supplying a conserved or cost-bearing ledger notion that this definition specializes to debit-credit deltas.
proof idea
The definition is a direct double summation: one Finset sum applies Cost.Jlog to each debit-component difference cast from integer to real, and a second identical sum does the same for the credit components. No lemmas or tactics are applied inside the definition; it is a pure abbreviation whose body is expanded at use sites.
why it matters
This supplies the explicit transition cost for the ledger posting model that converts abstract vector lemmas into concrete debit-credit adjacency. It is used by ledgerJlogCost_nonneg (non-negativity), ledgerJlogCost_post (exact cost of a single post equals Jlog 1), minJlogCost_monotoneStep_implies_postingStep, and postingStep_of_monotone_and_ledgerJlogCost_le_Jlog1. The definition thereby completes the module's upgrade from vector parity to ledger-shaped posting, supporting the one-bit parity change theorem stated in the module documentation and feeding the Recognition framework's J-cost machinery.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.