ledgerJlogCost_post
plain-language theorem explainer
The lemma establishes that applying a single-unit posting operation to one account in a d-dimensional ledger changes the aggregate Jlog-cost by exactly Jlog(1). Ledger-model researchers cite it when proving that minimal-cost monotone steps coincide with atomic postings. The proof splits into debit and credit cases, isolates the single nonzero delta via Finset sum erasure, and verifies that all other coordinates contribute zero.
Claim. Let $L$ be a ledger state over $d$ accounts. For any account index $k$ and direction (debit or credit), the Jlog-cost of the transition from $L$ to the state obtained by posting one unit at $k$ equals $Jlog(1)$.
background
LedgerState d is the type of pairs of debit and credit vectors indexed by Fin d, each entry an integer balance. The posting operation adds +1 to exactly one coordinate of either the debit or credit vector. ledgerJlogCost sums Jlog of the integer deltas across all accounts and both sides; Jlog itself is the composition Jcost(exp t) from the cost module. The module upgrades vector lemmas to an explicit ledger model whose single-post steps induce one-bit parity changes, as required by the parity-adjacency results imported from LedgerParityAdjacency.
proof idea
Case analysis on the Side constructor. For debit, the debit-sum is split by Finset.add_sum_erase at k, the k-term simplifies to Jlog(1) by direct post definition, and the erased sum is shown zero by pointwise simplification. The credit-sum is identically zero. Symmetric steps handle the credit case. The final simp only unfolds ledgerJlogCost after the sub-sums are established.
why it matters
It supplies the exact cost of an atomic posting step, which the downstream theorem minJlogCost_monotoneStep_implies_postingStep uses to conclude that any minimal-cost monotone ledger transition must be a posting. The result closes the ledger-to-parity bridge described in the module header, linking single-tick updates to the one-bit adjacency that feeds the eight-tick octave and D=3 spatial structure in the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.