run_step_oneBitDiff
plain-language theorem explainer
The theorem asserts that each posting step on a d-account ledger changes the induced parity vector by exactly one bit. Ledger modelers in Recognition Science cite it to link explicit debit-credit posting rules to Gray-code adjacency. The proof is a one-line simp that unfolds the run iterator and invokes the single-post parity lemma.
Claim. Let $d$ be a natural number, $L_0$ a ledger state on $d$ accounts, $sched : ℕ → (Fin d × Side)$ a posting schedule, and $t ∈ ℕ$. Then the parity vectors after $t$ and $t+1$ steps satisfy OneBitDiff(parity_d(run(L_0, sched, t)), parity_d(run(L_0, sched, t+1))).
background
The module upgrades a vector lemma to an explicit ledger model in which each tick posts one unit to exactly one account (debit or credit). LedgerState d is defined as Recognition.Ledger (AccountRS d). PostInstr d is the type Fin d × Side. The run function iterates the schedule forward from L_0.
proof idea
Term-mode proof consisting of a single simp [run, parity_oneBitDiff_of_post, parity]. The tactic unfolds one application of the posting step inside run and reduces the parity difference directly via the single-post theorem.
why it matters
It supplies the missing glue between ledger posting language and the parity/Gray adjacency result in LedgerParityAdjacency. The module doc states that a single post changes phi = debit-credit by ±1 at one coordinate, inducing the one-bit parity change. In the Recognition framework this supports the discrete tick structure by showing how ledger steps produce adjacent parity states.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.