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