postingStep_implies_legalAtomicTick
plain-language theorem explainer
If L' arises from L by posting one unit to a single account k on debit or credit side, the transition meets the legal atomic tick conditions of monotonicity plus unit L1 cost. Ledger modelers in recognition frameworks cite the result to confirm atomic postings remain admissible steps. The proof unpacks the existential witness in PostingStep and applies the direct lemma establishing legality for the post operation.
Claim. Let $L, L'$ be ledger states over $d$ accounts. If $L'$ is obtained from $L$ by a single atomic posting of one unit at account index $k$ on either debit or credit side, then the transition $L$ to $L'$ is a legal atomic tick: ledger counts remain monotone and the $L^1$ distance equals one.
background
LedgerState d is the Recognition ledger over AccountRS d, pairing debit and credit vectors indexed by Fin d. PostingStep L L' is the predicate that L' equals post L k side for some k and Side. LegalAtomicTick L L' requires MonotoneLedger L L' together with ledgerL1Cost L L' equal to 1. The module upgrades vector lemmas to an explicit ledger model in which each tick posts exactly one unit to one account, thereby inducing one-bit parity changes. Upstream LedgerState structures in variational dynamics treat the configuration as a conserved log-ratio charge, while information-theoretic versions view it as a finite list of recognition events.
proof idea
The term proof destructures the PostingStep hypothesis with rcases to obtain the witness k, side and the definitional equality, then applies the lemma legalAtomicTick_of_post which combines post_monotone and ledgerL1Cost_post to conclude the result.
why it matters
The implication supplies one direction of the equivalence postingStep_iff_legalAtomicTick, which identifies posting steps with legal atomic ticks. It thereby links the ledger posting model to the one-bit parity adjacency already established in LedgerParityAdjacency. Within the Recognition framework the result advances the ledger representation toward the phi-ladder and eight-tick octave by guaranteeing that atomic steps preserve monotonicity and minimal cost. It leaves open the separate derivation of the posting model from physical axioms.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.