oneBitDiff_snocBit_same
plain-language theorem explainer
If two d-bit patterns differ in exactly one position, appending the same bit b to both yields (d+1)-bit patterns that still differ in exactly one position. This preservation step is invoked during the inductive construction of the BRGC Gray cycle. The proof lifts the original differing index via castSucc, then uses Fin.lastCases to obtain a contradiction at the appended coordinate while recovering uniqueness on the prefix.
Claim. Let $p,q$ be patterns of length $d$ and let $b$ be a bit. If $p$ and $q$ differ in precisely one coordinate, then the extended patterns obtained by appending $b$ to each also differ in precisely one coordinate.
background
The module constructs an axiom-free Gray cycle for arbitrary dimension via the standard recursive BRGC definition: BRGC(0) is the single 0-bit pattern and BRGC(d+1) appends a fixed bit (0 on the left half, 1 on the reversed right half) to the patterns of dimension d. Pattern d denotes a length-d binary string; OneBitDiff p q asserts that p and q differ in exactly one coordinate. snocBit p b is the operation that appends bit b, used to build the left and right halves of brgcPath (d+1).
proof idea
Assume OneBitDiff p q witnessed by index k together with uniqueness. The proof refines the witness to k.castSucc. The first conjunct follows by simplification of the appended coordinate. Uniqueness is shown by induction on the target index via Fin.lastCases: the last coordinate yields an immediate contradiction because both extensions carry the same bit b; the cast case reduces to the original uniqueness after simplification.
why it matters
The lemma is applied inside brgc_oneBit_step to establish one-bit adjacency along the recursive BRGC path. It therefore contributes to the packaged GrayCycle d and GrayCover d (2^d) statements that close the module. In the Recognition framework this supplies the combinatorial one-bit adjacency required for the pattern layer, independent of bitwise Gray-code formulas and without axioms.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.