LegalAtomicTick
plain-language theorem explainer
LegalAtomicTick defines the predicate on pairs of ledger states L and L' in dimension d that holds when the transition is monotone in debit and credit counts and the L1 cost equals exactly one. Modelers of ledger-based recognition steps cite this predicate to certify that a single account posting meets the minimal conditions for parity adjacency. The definition is the direct conjunction of the MonotoneLedger property and the unit ledgerL1Cost condition.
Claim. For a natural number $d$ and ledger states $L, L'$ (each an instance of Recognition.Ledger over AccountRS $d$, consisting of debit and credit vectors), the predicate LegalAtomicTick holds precisely when the transition from $L$ to $L'$ is monotone and the L1 cost of the change equals 1.
background
The module develops a ledger-shaped model in which each state comprises debit and credit components over $d$ accounts. A tick posts exactly one unit to one account on one side, inducing a change in the phi = debit-credit vector at a single coordinate. This setup supplies the missing glue between ledger language and the parity one-bit adjacency results from LedgerParityAdjacency.
proof idea
The definition is the direct conjunction of MonotoneLedger (d := d) L L' and ledgerL1Cost (d := d) L L' = 1. No lemmas or tactics are invoked; the body simply assembles the two conditions into a single Prop.
why it matters
This predicate is invoked by downstream theorems such as legalAtomicTick_implies_PostingStep, legalAtomicTick_oneBitDiff, and postingStep_iff_legalAtomicTick, which convert the legality conditions into PostingStep and one-bit parity difference. It fills the legality interface in the ledger-to-parity bridge of the module documentation and aligns with minimal-cost transitions in the Recognition framework, consistent with the forcing chain steps that fix D = 3 and the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.