Encyclopedia Patterns Patterns Gray Cycle Brgc

ARTICLE 3 claims 3 theorems

Patterns Gray Cycle Brgc

A Gray cycle is a loop through every binary pattern of a given length, changing exactly one bit per step; the BRGC construction builds one for any dimension without assuming any axioms.

Verify this page

Gray cycles by reflection

A Gray cycle is a closed loop that visits every binary pattern of a fixed length exactly once, with each step flipping exactly one bit. For two bits, the cycle 00, 01, 11, 10, back to 00 works: every two-bit pattern appears, and each move changes a single digit. The binary reflected Gray code (BRGC) is the classic recursive recipe for building such a cycle in any number of dimensions. It starts with the single pattern for zero bits, then at each stage copies the previous list, reverses the copy, and appends a new bit to each entry: a 0 for the original list and a 1 for the reversed one. This reflection trick, known since Frank Gray's 1953 patent, guarantees that consecutive patterns differ in one bit even across the wrap-around from last to first.

The BRGC has a well-known closed form: the code for a number n is n XOR (n shifted right by one). That formula is convenient, but it is not the definition. The recursive construction is the definition, and it works for any dimension d, producing a list of exactly 2^d patterns. For d = 3, the cycle runs 000, 001, 011, 010, 110, 111, 101, 100 and then back to 000. Each step flips one bit, and the final step from 100 to 000 also flips one bit, so the wrap-around condition holds. The same property holds for every positive dimension, which is what makes the BRGC a genuine cycle rather than merely a path.

In Recognition Science, the framework models patterns as functions from a finite set of coordinates to bits, and a Gray cycle is a path through all such patterns with one-bit adjacency. The framework's machine-checked library of formal theorems contains a module that builds the BRGC recursively and proves its two essential properties. The first proof shows the construction never repeats a pattern: the path is injective, so it visits 2^d distinct patterns. The second proof shows one-bit adjacency holds at every step, including the wrap-around, for every dimension d greater than zero. These two facts together mean the path is a genuine cycle that covers every pattern exactly once.

The module packages these results into two ready-made objects: a GrayCycle, which is the path with its injectivity and adjacency proofs, and a GrayCover, which adds the proof that the cycle covers every pattern. Both are built for any positive dimension without assuming any axioms beyond the standard logical ones, and without relying on the bitwise XOR formula. The construction is self-contained: it uses only the recursive definition and the framework's basic pattern vocabulary. What this establishes in plain language is that a Gray cycle exists in every dimension, and the recursive reflection recipe is enough to build it and certify its properties mechanically.

THEOREM brgcPath_injective · 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
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 brgcGrayCycle · brgcGrayCover · IndisputableMonolith/Patterns/GrayCycleBRGC.lean
brgcGrayCycle · IndisputableMonolith/Patterns/GrayCycleBRGC.lean:425 
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
}
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
}

What this page does not claim

The module does not use the bitwise formula gray(n) = n XOR (n >> 1) anywhere in its construction or proofs. The existence of Gray cycles in every dimension does not by itself force any physical constant or dimension count. The framework's library proves the BRGC properties, but it does not claim this construction is the only possible 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/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