PostingStep
PostingStep defines an atomic ledger update between states L and L' over d accounts as the existence of a single account index k and side such that L' results from incrementing exactly one balance by one unit. Ledger modelers in recognition dynamics cite this to connect discrete postings to one-bit parity shifts in the induced vectors. The definition is the direct existential statement over the account index and debit-credit side.
claimLet $L$ and $L'$ be ledger states over $d$ accounts. The relation holds if there exists an account index $k$ in the finite set of size $d$ and a side $s$ (debit or credit) such that $L'$ is obtained by adding one unit to the chosen balance of account $k$ in $L$.
background
A ledger state for dimension $d$ is the type Recognition.Ledger applied to AccountRS d, the structure that equips the finite set Fin d with a trivial recognition relation. The post operation takes a ledger state, an account index k, and a side, then returns the state with the selected debit or credit balance incremented by one while the other remains fixed. This construction appears in the module whose documentation describes the upgrade from vector lemmas to an explicit ledger model in which each tick posts exactly one unit to exactly one account.
proof idea
The definition is the direct existential quantifier: there exist k in Fin d and side in Side such that L' equals post L k side. No lemmas are applied; the body is the statement itself.
why it matters in Recognition Science
This definition supplies the predicate used by downstream results including postingStep_iff_legalAtomicTick, which equates it with LegalAtomicTick, and postingStep_oneBitDiff, which derives the one-bit difference on parity vectors. It thereby supplies the glue between ledger language and the parity adjacency lemma noted in the module documentation. In the framework this supports the structure of atomic ticks by ensuring each step induces a minimal change in the coordinate system.
scope and limits
- Does not assert that every ledger transition arises from a single post.
- Does not incorporate the recognition relation from AccountRS into the step condition.
- Does not derive the posting model from variational principles or information bounds.
- Does not address simultaneous updates across multiple accounts.
Lean usage
rcases h : PostingStep L L' with ⟨k, side, rfl⟩; exact parity_oneBitDiff_of_post k sideformal statement (Lean)
143def PostingStep {d : Nat} (L L' : LedgerState d) : Prop :=
proof body
Definition body.
144 ∃ k : Fin d, ∃ side : Side, L' = post L k side
145
used by (9)
-
legalAtomicTick_implies_PostingStep -
legalAtomicTick_oneBitDiff -
minCost_monotoneStep_implies_postingStep -
minJlogCost_monotoneStep_implies_postingStep -
postingStep_iff_legalAtomicTick -
postingStep_implies_legalAtomicTick -
postingStep_of_monotone_and_ledgerJlogCost_le_Jlog1 -
postingStep_oneBitDiff -
stepAt_isPostingStep