OneBitDiff
plain-language theorem explainer
OneBitDiff declares the predicate that two patterns of dimension d differ in exactly one coordinate. Ledger adjacency and parity proofs cite it to certify that atomic updates produce one-bit flips. The definition is the direct unique-existence statement over the differing index in Fin d.
Claim. For patterns $p, q : (Fin d) → Bool$, the predicate OneBitDiff$(p, q)$ holds precisely when there exists a unique $k : Fin d$ such that $p(k) ≠ q(k)$.
background
The GrayCycle module works with patterns as maps Fin d → Bool, the vertices of the d-dimensional hypercube. Adjacency is the one-coordinate difference relation needed to upgrade cardinality facts to explicit Hamiltonian cycles that match ledger parity updates. Pattern is introduced uniformly as Fin d → Bool in the Patterns, Streams, and Measurement modules, supplying the state space for the cycle construction.
proof idea
The declaration is a definition whose body is the unique-existence quantifier ∃! k : Fin d, p k ≠ q k. No lemmas or tactics are applied; the Prop is introduced directly.
why it matters
OneBitDiff supplies the adjacency primitive for GrayCycle and is invoked in downstream results such as coordAtomicStep_oneBitDiff and postingStep_oneBitDiff. These theorems link atomic ledger steps to one-bit parity changes, supporting the hypercube adjacency required for the 2^D counting bound and D = 3 in the forcing chain. It closes the gap between coverage facts and explicit one-bit adjacency without external Gray-code axioms.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.