Patterns Gray Cycle Brgc One Bit Diff Snoc Bit Flip

The flip lemma

A Gray code is a sequence of binary strings in which each consecutive pair differs in exactly one position. The classic example for two bits is 00, 01, 11, 10, which wraps around so the last and first entries also differ by one bit. These sequences matter in digital electronics and mechanical encoders, where a single-bit change between states prevents transient errors. The binary reflected Gray code (BRGC) builds such sequences recursively: to double the length of a code, take the existing sequence, append a 0 to each entry, then take the sequence in reverse order and append a 1 to each entry.

The lemma named oneBitDiff_snocBit_flip concerns the act of appending a single bit to a pattern. In plain terms, it states that if you take any binary pattern and add a 0 at the end, and then take the same pattern and add a 1 at the end, those two resulting patterns differ in exactly one position: the newly appended bit. This is the core step that makes the recursive BRGC construction work, because it guarantees that the boundary between the first half of the doubled sequence and the reversed second half is a valid one-bit transition.

This lemma is proved in the framework's machine-checked library of formal theorems, within a module that constructs Gray cycles for any dimension without relying on the usual bitwise formula gray(n) = n XOR (n >> 1). The proof is axiom-free, meaning it does not add new assumptions to the underlying logic. The lemma itself is a small but load-bearing piece: together with a companion lemma about appending the same bit to two patterns that already differ by one bit, it establishes that the entire recursive path has the one-bit adjacency property, including the wrap-around step.

In Recognition Science, this construction is part of a broader pattern library, but the lemma itself makes no claim about recognition, cost functions, or the forcing chain. It is purely combinatorial. What it does not claim is that this Gray code is the only one, or that the BRGC is optimal in any sense. It does not claim that the recursive construction works for dimension zero, where the adjacency condition is trivially vacuous. And it does not claim that the bitwise formula is equivalent to the recursive definition; the module explicitly avoids that formula. The lemma simply certifies one local fact about appending a bit, and that fact is what lets the recursive construction close its cycles.

private theorem oneBitDiff_snocBit_flip {d : Nat} (p : Pattern d) :
    OneBitDiff (snocBit p false) (snocBit p true) := by
  classical
  refine ⟨Fin.last d, ?_, ?_⟩
  · simp
  · intro j hj
    induction j using Fin.lastCases with
    | last => rfl
    | cast j =>
        have : False := by
          -- on old coordinates the patterns are equal
          simpa [snocBit] using hj
        exact this.elim

noncomputable def brgcGrayCycle (d : Nat) (hdpos : 0 < d) : GrayCycle d :=
{ path := brgcPath d
  inj := brgcPath_injective d
  oneBit_step := brgc_oneBit_step (d := d) hdpos
}

private theorem oneBitDiff_snocBit_flip {d : Nat} (p : Pattern d) :
    OneBitDiff (snocBit p false) (snocBit p true) := by
  classical
  refine ⟨Fin.last d, ?_, ?_⟩
  · simp
  · intro j hj
    induction j using Fin.lastCases with
    | last => rfl
    | cast j =>
        have : False := by
          -- on old coordinates the patterns are equal
          simpa [snocBit] using hj
        exact this.elim

What this page does not claim

This lemma does not claim that the binary reflected Gray code is the unique or optimal Gray code for any dimension. This lemma does not claim that the recursive construction works for dimension zero, where the adjacency condition is vacuous. This lemma does not claim that the bitwise formula gray(n) = n XOR (n >> 1) is equivalent to the recursive definition.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Patterns/GrayCycleBRGC.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: