AccountRS
plain-language theorem explainer
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.
Claim. For 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.