post_monotone
plain-language theorem explainer
A single unit post on a d-account ledger, incrementing debit or credit at one index, produces a state whose debit and credit vectors are componentwise non-decreasing. Ledger-modeling work in Recognition Science cites the result to certify that atomic updates meet the monotonicity half of the LegalAtomicTick predicate. The term proof cases on Side, then splits each vector inequality by whether the index equals the posted account and applies direct comparison.
Claim. Let $L$ be a ledger state over $d$ accounts. For any account index $k$ and side $s$ (debit or credit), the state obtained by incrementing the chosen debit or credit entry of $L$ by one satisfies MonotoneLedger: every debit count and every credit count is non-decreasing.
background
In LedgerPostingAdjacency a ledger state is an instance of Recognition.Ledger over the structure AccountRS d, which carries two vectors of natural numbers indexed by Fin d: one for debit counts and one for credit counts. MonotoneLedger requires that both vectors are componentwise non-decreasing under the update. The operation post applies exactly one such increment, leaving the opposite vector untouched. The module situates this construction as the concrete carrier that converts vector updates into one-bit parity changes, bridging to the adjacency results of LedgerParityAdjacency.
proof idea
The term proof opens with classical and cases on the Side constructor. For debit it refines to a pair of forall statements; the debit case splits on index equality to k and uses simp to obtain the required inequalities, while credit is unchanged. The credit case is symmetric, again splitting only on the credit vector. All comparisons reduce by direct arithmetic after the index case split.
why it matters
The lemma supplies the monotonicity direction needed by legalAtomicTick_of_post, which in turn feeds the two min-cost implication theorems that characterize posting steps among monotone updates. It therefore anchors the ledger-shaped model that converts single-account increments into the one-bit parity adjacency used downstream. Within the Recognition framework this step realizes the posting-style update required for the parity/Gray adjacency lemma and the eight-tick octave structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.