Encyclopedia Patterns Patterns Gray Cycle General

ARTICLE 4 claims 4 theorems

Patterns Gray Cycle General

A Gray code is a way to list binary strings so each step changes only one bit; Recognition Science proves such a list exists in every dimension.

Verify this page

Gray cycles in any dimension

A Gray code is a sequence of binary strings in which every consecutive pair differs by exactly one bit. The classic example for three bits is 000, 001, 011, 010, 110, 111, 101, 100. Such sequences matter in engineering and mathematics because a single-bit change avoids the ambiguity that occurs when several bits flip at once. A Gray cycle adds the requirement that the last string also differs from the first by one bit, closing the list into a loop. The standard construction, the binary reflected Gray code, uses the formula gray(n) = n XOR (n >>> 1), where >>> is a right shift. This formula defines a path through all 2^d strings of length d.

The Recognition Science framework models patterns as binary strings and asks whether a Gray cycle can be built in any dimension d. The answer is yes. First, for any dimension d with 0 < d ≤ 64, the binary reflected formula produces a path that is injective (never repeats a string) and one-bit adjacent at every step, including the wrap from the last string back to the first. These two properties are what make the path a genuine Gray cycle. The proofs of injectivity and one-bit adjacency are carried out directly in the machine-checked library of formal theorems, with no extra assumptions beyond the bound on d.

The bound is then removed. A separate recursive construction, using append and rev, builds a Gray path for any positive dimension d with no size limit and no axioms. The theorem exists_grayCycle states that for every d > 0, there exists a Gray cycle whose path starts at the all-zero string. A companion theorem exists_grayCover states the same for a Gray cover, which is a surjective path with one-bit steps that visits every string. These are unconditional existence results: they hold for every positive dimension, not just small ones.

In plain language, the one-bit-change property is not a special feature of low dimensions. Whether d is 3 or 1000, a closed loop exists that visits every binary string exactly once, changing a single bit at each step. This matters for the framework because recognition events, modeled as patterns, can be ordered in a way that makes successive states minimally different. The existence of such an ordering in every dimension is a structural fact the framework can rely on when it reasons about sequences of recognition events.

THEOREM brgcPath · IndisputableMonolith/Patterns/GrayCycleGeneral.lean
brgcPath · IndisputableMonolith/Patterns/GrayCycleGeneral.lean:42 
/-- The BRGC path as a `Fin (2^d) → Pattern d`. -/
def brgcPath (d : Nat) : Fin (2 ^ d) → Pattern d :=
  fun i => binaryReflectedGray d i
THEOREM brgcPath_injective · brgc_oneBit_step · 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)
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⟩
THEOREM exists_grayCover · IndisputableMonolith/Patterns/GrayCycleGeneral.lean
exists_grayCover · IndisputableMonolith/Patterns/GrayCycleGeneral.lean:323 
/-- **THEOREM (GENERAL)**: There exists a Gray cover for any dimension `d > 0`. -/
theorem exists_grayCover {d : Nat} (hdpos : 0 < d) : ∃ w : GrayCover d (2 ^ d), w.path 0 = GrayCycleBRGC.brgcPath d 0 :=
  ⟨GrayCycleBRGC.brgcGrayCover d hdpos, rfl⟩

What this page does not claim

This answer does not claim the Gray cycle construction is unique or canonical. This answer does not claim the framework derives the physical dimension of space from Gray cycles. This answer does not claim the module proves anything about the cost function or the golden ratio.

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