postedAt_accountAt
plain-language theorem explainer
The lemma confirms that the selector accountAt returns an account satisfying the postedAt predicate for any AtomicTick instance on AccountRS(d). Ledger modelers cite it to verify that the canonical choice aligns with the unique posting rule at each tick. The term-mode proof extracts the existence witness from unique_post via ExistsUnique.exists and applies Classical.choose_spec after unfolding accountAt.
Claim. Let $d$ be a natural number. Suppose AccountRS$(d)$ carries an AtomicTick structure, where AccountRS$(d)$ is the recognition structure with universe Fin$(d)$. Then for every natural number $t$, the postedAt relation holds at tick $t$ for the account $a = $ accountAt$(d,t) in Fin$(d)$, where accountAt selects the unique posted account.
background
AccountRS$(d)$ is the minimal carrier for a $d$-account ledger, defined with universe Fin$(d)$ and trivial recognition relation. The AtomicTick class (from Chain) provides the postedAt predicate together with the unique_post axiom asserting exactly one account is posted per tick. The sibling definition accountAt is the noncomputable selector that applies Classical.choose to the existence witness furnished by unique_post.
proof idea
The term proof first constructs hex as the existence statement ExistsUnique.exists (AtomicTick.unique_post t). It then applies Classical.choose_spec to hex and simplifies with the definition of accountAt to obtain the required postedAt instance.
why it matters
The result anchors the explicit ledger posting model inside the Recognition framework, ensuring the account selector respects atomic tick uniqueness. It supplies the missing link to the parity one-bit adjacency theorem in LedgerParityAdjacency, which in turn feeds the phi-ladder and eight-tick octave constructions. The module positions this as the mathematical glue between ledger language and Gray-code adjacency, leaving empirical derivation of the posting rule as a separate bridge step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.