Encyclopedia Patterns Patterns Gray Cycle Brgc Brgc One Bit Step

ARTICLE 3 claims 3 theorems

Patterns Gray Cycle Brgc Brgc One Bit Step

A Gray code is a way to list binary strings so that each entry differs from the last by a single bit, and this theorem shows a standard construction always has that property.

Verify this page

The one-bit step

A Gray code is an ordered list of all binary strings of a fixed length, usually called a dimension, in which every string differs from the one before it by changing exactly one bit. The classic example for two bits runs 00, 01, 11, 10, and then wraps back to 00, again with a single bit change. Such codes matter in digital encoders and rotary sensors, where a mechanical position is read as a binary pattern and a multi-bit change at a boundary could be misread as a wild jump. The idea dates to Frank Gray, a Bell Labs researcher who patented the reflected binary code in 1953, though the underlying reflection principle was known earlier.

The standard way to build a Gray code for any dimension is the recursive reflected construction, often called BRGC after the binary reflected Gray code. Start with the single string 0 in dimension zero. For dimension d+1, take the list for dimension d, prefix every string with 0, then take the same list in reverse order, prefix every string with 1, and concatenate the two halves. This gives 2^(d+1) strings, and the reflection at the join is exactly what makes the wrap-around work. The construction is simple enough to write by hand, but proving that it always has the one-bit property, for every dimension and every step including the final wrap, is a formal task.

The machine-checked library of formal theorems contains a proof of exactly that claim. Its theorem, brgc_oneBit_step, states that for any positive dimension d and any index i in the list, the pattern at position i and the pattern at position i+1 differ by one bit. The proof proceeds by induction on the dimension, splitting the list into its two reflected halves and checking the join where the reflection happens. The same library also proves that the construction never repeats a string and that it covers every possible pattern, which together mean it is a genuine cycle through the whole space of binary strings.

In Recognition Science, this theorem is one small gear in a larger account of how patterns are recognized and compared. The framework models recognition as a discrete record of events, and the cost of moving from one pattern to another is forced by a proved uniqueness theorem. A Gray cycle offers a path through pattern space where each step has the same minimal cost, a single bit flip, which the framework interprets as a natural unit of change. The theorem does not itself say anything about recognition or cost; it is a purely combinatorial fact about binary strings that the framework can then use.

What the theorem does not claim is just as important. It does not say that the BRGC construction is the only Gray code, nor that it is optimal in any sense beyond the one-bit property. It does not use the common bitwise formula gray(n) = n XOR (n >> 1), and it does not depend on any axioms about Gray codes; the construction and its properties are proved from scratch. The theorem also does not apply to dimension zero, where the single empty pattern has no neighbor, and it says nothing about what happens if you allow changes of more than one bit.

THEOREM brgc_oneBit_step · IndisputableMonolith/Patterns/GrayCycleBRGC.lean
brgc_oneBit_step · IndisputableMonolith/Patterns/GrayCycleBRGC.lean:209 · truncated 
theorem brgc_oneBit_step : ∀ {d : Nat}, 0 < d →
    ∀ i : Fin (2 ^ d), OneBitDiff (brgcPath d i) (brgcPath d (i + 1))
  | 0, hdpos => (Nat.not_lt_zero _ hdpos).elim
  | 1, _ => by
      intro i
      -- dimension 1: the cycle is `0 → 1 → 0`, so the only bit flips each step
      fin_cases i
      · -- 0 → 1
        have : OneBitDiff (snocBit (brgcPath 0 0) false) (snocBit (brgcPath 0 0) true) :=
          oneBitDiff_snocBit_flip (p := brgcPath 0 0)
        simpa [brgcPath] using this
      · -- 1 → 0 (wrap), use symmetry
        have h : OneBitDiff (snocBit (brgcPath 0 0) false) (snocBit (brgcPath 0 0) true) :=
          oneBitDiff_snocBit_flip (p := brgcPath 0 0)
        have : OneBitDiff (snocBit (brgcPath 0 0) true) (snocBit (brgcPath 0 0) false) :=
          OneBitDiff_symm h
        simpa [brgcPath] using this
  | (d + 2), _ => by
      -- Inductive step: assume one-bit stepping for dimension `d+1`, prove for `d+2`.
      have ih :
          ∀ i : Fin (2 ^ (d + 1)), OneBitDiff (brgcPath (d + 1) i) (brgcPath (d + 1) (i + 1)) :=
        brgc_oneBit_step (d := d + 1) (Nat.succ_pos _)
      intro i
      classical
      let T : Nat := 2 ^ (d + 1)
      have hTT : 2 ^ (d + 2) = T + T := by
        simpa [T] using twoPow_succ_eq_add (d := d + 1)
      let left : Fin T → Pattern (d + 2) := fun k => snocBit (brgcPath (d + 1) k) false
      let right : Fin T → Pattern (d + 2) := fun k => snocBit (brgcPath (d + 1) (Fin.rev k)) true
      let i' : Fin (T + T) := i.cast hTT

      have hTpos : 0 < T := pow_pos (by decide : 0 < (2 : Nat)) (d + 1)
      letI : NeZero T := ⟨Nat.ne_zero_of_lt hTpos⟩
      letI : NeZero (T + T) := ⟨Nat.ne_zero_of_lt (Nat.add_pos_left hTpos T)⟩

      have hcast_succ : (i + 1).cast hTT = i' + 1 := by
        -- `cast` commutes with `+1` along definitional equalities
        simpa [i'] using (cast_add_one (n := 2 ^ (d + 2)) (m := T + T) (h := hTT) i)

      -- Reduce to the `Fin (T+T)` index space.
      have hTTgoal : OneBitDiff (Fin.append left right i') (Fin.append left right (i' + 1)) := by
        -- case split on whether `i'` lies in the left or right half, and whether we cross a boundary
        induction i' using Fin.addCases with
        | left k =>
            -- i' = castAdd T k
            by_cases hk : k.val + 1 < T
            · -- successor stays in the left half
              have hk_big : (Fin.castAdd T k : Fin (T + T)).val + 1 < T + T := by
                -- k.val + 1 < T ≤ T+T
                exact lt_of_lt_of_le hk (Nat.le_add_right T T)
              have hnext : (Fin.castAdd T k : Fin (T + T)) + 1 = Fin.castAdd T (k + 1) := by
                apply Fin.ext
                have hk1 : (k + 1).val = k.val + 1 :=
                  Fin.val_add_one_of_lt' (n := T) (i := k) hk
                have hk'1 : ((Fin.castAdd T k : Fin (T + T)) + 1).val =
                    (Fin.castAdd T k : Fin (T + T)).val + 1 :=
                  Fin.val_add_one_of_lt' (n := T + T) (i := Fin.castAdd T k) hk_big
                simpa [hk1] using hk'1
              -- adjacency comes from IH in dimension d+1, lifted through `snocBit`
              have hstep : OneBitDiff (brgcPath (d + 1) k) (brgcPath (d + 1) (k + 1)) := ih k
              have hstep' : OneBitDiff (left k) (left (k + 1)) :=
                oneBitDiff_snocBit_same false hstep
              -- rewrite the `append` evaluations
              simpa [Fin.append_left, hnext, left, right] using hstep'
            · -- boundary: last element of left half steps into the first element of right half
              have hkval : k.val = T - 1 := by
                have hle : k.val + 1 ≤ T := Nat.succ_le_of_lt k.isLt
                have hge : T ≤ k.val + 1 := Nat.le_of_not_gt hk
                have : k.val + 1 = T := Nat.le_antisymm hle hge
                exact Nat.eq_sub_of_add_eq this
              have hnext : (Fin.castAdd T k : Fin (T + T)) + 1 = Fin.natAdd T 0 := by
                apply Fin.ext
                -- both have value `T`
                have hT1 : 1 ≤ T := Nat.succ_le_of_lt hTpos
                have hkplus : (Fin.castAdd T k : Fin (T + T)).val + 1 = T := by
                  -- `(castAdd T k).val = k.val = T-1`
                  simpa [hkval, Nat.sub_add_cancel hT1]
                have hk_big : (Fin.castAdd T k : Fin (T + T)).val + 1 < T + T := by
                  -- `T < T+T` since `T>0`
                  have hT1 : 1 ≤ T := Nat.succ_le_of_lt hTpos
                  have hTlt : T < T + T := by
                    have hle : T + 1 ≤ T + T := Nat.add_le_add_left hT1 T
                    exact lt_of_lt_of_le (Nat.lt_succ_self T) hle
                  -- rewrite the LHS using `hkplus : (castAdd ...).val + 1 = T`
                  exact hkplus.symm ▸ hTlt
                have hk'1 : ((Fin.castAdd T k : Fin (T + T)) + 1).val =
                    (Fin.castAdd T k : Fin (T + T)).val + 1 :=
                  Fin.val_add_one_of_lt' (n := T + T) (i := Fin.castAdd T k) hk_big
                have hval : ((Fin.castAdd T k : Fin (T + T)) + 1).val = T := by
                  exact hk'1.trans hkplus
                -- `natAdd T 0` has val `T`
                simpa [hval]
              -- show underlying index on the right is also `k` (since `rev 0` is last)
              have hrev0 : Fin.rev (0 : Fin T) = k := by
                apply Fin.ext
                -- `rev 0` has value `T-1`
                simpa [hkval] using (Fin.val_rev_zero (n := T))
              have hstep' : OneBitDiff (left k) (right 0) := by
                -- same underlying pattern, last bit flips
                simpa [left, right, hrev0] using (oneBitDiff_snocBit_flip (p := brgcPath (d + 1) k))
              -- rewrite `append` at the boundary indices explicitly (avoid `natAdd`/`addNat` mismatch issues)
              have happL : Fin.append left right (Fin.castAdd T k) = left k := by
                simpa using (Fin.append_left (u := left) (v := right) k)
              have happNext : Fin.append left right ((Fin.castAdd T k : Fin (T + T)) + 1) = right 0 := by
                have : Fin.append left right (Fin.natAdd T (0 : Fin T)) = right 0 := by
                  simpa using (Fin.append_right (u := left) (v := right) (i := (0 : Fin T)))
                simpa [hnext] using this
              have hstep0 : OneBitDiff (Fin.append left right (Fin.castAdd T k)) (right 0) := by
                simpa [happL] using hstep'
              -- replace `right 0` with the `append` at the successor index
              simpa [happNext.symm] using hstep0
        | right k =>
            -- i' = natAdd T k
            by_cases hk : k.val + 1 < T
            · -- successor stays in the right half
              have hk_big : (Fin.natAdd T k : Fin (T + T)).val + 1 < T + T := by
                -- (T + k.val) + 1 < T + T since k.val + 1 < T
                have : T + (k.val + 1) < T + T := Nat.add_lt_add_left hk T
                simpa [Fin.natAdd, Nat.add_assoc] using this
              have hnext : (Fin.natAdd T k : Fin (T + T)) + 1 = Fin.natAdd T (k + 1) := by
                apply Fin.ext
                have hk1 : (k + 1).val = k.val + 1 :=
                  Fin.val_add_one_of_lt' (n := T) (i := k) hk
                have hk'1 : ((Fin.natAdd T k : Fin (T + T)) + 1).val =
                    (Fin.natAdd T k : Fin (T + T)).val + 1 :=
                  Fin.val_add_one_of_lt' (n := T + T) (i := Fin.natAdd T k) hk_big
                simpa [hk1, Nat.add_assoc, Nat.add_left_comm, Nat.add_comm] using hk'1
              -- adjacency comes from IH in dimension d+1, but the right half is reversed
              have hrevStep : OneBitDiff
                  (brgcPath (d + 1) (Fin.rev (k + 1))) (brgcPath (d + 1) ((Fin.rev (k + 1)) + 1)) := ih (Fin.rev (k + 1))
              have hrevRel : (Fin.rev (k + 1) : Fin T) + 1 = Fin.rev k := by
                -- rev(k+1) + 1 = rev(k) when k.val+1 < T
                -- use the helper lemma on `Fin T`
                simpa [Nat.add_assoc] using (rev_add_one_eq (n := T) (i := k) hk)
              have hstep0 : OneBitDiff (brgcPath (d + 1) (Fin.rev (k + 1))) (brgcPath (d + 1) (Fin.rev k)) := by
                simpa [hrevRel] using hrevStep
              have hstep1 : OneBitDiff (brgcPath (d + 1) (Fin.rev k)) (brgcPath (d + 1) (Fin.rev (k + 1))) :=
                OneBitDiff_symm hstep0
              have hstep' : OneBitDiff (right k) (right (k + 1)) :=
                oneBitDiff_snocBit_same true hstep1
              -- rewrite `append` on the right half via a successor-index evaluation
              have happK : Fin.append left right (Fin.natAdd T k) = right k := by
                simpa using (Fin.append_right (u := left) (v := right) (i := k))
              -- switch to the `addNat` presentation used by the simplifier in this file
              have hnextAdd : (k.addNat T : Fin (T + T)) + 1 = (k + 1).addNat T := by
                -- rewrite both `natAdd` endpoints into `addNat`
                simpa [natAdd_eq_addNat (T := T) (k := k), natAdd_eq_addNat (T := T) (k := (k + 1))] using hnext
              have happK' : Fin.append left right (k.addNat T) = right k := by
                have : Fin.append left right (Fin.natAdd T k) = right k := by
                  simpa using (Fin.append_right (u := left) (v := right) (i := k))
                simpa [natAdd_eq_addNat (T := T) (k := k)] using this
              have happNext : Fin.append left right (k.addNat T + 1) = right (k + 1) := by
                have : Fin.append left right (Fin.natAdd T (k + 1)) = right (k + 1) := by
                  simpa using (Fin.append_right (u := left) (v := right) (i := (k + 1)))
                have : Fin.append left right ((k + 1).addNat T) = right (k + 1) := by
                  simpa [natAdd_eq_addNat (T := T) (k := (k + 1))] using this
                simpa [hnextAdd.symm] using this
              have hstep0 : OneBitDiff (Fin.append left right (k.addNat T)) (right (k + 1)) := by
                simpa [happK'] using hstep'
              simpa [happNext.symm] using hstep0
            · -- boundary: last element of right half wraps back to the first element of left half
              have hkval : k.val = T - 1 := by
                have hle : k.val + 1 ≤ T := Nat.succ_le_of_lt k.isLt
                have hge : T ≤ k.val + 1 := Nat.le_of_not_gt hk
                have : k.val + 1 = T := Nat.le_antisymm hle hge
                exact Nat.eq_sub_of_add_eq this
              have hnext : (Fin.natAdd T k : Fin (T + T)) + 1 = Fin.castAdd T 0 := by
                apply Fin.ext
                -- last element in `Fin (T+T)` wraps to `0`
                have hT1 : 1 ≤ T := Nat.succ_le_of_lt hTpos
                have hsum : k.val + T + 1 = T + T := by
                  calc
                    k.val + T + 1 = (T - 1) + T + 1 := by simp [hkval]
                    _ = (T - 1) + 1 + T := by
                        simp [Nat.add_assoc, Nat.add_left_comm, Nat.add_comm]
                    _ = T + T := by
                        simp [Nat.sub_add_cancel hT1, Nat.add_assoc]
                -- `((natAdd T k) + 1).val = ((k.val + T) + 1) % (T+T) = 0`
                -- (the RHS `castAdd T 0` has value 0)
                have : ((k.val + T + 1) % (T + T)) = 0 := by
                  simpa [hsum, Nat.mod_self]
                simpa [Fin.val_add] using this
              have hrev_last : Fin.rev k = (0 : Fin T) := by
                apply Fin.ext
                -- rev(last) has value 0
                have hT1 : 1 ≤ T := Nat.succ_le_of_lt hTpos
                have : (T - 1 + 1) = T := Nat.sub_add_cancel hT1
                simp [Fin.val_rev, hkval, this]
              have hstep' : OneBitDiff (right k) (left 0) := by
                -- last bit flips from `true` to `false`
                have hflip : OneBitDiff (snocBit (brgcPath (d + 1) 0) false) (snocBit (brgcPath (d + 1) 0) true) :=
                  oneBitDiff_snocBit_flip (p := brgcPath (d + 1) 0)
                have hflip' : OneBitDiff (snocBit (brgcPath (d + 1) 0) true) (snocBit (brgcPat

-- … truncated for the page; open the module for the rest.
THEOREM brgcPath_injective · brgcGrayCover · IndisputableMonolith/Patterns/GrayCycleBRGC.lean
brgcPath_injective · IndisputableMonolith/Patterns/GrayCycleBRGC.lean:72 
theorem brgcPath_injective : ∀ d : Nat, Function.Injective (brgcPath d)
  | 0 => by
      intro i j _
      -- `Fin 1` is a subsingleton (only `0`)
      simpa [Fin.eq_zero i, Fin.eq_zero j]
  | (d + 1) => by
      intro i j hij
      -- unfold the `d+1` definition and reduce to injectivity of the appended halves
      classical
      let T : Nat := 2 ^ d
      have hTT : 2 ^ (d + 1) = T + T := by
        simpa [T, twoPow_succ_eq_add d]
      let left : Fin T → Pattern (d + 1) := fun k => snocBit (brgcPath d k) false
      let right : Fin T → Pattern (d + 1) := fun k => snocBit (brgcPath d (Fin.rev k)) true
      have hij' :
          Fin.append left right (i.cast hTT) = Fin.append left right (j.cast hTT) := by
        simpa [brgcPath, T, hTT, left, right] using hij

      have hleft_inj : Function.Injective left := by
        intro a b hab
        have hab' : brgcPath d a = brgcPath d b := by
          funext k
          have := congrArg (fun p : Pattern (d + 1) => p k.castSucc) hab
          simpa [left, snocBit] using this
        exact (brgcPath_injective d) hab'

      have hright_inj : Function.Injective right := by
        intro a b hab
        have hab' : brgcPath d (Fin.rev a) = brgcPath d (Fin.rev b) := by
          funext k
          have := congrArg (fun p : Pattern (d + 1) => p k.castSucc) hab
          simpa [right, snocBit] using this
        have : Fin.rev a = Fin.rev b := (brgcPath_injective d) hab'
        exact Fin.rev_injective this

      have hdis : ∀ a b : Fin T, left a ≠ right b := by
        intro a b hab
        have := congrArg (fun p : Pattern (d + 1) => p (Fin.last d)) hab
        -- last coordinate is the appended bit: false on left, true on right
        simpa [left, right] using this

      have happ_inj : Function.Injective (Fin.append left right) :=
        (Fin.append_injective_iff (xs := left) (ys := right)).2 ⟨hleft_inj, hright_inj, hdis⟩

      have hcast : i.cast hTT = j.cast hTT := happ_inj hij'
      -- cast back along the inverse equality
      have := congrArg (Fin.cast hTT.symm) hcast
      simpa [hTT] using this
brgcGrayCover · IndisputableMonolith/Patterns/GrayCycleBRGC.lean:431 
noncomputable def brgcGrayCover (d : Nat) (hdpos : 0 < d) : GrayCover d (2 ^ d) :=
{ path := brgcPath d
  complete := by
    classical
    have h_inj : Function.Injective (brgcPath d) := brgcPath_injective d
    have h_card : Fintype.card (Fin (2 ^ d)) = Fintype.card (Pattern d) := by
      simp [Patterns.card_pattern]
    have h_bij : Function.Bijective (brgcPath d) :=
      (Fintype.bijective_iff_injective_and_card (brgcPath d)).2 ⟨h_inj, h_card⟩
    exact h_bij.2
  oneBit_step := brgc_oneBit_step (d := d) hdpos
}
THEOREM brgcPath · IndisputableMonolith/Patterns/GrayCycleBRGC.lean
brgcPath · IndisputableMonolith/Patterns/GrayCycleBRGC.lean:51 
/-- The recursive BRGC path as a `Fin (2^d) → Pattern d`. -/
def brgcPath : (d : Nat) → Fin (2 ^ d) → Pattern d
  | 0, _ =>
      -- unique 0-bit pattern
      fun _ => False
  | (d + 1), i =>
      let T : Nat := 2 ^ d
      let hTT : 2 ^ (d + 1) = T + T := by
        simpa [T, twoPow_succ_eq_add d]
      let i' : Fin (T + T) := i.cast hTT
      let left : Fin T → Pattern (d + 1) := fun k => snocBit (brgcPath d k) false
      let right : Fin T → Pattern (d + 1) := fun k => snocBit (brgcPath d (Fin.rev k)) true
      Fin.append left right i'

What this page does not claim

The theorem does not say the BRGC construction is the only Gray code. The theorem does not apply to dimension zero, where the single pattern has no neighbor. The theorem does not depend on the bitwise XOR formula for Gray codes.

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:

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND