run
plain-language theorem explainer
The run definition iterates an initial ledger state forward by applying one single-account debit or credit posting per tick according to a supplied schedule. Models of recognition cost and parity evolution cite this operator to obtain discrete time steps that feed one-bit adjacency theorems. The definition is a direct recursion whose successor clause invokes the post operation on the state obtained at the previous tick.
Claim. Let $L_0$ be a ledger state on $d$ accounts and let $sched : ℕ → Fin(d) × Side$ be a posting schedule. Define the map $r : ℕ → LedgerState(d)$ by $r(0) := L_0$ and $r(t+1) := post(r(t), k, s)$ where $(k,s) = sched(t)$.
background
A LedgerState(d) is the Recognition ledger whose accounts are indexed by Fin d, each carrying a debit counter and a credit counter. PostInstr(d) is the type Fin(d) × Side, pairing an account index with a debit or credit side. The post operation adds one unit to the chosen counter of the chosen account while leaving the opposite counter unchanged. The module therefore supplies an explicit posting-style update rule whose parity vector changes in exactly one bit, linking the ledger model to the Gray-code adjacency results of LedgerParityAdjacency.
proof idea
The definition is given by pattern matching on the natural-number argument. The zero case returns the supplied initial state L0. The successor case recurses to obtain the state at t and then applies the single-post function to that state using the account and side extracted from sched(t).
why it matters
This definition supplies the time-evolution map required by the downstream theorem run_step_oneBitDiff, which proves that consecutive parity vectors differ by exactly one bit. It thereby supplies the discrete ledger dynamics used in ILG kernel estimates, Navier-Stokes skew identities, and the r-prediction bound in primordial spectrum calculations. Within the Recognition framework the construction realizes the posting model that underpins the eight-tick octave and the derivation of three spatial dimensions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.