accountRS_atomicTick
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.
claimFor 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 in Recognition Science
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.
scope and limits
- Does not claim that nature employs a finite number of accounts.
- Does not derive the value of d from physical constants or the phi-ladder.
- Does not connect the trivial recognition relation to J-cost or Recognition Composition Law.
- Does not prove any empirical scheduling property of ticks.
formal statement (Lean)
48noncomputable instance accountRS_atomicTick (d : Nat) [NeZero d] : Recognition.AtomicTick (AccountRS d) :=
proof body
Definition body.
49{ postedAt := fun t u =>
50 u = ⟨t % d, Nat.mod_lt _ (Nat.pos_of_ne_zero (NeZero.ne d))⟩
51 unique_post := by
52 intro t
53 refine ⟨⟨t % d, Nat.mod_lt _ (Nat.pos_of_ne_zero (NeZero.ne d))⟩, rfl, ?_⟩
54 intro u hu
55 simpa [hu]
56}
57