postingStep_oneBitDiff
A single atomic posting on a d-dimensional ledger changes the parity vector in exactly one bit. Researchers modeling recognition events via discrete ledger updates cite this to connect account postings to Gray-code adjacency in parity space. The proof performs case analysis on the existential PostingStep hypothesis and applies the specialized parity change lemma for the post operation.
claimIf $L'$ is obtained from ledger state $L$ by a single posting step in dimension $d$, then the parity vectors of $L$ and $L'$ differ in exactly one bit.
background
LedgerState d is the Recognition Ledger over AccountRS d, which records debit and credit counts for each of d accounts. PostingStep L L' holds when there exist an account index k and a side such that L' equals the result of posting one unit to that side of account k in L. The parity function extracts a bit vector from the ledger, and OneBitDiff asserts that two such vectors differ in precisely one position. This module supplies the ledger-shaped model that upgrades vector lemmas to explicit posting updates, as described in the module documentation.
proof idea
The proof performs case analysis on the PostingStep hypothesis to extract the account index k and side, then applies parity_oneBitDiff_of_post via simpa.
why it matters in Recognition Science
This theorem is the base case invoked by legalAtomicTick_oneBitDiff and stepAt_oneBitDiff, which lift it to legal atomic ticks and scheduled per-tick steps. It supplies the missing glue between ledger language and the parity/Gray adjacency lemma, supporting the discrete update structure underlying the eight-tick octave in the Recognition framework. The module documentation flags that deriving the posting model itself from core axioms remains a separate bridge step.
scope and limits
- Does not prove that all physical state changes must occur via single postings.
- Does not compute explicit values of the parity vector or link it to measured quantities.
- Does not address multi-step transitions or continuous-time limits.
- Does not derive the posting model from the Recognition axioms.
Lean usage
theorem example {d : Nat} {L L' : LedgerState d} (h : LegalAtomicTick (d := d) L L') : OneBitDiff (parity d L) (parity d L') := postingStep_oneBitDiff (legalAtomicTick_implies_PostingStep h)formal statement (Lean)
146theorem postingStep_oneBitDiff {d : Nat} {L L' : LedgerState d} (h : PostingStep (d := d) L L') :
proof body
Tactic-mode proof.
147 OneBitDiff (parity d L) (parity d L') := by
148 rcases h with ⟨k, side, rfl⟩
149 simpa using parity_oneBitDiff_of_post (d := d) L k side
150
151/-! ## Optional deepening: a cost/legality predicate that implies `PostingStep` -/
152
153/-- L1 cost of a ledger transition, measured as total absolute change in debit+credit counts. -/