accountAt
accountAt selects the unique account posted at tick t inside a d-account ledger equipped with an AtomicTick instance. Ledger modelers cite it when they need an explicit account selector to build concrete posting steps from the abstract uniqueness guarantee. The definition is a one-line wrapper that applies Classical.choose to the existence witness of unique_post.
claimGiven $d : Nat$ and an AtomicTick instance for the recognition structure whose universe is Fin $d$, the map accountAt$(t)$ returns the unique account in Fin $d$ posted at tick $t$.
background
AccountRS $d$ is the minimal recognition structure with universe Fin $d$ and trivial recognition relation. The AtomicTick class supplies the predicate postedAt : Nat → U → Prop together with the axiom unique_post : ∀ t, ∃! u, postedAt t u. This definition lives in the LedgerPostingAdjacency module, whose doc states that each tick posts exactly one unit to exactly one account (debit or credit) and that the induced parity pattern changes in one bit.
proof idea
The definition is a one-line wrapper. It extracts the existence witness via ExistsUnique.exists applied to AtomicTick.unique_post (M := AccountRS d) t, then feeds that witness to Classical.choose.
why it matters in Recognition Science
accountAt supplies the concrete selector required by the downstream lemmas postedAt_accountAt, stepAt, and stepAt_isPostingStep. It closes the gap between the abstract AtomicTick uniqueness (T2) and the explicit ledger updates that produce one-bit parity adjacency. The module doc positions the construction as the mathematical glue between ledger language and the Gray-code results in LedgerParityAdjacency; no open scaffolding remains here.
scope and limits
- Does not construct an AtomicTick instance for AccountRS d.
- Does not specify a concrete, computable choice function beyond the classical selector.
- Does not determine the debit or credit side of the post.
- Does not derive the one-bit parity change from first principles.
formal statement (Lean)
1002noncomputable def accountAt {d : Nat} [AtomicTick (AccountRS d)] (t : Nat) : Fin d :=
proof body
Definition body.
1003 Classical.choose (ExistsUnique.exists (AtomicTick.unique_post (M := AccountRS d) t))
1004