PostInstr
plain-language theorem explainer
PostInstr defines the type of per-tick posting instructions for a d-account ledger as a pair of an account index in Fin d and a debit or credit side. Ledger evolution models in Recognition Science cite this when constructing schedules that drive one-bit parity adjacency. The declaration is a direct type abbreviation with no proof content.
Claim. For a natural number $d$, a posting instruction is a pair $(k,s)$ where $k$ belongs to the finite set with $d$ elements and $s$ is either debit or credit.
background
The module upgrades vector-based lemmas to an explicit ledger model in which each tick posts exactly one unit to one account on either the debit or credit side. Side is the inductive type carrying the two constructors debit and credit. AccountRS equips the carrier Fin d with the trivial recognition relation that holds between any pair of accounts. The local setting is a mathematical model that supplies the missing glue between ledger language and the parity one-bit adjacency result in LedgerParityAdjacency.
proof idea
The declaration is a direct type abbreviation pairing Fin d with the inductive Side type.
why it matters
PostInstr supplies the instruction type consumed by the run function that evolves a LedgerState under a per-tick schedule. It directly enables the downstream theorem run_step_oneBitDiff, which establishes that each posting step changes the parity vector in exactly one bit. This realizes the module's key claim that a single post induces a one-bit parity change, bridging ledger posting to the Gray-adjacency structure required by the eight-tick octave in the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.