Encyclopedia Patterns Patterns Gray Cycle General Brgc Wrap One Bit Diff

ARTICLE 4 claims 4 theorems

Patterns Gray Cycle General Brgc Wrap One Bit Diff

A Gray code lists binary patterns so consecutive entries differ in one bit; the wrap-around step closes the list into a cycle.

Verify this page

The wrap-around step

A Gray code is a way of listing binary strings so that each step changes exactly one bit. The reflected binary Gray code, named after Frank Gray's 1953 patent, orders the 2^d strings of length d by the formula gray(n) = n XOR (n >>> 1). This ordering has a practical virtue: a mechanical encoder reading consecutive positions never sees two bits change at once, which avoids ambiguous readings at boundaries.

The standard construction starts at the all-zero string and visits every other string once. The question is whether the final string can return to the start in one step, closing the list into a cycle. For the reflected code, the last string is 1000...0 in most dimensions, which differs from 0000...0 in one bit, so the wrap works. The declaration brgc_wrap_oneBitDiff proves this formally: for any positive dimension d, the last entry of the reflected path differs from the first entry in exactly one bit.

The proof is axiom-free, meaning it relies only on the definitions of the bit operations and natural number arithmetic. It does not require the dimension to be bounded; it holds for every d greater than zero. The same file also proves that each consecutive pair in the path differs in one bit, but that result carries the extra assumption d ≤ 64 because it routes through a bitwise library. The wrap-around step alone needs no such bound.

In Recognition Science, the framework models recognition events as discrete patterns and uses Gray cycles to represent a complete traversal of possible states with minimal change between steps. The wrap-around theorem is the piece that turns a path into a cycle, allowing the traversal to repeat indefinitely. This matters for the framework's eight-tick recognition cycle, where the final state must connect back to the first to sustain repetition. The theorem guarantees that the reflected binary Gray code provides such a closed loop in any dimension.

The declaration does not claim that the reflected code is the only Gray code, nor that it is optimal for any particular purpose. It does not establish that the full cycle exists for dimensions above 64 using the bounded construction; that requires the separate recursive construction in GrayCycleBRGC.lean, which is axiom-free for all d. The wrap-around proof is a local fact about the last and first entries, not a statement about the entire cycle's existence.

THEOREM brgc_wrap_oneBitDiff · IndisputableMonolith/Patterns/GrayCycleGeneral.lean
brgc_wrap_oneBitDiff · IndisputableMonolith/Patterns/GrayCycleGeneral.lean:110 
theorem brgc_wrap_oneBitDiff {d : Nat} (hdpos : 0 < d) :
    OneBitDiff (brgcPath d ⟨2 ^ d - 1, by
      exact Nat.sub_lt (pow_pos (by decide : 0 < (2 : Nat)) d) (by decide)⟩) (brgcPath d 0) := by
  classical
  rcases Nat.exists_eq_succ_of_ne_zero (Nat.ne_of_gt hdpos) with ⟨t, rfl⟩
  -- d = t+1, unique differing bit is the last one (value t)
  let iLast : Fin (2 ^ (t + 1)) :=
    ⟨2 ^ (t + 1) - 1, by
      exact Nat.sub_lt (pow_pos (by decide : 0 < (2 : Nat)) (t + 1)) (by decide)⟩
  have hw : OneBitDiff (brgcPath (t + 1) iLast) (brgcPath (t + 1) 0) := by
    refine ⟨Fin.last t, ?_, ?_⟩
    · -- show the last bit differs (it is true at iLast, false at 0)
      have ht_true : (natToGray iLast.val).testBit t = true := by
        -- compute `natToGray (allOnes (t+1))` at bit t: true XOR false = true
        have hn : iLast.val = allOnes (t + 1) := rfl
        have hshift : (iLast.val >>> 1) = allOnes t := by
          -- `allOnes (t+1) = bit true (allOnes t)` ⇒ shiftRight 1 yields `allOnes t`
          have hrepr : allOnes (t + 1) = Nat.bit true (allOnes t) := allOnes_succ_eq_bit t
          -- use `bit_shiftRight_one`
          have : (Nat.bit true (allOnes t) >>> 1) = allOnes t := Nat.bit_shiftRight_one true (allOnes t)
          simpa [hn, hrepr] using this
        -- now compute testBit of xor
        -- n.testBit t = true (all ones), (n>>>1).testBit t = false
        have hnbit : (iLast.val).testBit t = true := by
          -- t < t+1
          have : t < t + 1 := Nat.lt_succ_self t
          simpa [hn, allOnes] using allOnes_testBit_lt (t := t + 1) (k := t) this
        have hmbit : (iLast.val >>> 1).testBit t = false := by
          -- iLast>>>1 = allOnes t, and that has bit t = false
          simpa [hshift] using allOnes_testBit_eq_false_at t
        -- combine via xor
        simp [natToGray, hnbit, hmbit]
      -- translate to the Pattern statement
      have : brgcPath (t + 1) iLast (Fin.last t) ≠ brgcPath (t + 1) 0 (Fin.last t) := by
        -- right side is false, left side is true
        have h0 : brgcPath (t + 1) 0 (Fin.last t) = false := by
          simp [brgcPath, binaryReflectedGray, natToGray]
        have h1 : brgcPath (t + 1) iLast (Fin.last t) = true := by
          simpa [brgcPath, binaryReflectedGray] using ht_true
        simpa [h0, h1]
      simpa using this
    · intro j hj
      -- any differing index must be the last one (all other bits are equal/false)
      induction j using Fin.lastCases with
      | last => rfl
      | cast j =>
          -- show contradiction: at castSucc j, both patterns are false
          have hjlt : (j.val : Nat) < t := j.isLt
          -- compute natToGray at bit j.val: true XOR true = false (since both allOnes have ones there)
          have hfalse : brgcPath (t + 1) iLast j.castSucc = false := by
            -- n = allOnes(t+1), m = n>>>1 = allOnes t
            have hn : iLast.val = allOnes (t + 1) := rfl
            have hnbit : (iLast.val).testBit j.val = true := by
              have : j.val < t + 1 := Nat.lt_succ_of_lt hjlt
              simpa [hn, allOnes] using allOnes_testBit_lt (t := t + 1) (k := j.val) this
            have hshift : (iLast.val >>> 1) = allOnes t := by
              have hrepr : allOnes (t + 1) = Nat.bit true (allOnes t) := allOnes_succ_eq_bit t
              have : (Nat.bit true (allOnes t) >>> 1) = allOnes t := Nat.bit_shiftRight_one true (allOnes t)
              simpa [hn, hrepr] using this
            have hmbit : (iLast.val >>> 1).testBit j.val = true := by
              simpa [hshift, allOnes] using allOnes_testBit_lt (t := t) (k := j.val) hjlt
            have : (natToGray iLast.val).testBit j.val = false := by
              simp [natToGray, hnbit, hmbit]
            simpa [brgcPath, binaryReflectedGray] using this
          have h0 : brgcPath (t + 1) 0 j.castSucc = false := by
            simp [brgcPath, binaryReflectedGray, natToGray]
          have : False := by
            -- hj says they differ, but both patterns are false
            simpa [hfalse, h0] using hj
          exact this.elim
  simpa [iLast] using hw
THEOREM brgc_wrap_oneBitDiff · IndisputableMonolith/Patterns/GrayCycleGeneral.lean
brgc_wrap_oneBitDiff · IndisputableMonolith/Patterns/GrayCycleGeneral.lean:110 
theorem brgc_wrap_oneBitDiff {d : Nat} (hdpos : 0 < d) :
    OneBitDiff (brgcPath d ⟨2 ^ d - 1, by
      exact Nat.sub_lt (pow_pos (by decide : 0 < (2 : Nat)) d) (by decide)⟩) (brgcPath d 0) := by
  classical
  rcases Nat.exists_eq_succ_of_ne_zero (Nat.ne_of_gt hdpos) with ⟨t, rfl⟩
  -- d = t+1, unique differing bit is the last one (value t)
  let iLast : Fin (2 ^ (t + 1)) :=
    ⟨2 ^ (t + 1) - 1, by
      exact Nat.sub_lt (pow_pos (by decide : 0 < (2 : Nat)) (t + 1)) (by decide)⟩
  have hw : OneBitDiff (brgcPath (t + 1) iLast) (brgcPath (t + 1) 0) := by
    refine ⟨Fin.last t, ?_, ?_⟩
    · -- show the last bit differs (it is true at iLast, false at 0)
      have ht_true : (natToGray iLast.val).testBit t = true := by
        -- compute `natToGray (allOnes (t+1))` at bit t: true XOR false = true
        have hn : iLast.val = allOnes (t + 1) := rfl
        have hshift : (iLast.val >>> 1) = allOnes t := by
          -- `allOnes (t+1) = bit true (allOnes t)` ⇒ shiftRight 1 yields `allOnes t`
          have hrepr : allOnes (t + 1) = Nat.bit true (allOnes t) := allOnes_succ_eq_bit t
          -- use `bit_shiftRight_one`
          have : (Nat.bit true (allOnes t) >>> 1) = allOnes t := Nat.bit_shiftRight_one true (allOnes t)
          simpa [hn, hrepr] using this
        -- now compute testBit of xor
        -- n.testBit t = true (all ones), (n>>>1).testBit t = false
        have hnbit : (iLast.val).testBit t = true := by
          -- t < t+1
          have : t < t + 1 := Nat.lt_succ_self t
          simpa [hn, allOnes] using allOnes_testBit_lt (t := t + 1) (k := t) this
        have hmbit : (iLast.val >>> 1).testBit t = false := by
          -- iLast>>>1 = allOnes t, and that has bit t = false
          simpa [hshift] using allOnes_testBit_eq_false_at t
        -- combine via xor
        simp [natToGray, hnbit, hmbit]
      -- translate to the Pattern statement
      have : brgcPath (t + 1) iLast (Fin.last t) ≠ brgcPath (t + 1) 0 (Fin.last t) := by
        -- right side is false, left side is true
        have h0 : brgcPath (t + 1) 0 (Fin.last t) = false := by
          simp [brgcPath, binaryReflectedGray, natToGray]
        have h1 : brgcPath (t + 1) iLast (Fin.last t) = true := by
          simpa [brgcPath, binaryReflectedGray] using ht_true
        simpa [h0, h1]
      simpa using this
    · intro j hj
      -- any differing index must be the last one (all other bits are equal/false)
      induction j using Fin.lastCases with
      | last => rfl
      | cast j =>
          -- show contradiction: at castSucc j, both patterns are false
          have hjlt : (j.val : Nat) < t := j.isLt
          -- compute natToGray at bit j.val: true XOR true = false (since both allOnes have ones there)
          have hfalse : brgcPath (t + 1) iLast j.castSucc = false := by
            -- n = allOnes(t+1), m = n>>>1 = allOnes t
            have hn : iLast.val = allOnes (t + 1) := rfl
            have hnbit : (iLast.val).testBit j.val = true := by
              have : j.val < t + 1 := Nat.lt_succ_of_lt hjlt
              simpa [hn, allOnes] using allOnes_testBit_lt (t := t + 1) (k := j.val) this
            have hshift : (iLast.val >>> 1) = allOnes t := by
              have hrepr : allOnes (t + 1) = Nat.bit true (allOnes t) := allOnes_succ_eq_bit t
              have : (Nat.bit true (allOnes t) >>> 1) = allOnes t := Nat.bit_shiftRight_one true (allOnes t)
              simpa [hn, hrepr] using this
            have hmbit : (iLast.val >>> 1).testBit j.val = true := by
              simpa [hshift, allOnes] using allOnes_testBit_lt (t := t) (k := j.val) hjlt
            have : (natToGray iLast.val).testBit j.val = false := by
              simp [natToGray, hnbit, hmbit]
            simpa [brgcPath, binaryReflectedGray] using this
          have h0 : brgcPath (t + 1) 0 j.castSucc = false := by
            simp [brgcPath, binaryReflectedGray, natToGray]
          have : False := by
            -- hj says they differ, but both patterns are false
            simpa [hfalse, h0] using hj
          exact this.elim
  simpa [iLast] using hw
THEOREM brgc_wrap_oneBitDiff · IndisputableMonolith/Patterns/GrayCycleGeneral.lean
brgc_wrap_oneBitDiff · IndisputableMonolith/Patterns/GrayCycleGeneral.lean:110 
theorem brgc_wrap_oneBitDiff {d : Nat} (hdpos : 0 < d) :
    OneBitDiff (brgcPath d ⟨2 ^ d - 1, by
      exact Nat.sub_lt (pow_pos (by decide : 0 < (2 : Nat)) d) (by decide)⟩) (brgcPath d 0) := by
  classical
  rcases Nat.exists_eq_succ_of_ne_zero (Nat.ne_of_gt hdpos) with ⟨t, rfl⟩
  -- d = t+1, unique differing bit is the last one (value t)
  let iLast : Fin (2 ^ (t + 1)) :=
    ⟨2 ^ (t + 1) - 1, by
      exact Nat.sub_lt (pow_pos (by decide : 0 < (2 : Nat)) (t + 1)) (by decide)⟩
  have hw : OneBitDiff (brgcPath (t + 1) iLast) (brgcPath (t + 1) 0) := by
    refine ⟨Fin.last t, ?_, ?_⟩
    · -- show the last bit differs (it is true at iLast, false at 0)
      have ht_true : (natToGray iLast.val).testBit t = true := by
        -- compute `natToGray (allOnes (t+1))` at bit t: true XOR false = true
        have hn : iLast.val = allOnes (t + 1) := rfl
        have hshift : (iLast.val >>> 1) = allOnes t := by
          -- `allOnes (t+1) = bit true (allOnes t)` ⇒ shiftRight 1 yields `allOnes t`
          have hrepr : allOnes (t + 1) = Nat.bit true (allOnes t) := allOnes_succ_eq_bit t
          -- use `bit_shiftRight_one`
          have : (Nat.bit true (allOnes t) >>> 1) = allOnes t := Nat.bit_shiftRight_one true (allOnes t)
          simpa [hn, hrepr] using this
        -- now compute testBit of xor
        -- n.testBit t = true (all ones), (n>>>1).testBit t = false
        have hnbit : (iLast.val).testBit t = true := by
          -- t < t+1
          have : t < t + 1 := Nat.lt_succ_self t
          simpa [hn, allOnes] using allOnes_testBit_lt (t := t + 1) (k := t) this
        have hmbit : (iLast.val >>> 1).testBit t = false := by
          -- iLast>>>1 = allOnes t, and that has bit t = false
          simpa [hshift] using allOnes_testBit_eq_false_at t
        -- combine via xor
        simp [natToGray, hnbit, hmbit]
      -- translate to the Pattern statement
      have : brgcPath (t + 1) iLast (Fin.last t) ≠ brgcPath (t + 1) 0 (Fin.last t) := by
        -- right side is false, left side is true
        have h0 : brgcPath (t + 1) 0 (Fin.last t) = false := by
          simp [brgcPath, binaryReflectedGray, natToGray]
        have h1 : brgcPath (t + 1) iLast (Fin.last t) = true := by
          simpa [brgcPath, binaryReflectedGray] using ht_true
        simpa [h0, h1]
      simpa using this
    · intro j hj
      -- any differing index must be the last one (all other bits are equal/false)
      induction j using Fin.lastCases with
      | last => rfl
      | cast j =>
          -- show contradiction: at castSucc j, both patterns are false
          have hjlt : (j.val : Nat) < t := j.isLt
          -- compute natToGray at bit j.val: true XOR true = false (since both allOnes have ones there)
          have hfalse : brgcPath (t + 1) iLast j.castSucc = false := by
            -- n = allOnes(t+1), m = n>>>1 = allOnes t
            have hn : iLast.val = allOnes (t + 1) := rfl
            have hnbit : (iLast.val).testBit j.val = true := by
              have : j.val < t + 1 := Nat.lt_succ_of_lt hjlt
              simpa [hn, allOnes] using allOnes_testBit_lt (t := t + 1) (k := j.val) this
            have hshift : (iLast.val >>> 1) = allOnes t := by
              have hrepr : allOnes (t + 1) = Nat.bit true (allOnes t) := allOnes_succ_eq_bit t
              have : (Nat.bit true (allOnes t) >>> 1) = allOnes t := Nat.bit_shiftRight_one true (allOnes t)
              simpa [hn, hrepr] using this
            have hmbit : (iLast.val >>> 1).testBit j.val = true := by
              simpa [hshift, allOnes] using allOnes_testBit_lt (t := t) (k := j.val) hjlt
            have : (natToGray iLast.val).testBit j.val = false := by
              simp [natToGray, hnbit, hmbit]
            simpa [brgcPath, binaryReflectedGray] using this
          have h0 : brgcPath (t + 1) 0 j.castSucc = false := by
            simp [brgcPath, binaryReflectedGray, natToGray]
          have : False := by
            -- hj says they differ, but both patterns are false
            simpa [hfalse, h0] using hj
          exact this.elim
  simpa [iLast] using hw
THEOREM brgc_oneBit_step · IndisputableMonolith/Patterns/GrayCycleGeneral.lean
brgc_oneBit_step · IndisputableMonolith/Patterns/GrayCycleGeneral.lean:233 
lemma brgc_oneBit_step {d : Nat} (hdpos : 0 < d) (hd : d ≤ 64) :
    ∀ i : Fin (2 ^ d), OneBitDiff (brgcPath d i) (brgcPath d (i + 1)) := by
  intro i
  classical
  -- split on whether `i.val + 1 < 2^d` (no wrap) or wrap case
  by_cases hstep : i.val + 1 < 2 ^ d
  · -- Use the Gray-code one-bit property at the Nat level.
    rcases GrayCodeAxioms.gray_code_one_bit_property (d := d) (n := i.val) hstep with
      ⟨k, hk, hkuniq⟩
    have hklt : k < d := hk.1
    let kk : Fin d := ⟨k, hklt⟩
    refine ⟨kk, ?diff, ?uniq⟩
    · -- Show the bit differs at coordinate kk.
      haveI : NeZero (2 ^ d) := ⟨pow_ne_zero d (by decide : (2 : Nat) ≠ 0)⟩
      have hval : (i + 1).val = i.val + 1 :=
        Fin.val_add_one_of_lt' (n := 2 ^ d) (i := i) hstep
      dsimp [brgcPath, binaryReflectedGray, natToGray, kk]
      simpa [hval] using hk.2
    · intro j hj
      -- Uniqueness: any differing coordinate must be kk.
      haveI : NeZero (2 ^ d) := ⟨pow_ne_zero d (by decide : (2 : Nat) ≠ 0)⟩
      have hval : (i + 1).val = i.val + 1 :=
        Fin.val_add_one_of_lt' (n := 2 ^ d) (i := i) hstep
      have hjnat :
          ((i.val ^^^ (i.val >>> 1)).testBit j.val) ≠
            (((i.val + 1) ^^^ ((i.val + 1) >>> 1)).testBit j.val) := by
        dsimp [brgcPath, binaryReflectedGray, natToGray] at hj
        simpa [hval] using hj
      have : (j.val : Nat) = k := by
        exact hkuniq j.val ⟨j.isLt, hjnat⟩
      apply Fin.ext
      simpa [kk] using this
  · -- Wrap case: i is the last index and (i+1)=0 in `Fin (2^d)`.
    -- In the wrap branch, `i` must be the last element: `i.val = 2^d - 1`.
    have hi_eq : i.val = 2 ^ d - 1 := by
      have hle : i.val ≤ 2 ^ d - 1 := Nat.le_pred_of_lt i.isLt
      have hge : 2 ^ d - 1 ≤ i.val := by
        -- not (i+1 < 2^d) ⇒ 2^d ≤ i+1 ⇒ 2^d - 1 ≤ i
        have : 2 ^ d ≤ i.val + 1 := Nat.le_of_not_gt hstep
        have hpos : 0 < 2 ^ d := pow_pos (by decide : 0 < (2 : Nat)) d
        have : Nat.succ (2 ^ d - 1) ≤ Nat.succ i.val := by
          simpa [Nat.succ_eq_add_one, Nat.succ_pred_eq_of_pos hpos] using this
        exact Nat.succ_le_succ_iff.mp this
      exact Nat.le_antisymm hle hge
    let iLast : Fin (2 ^ d) :=
      ⟨2 ^ d - 1, by
        exact Nat.sub_lt (pow_pos (by decide : 0 < (2 : Nat)) d) (by decide)⟩
    have hi_def : i = iLast := by
      apply Fin.ext
      simp [iLast, hi_eq]
    have hsucc0_last : iLast + 1 = 0 := by
      apply Fin.ext
      -- compute val_add modulo 2^d at the last index
      have hle : 1 ≤ 2 ^ d := Nat.one_le_pow d 2 (by decide : 0 < (2 : Nat))
      -- (2^d - 1 + 1) % 2^d = 0
      simp [Fin.val_add, iLast, Nat.sub_add_cancel hle]
    -- reduce to the wrap-around axiom statement (last index → 0)
    simpa [hi_def, hsucc0_last] using (brgc_wrap_oneBitDiff (d := d) hdpos)

What this page does not claim

The reflected binary Gray code is the only Gray code for a given dimension. The bounded construction provides a full cycle for dimensions above 64. The wrap-around theorem alone establishes the existence of a complete Gray cycle.

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/GrayCycleGeneral.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