Patterns Gray Cycle General Exists Gray Cover Of Le64

The bounded Gray cover

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 runs 000, 001, 011, 010, 110, 111, 101, 100, and wraps around so the last entry also differs from the first by one bit. These sequences appear in rotary encoders, error correction, and puzzle design because a single-bit change avoids ambiguous transitions between states.

The binary reflected Gray code (BRGC) is the standard construction: for a number n, its Gray code is n XOR (n shifted right by one). This formula produces a path through all 2^d strings of length d. The framework's machine-checked library of formal theorems proves that this path is injective, meaning it visits every string exactly once, and that each step, including the wrap-around step, changes exactly one bit.

In Recognition Science, the declaration exists_grayCover_of_le64 establishes a bounded existence result. For any dimension d greater than zero and at most 64, the theorem proves there is a Gray cover: a sequence of all 2^d patterns where each step flips one bit and the final entry connects back to the first. The proof routes the bitwise arithmetic through a set of axioms about Gray codes, which is why the result carries the d ≤ 64 bound.

The framework also provides an unconditional version. A separate theorem, exists_grayCover, proves the same existence for every positive dimension d with no bound and no extra axioms, using a recursive construction that appends and reverses paths. The bounded result is therefore a convenience for working with fixed-width machine words, not the strongest statement the library offers.

What the bounded theorem does not claim is that 64 is a natural limit. The bound is an artifact of the proof method, which relies on 64-bit arithmetic facts. For any d, the unconditional theorem already supplies the Gray cover; the bounded version simply packages the same idea for the common case of machine-sized dimensions.

theorem exists_grayCover_of_le64 {d : Nat} (hdpos : 0 < d) (hd : d ≤ 64) :
    ∃ w : GrayCover d (2 ^ d), w.path = brgcPath d :=
  ⟨brgcGrayCover d hdpos hd, rfl⟩

/-- **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

The bound d ≤ 64 is a proof artifact, not a claim that Gray covers fail for larger dimensions. The theorem does not construct a Gray cover that is unique or canonical in any framework-specific sense.

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: