minCost_monotoneStep_implies_postingStep
plain-language theorem explainer
Minimal-cost monotone ledger transitions are exactly the atomic posting steps. Recognition Science ledger modelers cite this to establish that unit-cost updates correspond to single-account ticks. The proof reduces the claim to cost exactly 1 by comparing against an explicit debit post at account 0, applies the minimality hypothesis, rules out zero cost via the nontriviality assumption, and invokes the LegalAtomicTick equivalence.
Claim. Let $d$ be a positive integer. Let $L, L'$ be ledger states on $d$ accounts. If the transition $L$ to $L'$ is monotone (all debit and credit counts nondecreasing), $L$ differs from $L'$, and $L'$ minimizes the $L^1$ ledger cost among all monotone nontrivial transitions from $L$, then there exist an account index $k$ and side $s$ (debit or credit) such that $L'$ equals the result of posting one unit to account $k$ on side $s$.
background
The module upgrades vector lemmas to an explicit ledger model in which each tick posts exactly one unit to one account, inducing a one-bit parity change. LedgerState $d$ is the type of debit-credit pairs over the $d$ accounts (Fin $d$ with trivial recognition relation). MonotoneLedger requires that debit and credit counts are nondecreasing in every coordinate. PostingStep asserts existence of $k$ and side such that $L'$ equals post $L$ $k$ side. LegalAtomicTick is the conjunction of MonotoneLedger and ledgerL1Cost equal to 1. The local theoretical setting is the mathematical glue between ledger language and the parity/Gray adjacency lemma.
proof idea
The tactic proof selects a concrete candidate: post at account 0 on the debit side. It verifies monotonicity via post_monotone and cost exactly 1 via ledgerL1Cost_post. The minimality hypothesis then yields ledgerL1Cost of the target transition at most 1. Nonzero cost follows from ledgerL1Cost_eq_zero_iff together with the inequality assumption. Nat.le_one_iff_eq_zero_or_eq_one splits the cases; the zero case is eliminated, leaving cost exactly 1. The equivalence postingStep_iff_legalAtomicTick then concludes PostingStep.
why it matters
This theorem justifies that minimal $L^1$-cost monotone steps are atomic postings and thereby supports the parity one-bit adjacency results in the same module. It fills the ledger-shaped model step between abstract vector updates and the explicit posting mechanics required for Gray-code adjacency. In the Recognition framework it underpins the atomic-tick layer that feeds the eight-tick octave and spatial-dimension derivations, although the ledger model itself remains a modeling choice rather than an axiom.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.