oneBitDiff_snocBit_flip
The declaration shows that appending false versus true as the final coordinate to any d-dimensional pattern yields two (d+1)-dimensional patterns differing in exactly one position. Researchers constructing recursive Gray cycles cite it to verify adjacency under the BRGC recursion. The proof exhibits the last coordinate as the unique witness and uses Fin.lastCases induction to obtain an immediate contradiction on all prior coordinates.
claimFor every natural number $d$ and every map $p : Fin d → Bool$, the two maps obtained by appending false and true as the final coordinate differ in exactly one position.
background
In this module patterns are maps from Fin d to Bool. The snocBit operation extends such a map by appending a new final coordinate b, defined via Fin.lastCases so that the new coordinate is b and the prefix recovers the original p. OneBitDiff asserts that two patterns differ in exactly one coordinate, i.e., there exists a unique k in Fin (d+1) at which they disagree (Hamming distance 1).
proof idea
The tactic proof opens with classical reasoning and refines the existential witness to Fin.last d. After simp it performs induction on the test coordinate j via Fin.lastCases. The last case is reflexivity. The cast case derives False because the two snocBit patterns agree on every original coordinate, contradicting the assumption hj.
why it matters in Recognition Science
This lemma is invoked by brgc_oneBit_step to establish consecutive one-bit steps along the BRGC path. It supplies the adjacency step inside the recursive construction BRGC(d+1) = [0·BRGC(d), 1·(BRGC(d))ʳ] that yields an axiom-free GrayCycle for arbitrary dimension. The result therefore supports the pattern layer used throughout the Recognition forcing chain and the Recognition Composition Law.
scope and limits
- Does not prove injectivity or wrap-around closure of the full BRGC path.
- Does not treat the base case d = 0.
- Does not address non-recursive or bitwise Gray-code formulas.
- Does not quantify over multiple consecutive steps.
formal statement (Lean)
143private theorem oneBitDiff_snocBit_flip {d : Nat} (p : Pattern d) :
144 OneBitDiff (snocBit p false) (snocBit p true) := by
proof body
Tactic-mode proof.
145 classical
146 refine ⟨Fin.last d, ?_, ?_⟩
147 · simp
148 · intro j hj
149 induction j using Fin.lastCases with
150 | last => rfl
151 | cast j =>
152 have : False := by
153 -- on old coordinates the patterns are equal
154 simpa [snocBit] using hj
155 exact this.elim
156
157/-! ### Relating `natAdd` vs `addNat` when the sizes match -/
158