ledgerL1Cost_post
plain-language theorem explainer
The lemma shows that applying a single atomic post to a d-dimensional ledger state changes its L1 cost by exactly one. Ledger-model researchers cite it to confirm that posting steps realize the minimal unit cost in the Recognition framework. The proof uses case split on debit versus credit, Finset sum erasure to isolate the changed coordinate, and direct simplification to verify the other vector remains untouched.
Claim. Let $L$ be a ledger state with debit and credit vectors indexed by $d$ accounts. For any account index $k$ and side $s$ (debit or credit), the L1 cost of the updated state obtained by posting one unit at $k$ on side $s$ equals 1: $C_{L1}(L, post(L,k,s)) = 1$.
background
LedgerState d is the type of pairs of debit and credit vectors over Fin d, each entry an integer recording recognition events at that account. The post operation adds exactly one unit to either the debit or credit component at a chosen index k, leaving the opposite vector unchanged. ledgerL1Cost is the sum of absolute differences across all debit entries plus the same sum across all credit entries, measuring the total integer displacement between two ledger states. The module upgrades an abstract vector model to this explicit posting ledger so that parity changes become one-bit adjacency steps. Upstream LedgerState structures in VariationalDynamics and InformationIsLedger supply the conserved log-ratio and event-list interpretations that this concrete carrier refines.
proof idea
The tactic proof opens with classical and cases on side. For debit it defines an auxiliary function f for absolute debit differences, applies Finset.add_sum_erase to split the sum at k, proves f k = 1 by direct simplification of post, shows the erased sum vanishes by sum_eq_zero on the remaining indices, then reassembles to obtain debit sum = 1 and credit sum = 0. The credit case mirrors the argument with roles reversed. Both branches finish by unfolding ledgerL1Cost and substituting the two sums.
why it matters
This lemma supplies the cost side of the LegalAtomicTick predicate used by legalAtomicTick_of_post, which in turn feeds minCost_monotoneStep_implies_postingStep. It therefore closes the gap between the abstract Recognition ledger and the concrete posting model required for parity one-bit adjacency. In the framework it realizes the minimal-cost atomic tick that preserves the J-cost structure while advancing the phi-ladder by a single rung, consistent with the eight-tick octave and D = 3 spatial embedding. No open scaffolding remains at this node.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.