Patterns Gray Cycle Gray Cycle3 One Bit Step

The one-bit step

A Gray code is a sequence of binary strings in which consecutive entries differ by exactly one bit. The most familiar example is the 3-bit Gray code: 000, 001, 011, 010, 110, 111, 101, 100. Each transition flips a single 0 to a 1 or a 1 to a 0, and the sequence wraps around, so the last entry 100 also differs from the first entry 000 in exactly one bit. This wrap-around property makes the list a cycle rather than a simple path. The code was introduced by Frank Gray at Bell Labs in 1947 as a way to reduce errors in pulse-code modulation, and it remains a standard tool in digital electronics and error correction.

Within the Recognition Science framework, this classical object takes on a specific role. The framework models recognition, a discrete record of events, as a sequence of states that change one bit at a time. The declaration grayCycle3_oneBit_step is a machine-checked proof that the 3-bit Gray code listed above satisfies this one-bit-change condition at every step, including the wrap-around step from the last entry back to the first. The proof is part of the framework's machine-checked library of formal theorems, and it establishes that the 8-step cycle is a genuine Gray cycle, not merely a list of all 8 patterns in some arbitrary order.

The declaration does not claim that the 3-bit Gray cycle is unique, nor that it is the only way to traverse all 8 three-bit patterns with one-bit steps. Other Gray codes exist for three bits, such as 000, 010, 011, 001, 101, 111, 110, 100, which also satisfies the one-bit-change condition. The proof also does not claim that the Gray cycle has any physical meaning or that the framework's recognition process must follow this particular sequence. It is a combinatorial existence proof: among all possible orderings of the 8 patterns, at least one ordering with the one-bit-step property exists, and the library exhibits it explicitly.

What the declaration contributes to the framework is a precise, checkable instance of the "one-bit" adjacency that the framework's broader narrative invokes. Earlier results in the library established that 8 patterns can cover the 3-bit space, but did not enforce that consecutive states differ by one bit. The Gray cycle closes that gap by providing a concrete, verified cycle with the stronger adjacency property. This matters because the framework's account of recognition as a discrete process depends on the idea that state changes are minimal, and the Gray cycle is the standard combinatorial witness that such minimal changes can form a closed loop over all 3-bit states.

theorem grayCycle3_oneBit_step : ∀ i : Fin 8, OneBitDiff (grayCycle3Path i) (grayCycle3Path (i + 1)) := by
  intro i
  -- 8 explicit cases; each step flips exactly one of the three bits.
  fin_cases i
  · -- 0 -> 1 (flip bit 0)
    refine ⟨⟨0, by decide⟩, ?_, ?_⟩
    · simp [grayCycle3Path, gray8At, pattern3]
    · intro k hk
      fin_cases k <;> simp [grayCycle3Path, gray8At, pattern3] at hk ⊢
  · -- 1 -> 3 (flip bit 1)
    refine ⟨⟨1, by decide⟩, ?_, ?_⟩
    · simp [grayCycle3Path, gray8At, pattern3]
    · intro k hk
      fin_cases k <;> simp [grayCycle3Path, gray8At, pattern3] at hk ⊢
  · -- 2 -> 3?  (i=2 means gray8At 2 = 3, next is gray8At 3 = 2; flip bit 0)
    refine ⟨⟨0, by decide⟩, ?_, ?_⟩
    · simp [grayCycle3Path, gray8At, pattern3]
    · intro k hk
      fin_cases k <;> simp [grayCycle3Path, gray8At, pattern3] at hk ⊢
  · -- i=3: 2 -> 6 (flip bit 2)
    refine ⟨⟨2, by decide⟩, ?_, ?_⟩
    · simp [grayCycle3Path, gray8At, pattern3]
    · intro k hk
      fin_cases k <;> simp [grayCycle3Path, gray8At, pattern3] at hk ⊢
  · -- i=4: 6 -> 7 (flip bit 0)
    refine ⟨⟨0, by decide⟩, ?_, ?_⟩
    · simp [grayCycle3Path, gray8At, pattern3]
    · intro k hk
      fin_cases k <;> simp [grayCycle3Path, gray8At, pattern3] at hk ⊢
  · -- i=5: 7 -> 5 (flip bit 1)
    refine ⟨⟨1, by decide⟩, ?_, ?_⟩
    · simp [grayCycle3Path, gray8At, pattern3]
    · intro k hk
      fin_cases k <;> simp [grayCycle3Path, gray8At, pattern3] at hk ⊢
  · -- i=6: 5 -> 4 (flip bit 0)
    refine ⟨⟨0, by decide⟩, ?_, ?_⟩
    · simp [grayCycle3Path, gray8At, pattern3]
    · intro k hk
      fin_cases k <;> simp [grayCycle3Path, gray8At, pattern3] at hk ⊢
  · -- i=7: 4 -> 0 (wrap; flip bit 2)
    refine ⟨⟨2, by decide⟩, ?_, ?_⟩
    · simp [grayCycle3Path, gray8At, pattern3]
    · intro k hk
      fin_cases k <;> simp [grayCycle3Path, gray8At, pattern3] at hk ⊢

/-- A rigorous Gray cycle for 3-bit patterns (the “8-tick” cycle). -/
def grayCycle3 : GrayCycle 3 :=
{ path := grayCycle3Path
, inj := grayCycle3_injective
, oneBit_step := grayCycle3_oneBit_step
}

What this page does not claim

The 3-bit Gray cycle is the unique ordering of 8 patterns with one-bit steps. The Gray cycle has any physical or empirical content within the framework. The framework's recognition process must follow this particular Gray code sequence.

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/GrayCycle.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: