postingStep_of_monotone_and_ledgerJlogCost_le_Jlog1
plain-language theorem explainer
If a monotone ledger transition between distinct states L and L' incurs J-log cost at most Jlog(1), then the transition is a single posting step. Recognition Science ledger modelers cite this result to enforce atomicity from cost bounds. The proof derives nonnegativity of deltas from monotonicity, then obtains a contradiction for any delta exceeding 1 by showing that the corresponding Jlog term would exceed the total cost bound via single-term lower bounds and nonnegativity of the remaining sum.
Claim. Let $d$ be a natural number and let $L,L'$ be ledger states over $d$ accounts. If the transition from $L$ to $L'$ is monotone (every debit and credit count is nondecreasing), $L$ differs from $L'$, and the total J-log cost of the integer deltas satisfies ledgerJlogCost$(L,L') ≤ Jlog(1)$, then the transition is a posting step.
background
LedgerState $d$ is the type of ledger configurations consisting of debit and credit vectors over $d$ accounts, drawn from the Recognition ledger structure. MonotoneLedger $L$ $L'$ asserts that every debit and credit entry in $L$ is at most the corresponding entry in $L'$. The ledger J-log cost is the sum of Jlog applied to each integer delta in the debit and credit vectors, where Jlog$(t) = Jcost(exp t)$ and Jcost is the base recognition cost function. This theorem sits inside the LedgerPostingAdjacency module, whose goal is to show that posting-style updates induce one-bit changes in the parity pattern. It relies on the nonnegativity of Jlog and the strict increase property jlog_lt_jlog_of_one_lt for arguments greater than 1.
proof idea
The proof first extracts the debit and credit deltas and establishes their nonnegativity directly from the monotone hypothesis using linarith. It then proves by contradiction that no debit delta can exceed 1: assuming a delta at least 2 produces a Jlog term strictly larger than Jlog(1) by the strict monotonicity lemma, and this term is bounded above by the total ledger cost via the single-element sum inequality and nonnegativity of the credit contribution, contradicting the cost hypothesis. The same argument applies to credit deltas. The remainder assembles these bounds into the definition of PostingStep.
why it matters
This result supplies the cost-to-atomicity implication used by the parent theorem minJlogCost_monotoneStep_implies_postingStep, which replaces the explicit cost bound with a minimality assumption. It closes the gap between the abstract ledger model and the parity-adjacency lemmas in LedgerParityAdjacency, allowing Recognition Science to treat single-tick postings as the only low-cost monotone transitions. The construction aligns with the eight-tick octave by ensuring discrete unit steps.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.