legalAtomicTick_of_post
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.
claimFor 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 in Recognition Science
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.
scope and limits
- Does not establish that every LegalAtomicTick arises from a single post.
- Does not incorporate Jlog-cost variants of the step predicate.
- Does not derive the posting model from the Recognition Composition Law.
- Does not address multi-tick sequences or global conservation.
Lean usage
exact legalAtomicTick_of_post L k sideformal statement (Lean)
748theorem legalAtomicTick_of_post {d : Nat} (L : LedgerState d) (k : Fin d) (side : Side) :
749 LegalAtomicTick (d := d) L (post L k side) := by
proof body
One-line wrapper that applies refine.
750 refine ⟨post_monotone (d := d) L k side, ledgerL1Cost_post (d := d) L k side⟩
751