AccountRS
AccountRS supplies the RecognitionStructure carrier for a ledger with exactly d accounts. Model builders invoke it to instantiate AtomicTick and to define posting steps that alter parity in one bit. The construction is a direct record literal with no auxiliary lemmas.
claimFor each natural number $d$, the account recognition structure is the pair $(U := {Fin}_d, R := (fun _ _ => True))$.
background
RecognitionStructure from Chain is the base record with fields U : Type and R : U → U → Prop. The module models a ledger as d accounts whose states evolve by single-unit posts. Upstream AtomicTick class requires postedAt : Nat → U → Prop together with unique_post, which the sibling instance discharges on this carrier. The local setting is the explicit ledger model that replaces abstract vector lemmas with concrete debit-credit updates.
proof idea
Direct definition that populates the RecognitionStructure record with U set to Fin d and R set to the constant true predicate. No lemmas or tactics are applied.
why it matters in Recognition Science
AccountRS is the carrier for LedgerState, accountAt, stepAt and the AtomicTick instance accountRS_atomicTick. It supplies the concrete model needed for the one-bit parity change that feeds the adjacency theorem in LedgerParityAdjacency. The construction closes the ledger-to-parity bridge inside the eight-tick octave evolution of the Recognition framework.
scope and limits
- Does not fix any concrete value of d.
- Does not encode the debit or credit posting rule.
- Does not assert that R encodes a physical interaction.
- Does not derive the AtomicTick instance.
- Does not address mass formulas or phi-ladder rungs.
formal statement (Lean)
35def AccountRS (d : Nat) : RecognitionStructure :=
proof body
Definition body.
36 { U := Fin d, R := fun _ _ => True }
37
38/-!
39### AtomicTick availability (Workstream B tightening)
40
41For the concrete carrier `Fin d` (with `d ≠ 0`), we can construct an `AtomicTick` instance
42directly: at tick `t`, the posted account is the canonical `Fin d` coercion of `t`.
43
44Claim hygiene: this is a *model existence* theorem (THEOREM-level within Lean), not an empirical
45claim about nature’s tick scheduling.
46-/
47