stepAt_isPostingStep
Advancing a d-account ledger by one tick under a prescribed debit-credit schedule yields a valid single-account posting step. Parity-adjacency arguments cite this to chain the one-bit difference property across successive ticks. The argument is a direct refinement that exhibits the posted account and chosen side as witnesses.
claimLet $d$ be a natural number equipped with an atomic tick structure on the $d$-account ledger carrier. For any side schedule assigning debit or credit to each tick, any tick $t$, and any ledger state $L$, the state reached after one step is obtained from $L$ by posting one unit to a single account on the prescribed side.
background
The module constructs an explicit ledger model in which each tick posts exactly one unit to one of $d$ accounts, either debit or credit. AccountRS d is the recognition structure whose universe is Fin d with the trivial recognition relation. LedgerState d is the ledger type built over this carrier. PostingStep is the proposition that there exist an account index k in Fin d and a side such that the successor state equals the result of the post operation applied to L at k on that side. The AtomicTick class guarantees a unique posted account at each tick t via its unique_post axiom.
proof idea
The proof is a one-line wrapper that refines the existential quantifier in the definition of PostingStep. It supplies the account returned by accountAt at tick t, the side taken from the schedule at t, and reflexivity to confirm equality with the post operation.
why it matters in Recognition Science
This lemma is the direct hypothesis for the theorem stepAt_oneBitDiff, which shows that a per-tick posting schedule produces an adjacent walk in parity space. It supplies the ledger-to-parity glue step described in the module documentation and supports the Recognition framework's derivation of one-bit adjacency from atomic updates. No open scaffolding questions are closed here.
scope and limits
- Does not prove that nature must evolve ledgers by single postings.
- Does not treat simultaneous updates to multiple accounts.
- Does not fix a concrete value of d or an explicit side schedule.
- Does not derive the parity map or the one-bit difference property itself.
Lean usage
postingStep_oneBitDiff (stepAt_isPostingStep (d := d) sideAt t L)formal statement (Lean)
1016lemma stepAt_isPostingStep {d : Nat} [AtomicTick (AccountRS d)] (sideAt : Nat → Side) (t : Nat) (L : LedgerState d) :
1017 PostingStep (d := d) L (stepAt (d := d) sideAt t L) := by
proof body
One-line wrapper that applies refine.
1018 refine ⟨accountAt (d := d) t, sideAt t, rfl⟩
1019