ledgerL1Cost
plain-language theorem explainer
LedgerL1Cost defines the total absolute change in debit and credit counts between two ledger states of dimension d. Researchers modeling recognition events via ledger transitions cite it to quantify minimal posting steps. The definition expands directly as the sum of natAbs differences over the Fin d indices for both debit and credit components.
Claim. For ledger states $L, L'$ in dimension $d$, the L1 cost is $sum_{i : Fin d} |L'.debit(i) - L.debit(i)| + sum_{i : Fin d} |L'.credit(i) - L.credit(i)|$, where debit and credit are the integer maps on accounts.
background
In the LedgerPostingAdjacency module a LedgerState d is the abbreviation Recognition.Ledger (AccountRS d), consisting of debit and credit functions from Fin d to Int. The module develops posting-style ledger updates in which a tick posts exactly one unit to one account, inducing a one-bit change in the induced parity pattern. Upstream LedgerState structures from VariationalDynamics, InformationIsLedger and Thermodynamics treat ledgers as collections of recognition events or configurations whose total log-ratio is conserved.
proof idea
This is a direct definition that computes the L1 norm of the difference vectors for debit and credit separately by summing Int.natAbs over Fin d.
why it matters
The definition supplies the cost metric inside LegalAtomicTick, which pairs monotonicity with unit L1 cost to characterize posting steps. It feeds the downstream theorems legalAtomicTick_implies_PostingStep and minCost_monotoneStep_implies_postingStep. Within the Recognition framework it supplies the discrete cost for ledger transitions that realize one-bit parity adjacency, linking to the eight-tick octave and the underlying Recognition.Ledger construction.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.