stepAt_oneBitDiff
The theorem shows that applying a single per-tick posting to a d-account ledger changes its parity vector by exactly one bit. Ledger-model researchers in Recognition Science cite it to link explicit posting mechanics to Gray-code adjacency in parity space. The proof is a direct term application of the general posting-step adjacency lemma to the concrete stepAt construction.
claimLet $d$ be a natural number and assume an atomic-tick instance for the $d$-account ledger structure. Given a side-assignment function sideAt, a tick $t$, and any ledger state $L$, the parity vector of $L$ differs from the parity vector of the state obtained by posting one unit (debit or credit) at the account selected by sideAt at tick $t$ in exactly one coordinate.
background
AccountRS d is the minimal recognition structure whose universe is Fin d (d accounts) with the trivial recognition relation. LedgerState d is the abbreviation for Recognition.Ledger (AccountRS d), i.e., a configuration of debit and credit entries indexed by the d accounts. Side is the inductive type with constructors debit and credit; a posting applies one unit to exactly one account on one side. AtomicTick supplies the postedAt predicate and uniqueness axiom that guarantee each tick selects a unique account. The module states that a ledger state consists of (debit, credit) pairs and that each tick posts exactly one unit to one account, inducing a ±1 change in the phi = debit-credit vector at a single coordinate and therefore a one-bit flip in the induced parity pattern.
proof idea
The proof is a one-line term wrapper: it instantiates the general lemma postingStep_oneBitDiff on the concrete fact that stepAt (sideAt t L) satisfies the PostingStep predicate, which is supplied by the sibling lemma stepAt_isPostingStep.
why it matters in Recognition Science
This declaration supplies the explicit ledger-shaped model that converts the abstract parity-adjacency result of LedgerParityAdjacency into a concrete posting schedule. It completes the module-level claim that a per-tick posting induces an adjacent walk in parity space, bridging the AtomicTick class and the Recognition.Ledger structure to the one-bit difference relation. The result sits inside the larger ledger-to-parity pipeline that supports the Recognition Composition Law and the eight-tick octave structure; no downstream uses are yet recorded.
scope and limits
- Does not derive the posting model from the core recognition axioms.
- Does not compute explicit parity vectors or their evolution for concrete d.
- Does not address multi-tick or continuous-time limits.
- Does not connect the one-bit change to physical constants or spatial dimension D=3.
formal statement (Lean)
1020theorem stepAt_oneBitDiff {d : Nat} [AtomicTick (AccountRS d)] (sideAt : Nat → Side) (t : Nat) (L : LedgerState d) :
1021 OneBitDiff (parity d L) (parity d (stepAt (d := d) sideAt t L)) :=
proof body
Term-mode proof.
1022 postingStep_oneBitDiff (stepAt_isPostingStep (d := d) sideAt t L)
1023
1024/-! ## A per-tick posting schedule induces an adjacent walk in parity space -/
1025
1026/-- A per-tick posting instruction: (account index, side). -/