legalAtomicTick_oneBitDiff
plain-language theorem explainer
A legal atomic tick between d-dimensional ledger states L and L' forces their parity vectors to differ in exactly one bit. Ledger-based modelers in Recognition Science cite this to link atomic ticks to Gray-code adjacency on parity patterns. The proof is a one-line term composition that first converts the legal tick into a posting step and then applies the posting-step one-bit lemma.
Claim. If ledger states $L$ and $L'$ in dimension $d$ satisfy the legal atomic tick predicate (monotone ledger counts with unit L1 cost), then the parity vectors of $L$ and $L'$ differ in exactly one bit.
background
LedgerState d is the type Recognition.Ledger (AccountRS d), a finite collection of recognition events indexed by accounts in dimension d. LegalAtomicTick L L' is the predicate MonotoneLedger L L' together with ledgerL1Cost L L' = 1, enforcing a unit step that preserves monotonicity. The module models ledger updates as single-account posts (debit or credit), upgrading vector lemmas to explicit ledger-shaped dynamics. Upstream, AtomicTick supplies the unique-posted-at-tick structure, while tick is the RS-native time quantum equal to 1.
proof idea
The term proof applies postingStep_oneBitDiff directly to the result of legalAtomicTick_implies_PostingStep h. This is a one-line wrapper that reduces the legal-tick hypothesis to a posting step and then invokes the already-established one-bit parity change for any posting step.
why it matters
The declaration closes the Workstream B tightening step that converts an RS AtomicTick instance into an explicit PostingStep legality predicate. It supplies the missing glue between ledger language and the parity one-bit adjacency lemma, ensuring that a single post changes phi by ±1 at one coordinate and therefore flips exactly one parity bit. The result sits inside the eight-tick octave structure and supports downstream parity-adjacency arguments without introducing new hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.