run_step_oneBitDiff
Advancing a d-account ledger by one posting step changes its parity vector in exactly one bit. Ledger modelers in Recognition Science cite the result to connect explicit posting schedules to Gray-code adjacency on parity patterns. The proof is a one-line simplification that unfolds the run iterator and invokes the single-post parity change lemma.
claimLet $L_t$ be the ledger state reached after $t$ steps of schedule $s$ starting from initial state $L_0$. Then the parity vectors of $L_t$ and $L_{t+1}$ differ in precisely one coordinate.
background
LedgerState d is the type of ledgers with d accounts, each carrying debit and credit balances. PostInstr d is a pair consisting of an account index in Fin d and a side (debit or credit). The run function iterates the schedule to produce the state after any number of ticks. Parity extracts the one-bit pattern induced by the phi-vector of debit-minus-credit differences at each account. The module supplies the explicit posting model that upgrades the abstract parity adjacency result from LedgerParityAdjacency to a concrete ledger-shaped dynamics.
proof idea
The proof is a one-line wrapper. It unfolds the definition of run to expose the single posting at step t, applies the sibling lemma parity_oneBitDiff_of_post, and closes with the definition of parity.
why it matters in Recognition Science
The declaration supplies the missing ledger-to-parity bridge required by the module documentation. It shows that the posting model induces exactly the one-bit adjacency needed for Gray-code evolution of parity vectors. No downstream uses are recorded yet, but the result closes the gap between the abstract parity lemma and the concrete ledger posting mechanics.
scope and limits
- Does not derive why physical systems must adopt this posting model.
- Does not compute explicit parity sequences for concrete schedules.
- Does not address simultaneous multi-postings or continuous-time limits.
- Does not connect directly to the phi-ladder or J-cost formulas.
formal statement (Lean)
1036theorem run_step_oneBitDiff {d : Nat} (L0 : LedgerState d) (sched : Nat → PostInstr d) (t : Nat) :
1037 OneBitDiff (parity d (run L0 sched t)) (parity d (run L0 sched (t + 1))) := by
proof body
Term-mode proof.
1038 -- unfold one step of `run` and apply the single-post theorem
1039 simp [run, parity_oneBitDiff_of_post, parity]
1040
1041end LedgerPostingAdjacency
1042end IndisputableMonolith