Patterns Gray Cycle Brgc One Bit Diff Snoc Bit Same

The append lemma

A Gray code is a sequence of binary patterns in which consecutive entries differ by exactly one bit. The most famous example is the binary reflected Gray code, which for a given number of bits lists all possible patterns so that each step flips a single bit, including the wrap-around from the last entry back to the first. The declaration oneBitDiff_snocBit_same concerns a specific operation in this setting: appending a new last bit to a pattern. The lemma states that if two patterns already differ by exactly one bit, then appending the same bit value to both of them preserves that one-bit difference.

This is a structural property of the recursive construction. The standard way to build a Gray code for d+1 bits is to take the code for d bits, list it forward with a 0 appended, then list it in reverse with a 1 appended. The lemma guarantees that within each half of this construction, the one-bit adjacency property is inherited from the smaller code. Without it, the recursive step would not preserve the defining feature of a Gray code. The machine-checked library of formal theorems proves this lemma as part of a larger, axiom-free construction of Gray cycles for any positive dimension.

The theorem does not claim anything about what happens when different bits are appended to two patterns, nor does it address the flip case where one pattern gets a 0 and the other gets a 1. Those are separate facts, handled by a companion lemma. It also does not establish that the full Gray cycle has the one-bit property; that is a larger theorem that uses this lemma as one ingredient. The lemma is a local statement about a single operation, not a global claim about sequences.

What the lemma gives a reader is a precise guarantee about a basic building block. It says that the operation of appending a bit is, in a specific sense, safe: it does not destroy the one-bit difference that already exists between two patterns. This is the kind of small, exact fact that makes larger constructions trustworthy, because each step can be checked independently before being composed into a full cycle.

private theorem oneBitDiff_snocBit_same {d : Nat} {p q : Pattern d} (b : Bool) :
    OneBitDiff p q → OneBitDiff (snocBit p b) (snocBit q b) := by
  intro h
  classical
  rcases h with ⟨k, hk, hkuniq⟩
  refine ⟨k.castSucc, ?_, ?_⟩
  · simpa using hk
  · intro j hj
    -- any differing coordinate cannot be the new last coordinate (since it is fixed to `b`)
    induction j using Fin.lastCases with
    | last =>
        have : False := by
          simpa [snocBit] using hj
        exact this.elim
    | cast j =>
        have hj' : p j ≠ q j := by
          simpa [snocBit] using hj
        have : j = k := hkuniq j hj'
        simpa [this]

What this page does not claim

The lemma does not claim that appending different bits to two patterns preserves one-bit difference. The lemma does not claim that the full Gray cycle has the one-bit property; that is a separate theorem. The lemma does not address the flip case where one pattern gets a 0 and the other gets a 1.

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: