MonotoneLedger
plain-language theorem explainer
MonotoneLedger defines the predicate that a ledger update from state L to L' never decreases any debit or credit entry. Ledger-based models of recognition events cite this predicate to enforce incremental posting steps before proving parity adjacency. The definition is the direct conjunction of two componentwise inequalities over the d-dimensional vectors.
Claim. Let $L, L'$ be ledger states in dimension $d$. The predicate holds if and only if $L._{debit}(i) ≤ L'._{debit}(i)$ and $L._{credit}(i) ≤ L'._{credit}(i)$ for every coordinate $i$.
background
LedgerState is the abbreviation Recognition.Ledger (AccountRS d), a pair of debit and credit vectors indexed by Fin d. The module models posting-style ledger updates in which each tick increments exactly one account by one unit, either on the debit or credit side. This supplies the missing link between ledger language and the parity one-bit adjacency result in LedgerParityAdjacency.
proof idea
The definition is a direct encoding: it expands to the conjunction of two universal quantifiers, each asserting componentwise non-decrease on the debit vector and on the credit vector respectively. No lemmas or tactics are invoked; the body is the explicit predicate.
why it matters
MonotoneLedger supplies the monotonicity hypothesis required by LegalAtomicTick and by the theorems minCost_monotoneStep_implies_postingStep, minJlogCost_monotoneStep_implies_postingStep, and post_monotone. It thereby connects ledger increments to the one-bit parity change that realizes the eight-tick octave and D = 3 spatial structure in the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.