oneBitDiff_snocBit_same
plain-language theorem explainer
The lemma shows that single-bit differences between two patterns of dimension d remain single-bit differences after the same boolean bit is appended to each. Researchers constructing recursive Gray cycles via BRGC would cite this preservation step. The proof extracts the original differing index, lifts it by castSucc, and applies Fin.lastCases to rule out the new coordinate as a possible difference site.
Claim. If patterns $p, q :$ Pattern $d$ satisfy OneBitDiff $p$ $q$, then for any boolean $b$, OneBitDiff (snocBit $p$ $b$) (snocBit $q$ $b$) holds.
background
Pattern $d$ denotes a length-$d$ binary string (finite window) drawn from the Patterns module. snocBit appends a single boolean coordinate to such a string. OneBitDiff $p$ $q$ asserts that $p$ and $q$ differ in exactly one coordinate position. The GrayCycleBRGC module builds the BRGC path recursively: the $d+1$ case splits the index range into a left half with appended false and a right half with appended true, using the $d$-case path on reversed indices for the right half. This lemma propagates the adjacency property through that recursion. Upstream OneBitDiff is supplied by the GrayCycle sibling module.
proof idea
The tactic proof intros the hypothesis, invokes classical, and rcases to obtain the unique differing index $k$. It refines the new witness to $k$.castSucc. The first subgoal is discharged by simpa. The uniqueness subgoal proceeds by induction on the candidate index $j$ via Fin.lastCases: the last case produces a contradiction because the appended bits match, while the cast case reduces the inequality to the original uniqueness statement via simpa.
why it matters
The result is invoked directly by brgc_oneBit_step, which establishes the one-bit step property of the full BRGC path. Together with brgcPath_injective it completes the inductive verification that the recursive construction yields a Gray cycle (one-bit transitions, no repeats) for every dimension. The module supplies an axiom-free general-$D$ GrayCycle implementation independent of bitwise formulas, supporting the pattern layer of the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.