legalAtomicTick_of_post
plain-language theorem explainer
A single posting operation on a d-account ledger produces a state that meets the LegalAtomicTick criterion of monotonicity plus unit L1 distance. Researchers modeling recognition events via explicit ledger updates would cite this when verifying that atomic posts preserve legality before invoking parity-adjacency results. The proof is a one-line wrapper that directly invokes post_monotone and ledgerL1Cost_post.
Claim. For a natural number $d$, a ledger state $L$ over $d$ accounts, an index $k$ in Fin $d$, and a side $s$ (debit or credit), the updated ledger post$(L, k, s)$ satisfies LegalAtomicTick$(L, $post$(L, k, s))$, where LegalAtomicTick requires the update to be monotone and to have L1 cost exactly 1.
background
The module models ledger updates as single-unit posts to debit or credit sides of accounts indexed by Fin $d$. LedgerState $d$ is defined as Recognition.Ledger (AccountRS $d$), where AccountRS equips the finite set Fin $d$ with the trivial recognition relation. LegalAtomicTick is the predicate MonotoneLedger $L$ $L'$ together with ledgerL1Cost $L$ $L'$ = 1. Upstream LedgerState structures appear in VariationalDynamics, InformationIsLedger, and Thermodynamics, each supplying a conserved quantity or cost interpretation that the local posting model specializes to integer debit-credit vectors.
proof idea
The proof is a one-line wrapper that refines the goal into the pair consisting of post_monotone applied to the inputs and ledgerL1Cost_post applied to the inputs.
why it matters
This theorem supplies the direct verification that a posting step yields a legal atomic tick, which is then used in postingStep_implies_legalAtomicTick to connect PostingStep to LegalAtomicTick. It forms part of the ledger-shaped model that bridges to the parity one-bit adjacency lemma in LedgerParityAdjacency, advancing the Recognition Science program toward explicit ledger representations of recognition events. It touches the T7 eight-tick octave indirectly through atomic steps but does not yet address physical derivation from the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.