accountRS_atomicTick
plain-language theorem explainer
Researchers modeling ledger updates in Recognition Science cite this instance to equip the d-account structure with an AtomicTick relation. It defines the posted account at tick t as the modular reduction t mod d within Fin d. The construction proceeds by direct definition of postedAt together with a uniqueness proof that reduces to reflexivity and simplification.
Claim. For the recognition structure $M$ with universe $U = $ Fin $d$ ($d > 0$) and trivial recognition relation, the instance supplies postedAt$(t,u)$ holding precisely when $u$ is the canonical embedding of $t$ mod $d$ into Fin $d$, together with the uniqueness axiom that each $t$ determines a unique such $u$.
background
AccountRS $d$ is the minimal RecognitionStructure whose universe is the finite set Fin $d$ and whose recognition relation is constantly true. The module LedgerPostingAdjacency employs this carrier to model a ledger in which each tick posts exactly one unit to one account (debit or credit). The upstream AtomicTick class (from Recognition and its re-export in RRF.Core) is the interface requiring a postedAt predicate Nat → U → Prop together with the axiom ∀ t, ∃! u, postedAt t u.
proof idea
The instance is supplied by explicit construction of the two fields. postedAt is defined via the equality u = ⟨t % d, Nat.mod_lt …⟩. The unique_post field is discharged by exhibiting the witness ⟨t % d, …⟩ and then applying simpa to the uniqueness subgoal after assuming the hypothesis hu.
why it matters
This declaration supplies the concrete AtomicTick model needed to derive one-bit parity adjacency from ledger posting steps. It instantiates the atomic tick axiom for finite account carriers, closing the model-existence step between abstract RecognitionStructure and the parity lemmas (parity_oneBitDiff_of_post, phiVec_post_debit) in the same module. Within the framework it realizes the atomic tick requirement for Workstream B ledger models without invoking the full J-cost or phi-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.