Encyclopedia Patterns Patterns Gray Cycle General Exists Gray Cycle Of Le64

ARTICLE 3 claims 3 theorems

Patterns Gray Cycle General Exists Gray Cycle Of Le64

A machine-checked theorem guarantees that any dimension up to 64 admits a Gray cycle, a path through all binary patterns that changes one bit at a time.

Verify this page

A bounded Gray cycle

A Gray cycle is a circular ordering of all binary strings of a fixed length, say d bits, such that consecutive strings differ in exactly one bit position. The classic example is the reflected binary code, often called the binary reflected Gray code, where the string at position n is computed as n XOR (n shifted right by one). This construction dates to Frank Gray's 1953 patent and remains a standard tool in digital encoders and error correction.

The theorem exists_grayCycle_of_le64 states that for any positive dimension d no larger than 64, such a cycle exists, and its path is exactly the binary reflected Gray code. The proof is machine-checked: a computer program verified every step of the argument, from the injectivity of the encoding to the one-bit adjacency of each step, including the wrap-around from the last string back to the first. The result is packaged as a formal object that carries the path, the injectivity proof, and the adjacency proof together.

The bound of 64 is not an accident of the mathematics; it is a convenience of the implementation. The construction routes the successor adjacency and the inverse through a set of axioms about 64-bit arithmetic, so the packaged object requires the dimension to fit in that width. A separate theorem in the same file, exists_grayCycle, removes the bound entirely by delegating to a recursive construction that works for every positive dimension with no axioms at all. The bounded version is therefore the practical one for concrete computation, while the unbounded version is the general mathematical statement.

In Recognition Science, the framework that develops this library, Gray cycles serve as a discrete record of events, a ledger in which adjacent entries differ minimally. The theorem does not claim that Gray cycles are unique, that the binary reflected code is the only one-bit-adjacent ordering, or that the result extends beyond 64 bits in this particular packaged form. It establishes existence for the stated range, nothing more and nothing less.

THEOREM exists_grayCycle_of_le64 · IndisputableMonolith/Patterns/GrayCycleGeneral.lean
exists_grayCycle_of_le64 · IndisputableMonolith/Patterns/GrayCycleGeneral.lean:327 
theorem exists_grayCycle_of_le64 {d : Nat} (hdpos : 0 < d) (hd : d ≤ 64) :
    ∃ w : GrayCycle d, w.path = brgcPath d :=
  ⟨brgcGrayCycle d hdpos hd, rfl⟩
THEOREM brgcPath_injective · brgc_oneBit_step · brgc_wrap_oneBitDiff · IndisputableMonolith/Patterns/GrayCycleGeneral.lean
brgcPath_injective · IndisputableMonolith/Patterns/GrayCycleGeneral.lean:204 
theorem brgcPath_injective {d : Nat} (hdpos : 0 < d) (hd : d ≤ 64) : Function.Injective (brgcPath d) := by
  intro i j hij
  -- reduce to equality of the Nat Gray codes, then invert using `GrayCodeFacts.grayToNat_inverts_natToGray`.
  have hbits : ∀ k : Nat, (natToGray i.val).testBit k = (natToGray j.val).testBit k := by
    intro k
    by_cases hk : k < d
    · have := congrArg (fun p : Pattern d => p ⟨k, hk⟩) hij
      simpa [brgcPath, binaryReflectedGray, natToGray] using this
    · have hkge : d ≤ k := le_of_not_gt hk
      have hi0 : (natToGray i.val).testBit k = false :=
        natToGray_testBit_false_of_ge (d := d) (n := i.val) (k := k) i.isLt hkge
      have hj0 : (natToGray j.val).testBit k = false :=
        natToGray_testBit_false_of_ge (d := d) (n := j.val) (k := k) j.isLt hkge
      simp [hi0, hj0]
  have hgray : natToGray i.val = natToGray j.val := by
    exact Nat.eq_of_testBit_eq hbits
  -- show both indices are < 2^64
  have hpow : 2 ^ d ≤ 2 ^ 64 := Nat.pow_le_pow_right (by decide : 0 < (2 : Nat)) hd
  have hi64 : i.val < 2 ^ 64 := lt_of_lt_of_le i.isLt hpow
  have hj64 : j.val < 2 ^ 64 := lt_of_lt_of_le j.isLt hpow
  have hi_inv : GrayCodeAxioms.grayInverse (natToGray i.val) = i.val :=
    GrayCodeFacts.grayToNat_inverts_natToGray (n := i.val) hi64
  have hj_inv : GrayCodeAxioms.grayInverse (natToGray j.val) = j.val :=
    GrayCodeFacts.grayToNat_inverts_natToGray (n := j.val) hj64
  have : i.val = j.val := by
    have := congrArg GrayCodeAxioms.grayInverse hgray
    simpa [hi_inv, hj_inv] using this
  exact Fin.ext this
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)
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 exists_grayCycle · IndisputableMonolith/Patterns/GrayCycleGeneral.lean
exists_grayCycle · IndisputableMonolith/Patterns/GrayCycleGeneral.lean:316 
/-- **THEOREM (GENERAL)**: There exists a Gray cycle for any dimension `d > 0`.

    This theorem provides the unconditional existence witness by delegating to
    the recursive BRGC construction in `GrayCycleBRGC.lean`. -/
theorem exists_grayCycle {d : Nat} (hdpos : 0 < d) : ∃ w : GrayCycle d, w.path 0 = GrayCycleBRGC.brgcPath d 0 :=
  ⟨GrayCycleBRGC.brgcGrayCycle d hdpos, rfl⟩

What this page does not claim

The theorem does not claim that Gray cycles are unique or that the binary reflected code is the only one-bit-adjacent ordering. The theorem does not claim the result extends beyond 64 bits in this packaged form. The theorem does not claim any physical significance for Gray cycles in the framework.

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