PostInstr
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.
claimFor 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 in Recognition Science
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.
scope and limits
- Does not impose a nontrivial recognition relation on the accounts.
- Does not represent the full ledger state beyond debit and credit vectors.
- Does not derive the posting schedule from the Recognition Composition Law.
- Does not address continuous-time limits or multi-unit postings.
formal statement (Lean)
1027abbrev PostInstr (d : Nat) : Type := Fin d × Side
proof body
Definition body.
1028
1029/-- Run a ledger forward under a per-tick posting schedule. -/