Patterns Gray Cycle Gray Cycle3 Bijective

The eight-step cycle

A Gray code is a sequence of binary strings in which every adjacent pair differs in exactly one bit. For three bits there are eight possible strings, and the classic reflected Gray code orders them as 000, 001, 011, 010, 110, 111, 101, 100. The property that matters here is that the sequence is a Hamiltonian cycle: it visits all eight strings exactly once and the last string differs from the first in one bit, so the list wraps around into a loop. This is a standard object in digital circuit design, where it prevents glitches when a counter advances through states that differ by a single bit.

The framework's library of machine-checked formal theorems contains a declaration, grayCycle3_bijective, which proves that this eight-step sequence is a bijection: it pairs each of the eight positions in the cycle with a distinct three-bit string, covering all of them. The proof is fully explicit, built from a concrete list of eight codewords, and it is checked by the computer to be correct. The declaration also establishes the two components of bijectivity separately: the sequence is injective, meaning no string repeats, and surjective, meaning every three-bit string appears. Together these facts certify that the cycle is Hamiltonian, not merely a path that might skip or repeat entries.

In Recognition Science, this result matters because the framework models a recognition cycle as a discrete ledger, a record of events, where each step changes one bit of a three-bit pattern. The theorem shows that an eight-tick cycle can cover all eight patterns with exactly the adjacency the framework requires. It is a structural guarantee: the eight-tick counting bound, which earlier work established by a counting argument, is here upgraded to a full adjacency-compatible cycle. The framework proves that such a cycle exists, not that it is the only one, and the result is specific to three bits.

The declaration does not claim that the Gray cycle is unique, nor that it extends to any number of bits. It also does not assert anything about why eight ticks are physically required; that is a separate question about the framework's forcing chain. What the theorem does give is a rigorous, machine-checked existence proof for the canonical three-bit Gray cycle, which the framework can then use as a concrete witness for its eight-tick structure.

theorem grayCycle3_bijective : Function.Bijective grayCycle3Path := by
  classical
  -- card(Fin 8) = 8
  have hFin : Fintype.card (Fin 8) = 8 := by simp
  -- card(Pattern 3) = 2^3 = 8
  have hPat' : Fintype.card (Pattern 3) = 2 ^ 3 := by
    simpa using (Patterns.card_pattern 3)
  have hPow : (2 ^ 3 : Nat) = 8 := by decide
  have hPat : Fintype.card (Pattern 3) = 8 := by simpa [hPow] using hPat'
  have hcard : Fintype.card (Fin 8) = Fintype.card (Pattern 3) := by
    -- rewrite both sides to 8
    calc
      Fintype.card (Fin 8) = 8 := hFin
      _ = Fintype.card (Pattern 3) := by simpa [hPat]
  -- injective + card equality ⇒ bijective
  exact (Fintype.bijective_iff_injective_and_card grayCycle3Path).2 ⟨grayCycle3_injective, hcard⟩

theorem grayCycle3_injective : Function.Injective grayCycle3Path := by
  intro i j hij
  have h0 : gray8At i = gray8At j := pattern3_injective (by simpa [grayCycle3Path] using hij)
  exact gray8At_injective h0

theorem grayCycle3_surjective : Function.Surjective grayCycle3Path :=
  (grayCycle3_bijective).2

/-- 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 declaration does not claim the Gray cycle is unique. It does not claim the result extends to any number of bits beyond three. It does not claim anything about why eight ticks are physically required.

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: