Patterns Gray Cycle Gray Cover Eight Tick Min

The eight-tick minimum

A Gray code, named for Frank Gray who patented it in 1953, lists binary strings so that consecutive entries differ in exactly one bit. The classic example for three bits runs 000, 001, 011, 010, 110, 111, 101, 100. This ordering matters in rotary encoders and error correction, where a single-bit change prevents a mistransition from being read as a wildly wrong value.

The theorem grayCover_eight_tick_min proves a lower bound: any sequence of three-bit patterns in which consecutive entries differ by one bit, and which visits every one of the eight possible patterns, must contain at least eight entries. The proof is a short argument from a more general result, grayCover_min_ticks, which states that covering all d-bit patterns requires at least 2^d steps. For three bits, 2^3 = 8, so the bound is exactly eight. The declaration is a theorem in a machine-checked library of formal theorems, meaning the proof has been verified step by step by a computer.

In Recognition Science, the framework models a ledger, a discrete record of events, as a sequence of such patterns. The framework's library uses this eight-step minimum to support a claim about a recognition cycle: the smallest number of distinct states needed to distinguish all eight patterns is eight. The theorem itself, however, is purely combinatorial. It says nothing about physics, time, or the meaning of the patterns. It establishes a counting fact about binary strings.

The explicit witness grayCycle3 shows the bound is attainable: the standard three-bit Gray code achieves exactly eight steps and visits every pattern. This closes the question: eight is both necessary and sufficient. The theorem does not claim that any particular physical process must follow this sequence, nor that the eight-step cycle has a unique form. It proves a minimum, not a prescription.

theorem grayCover_eight_tick_min {T : Nat} [NeZero T] (w : GrayCover 3 T) : 8 ≤ T := by
  simpa using (Patterns.eight_tick_min (T := T) w.path w.complete)

/-- A Gray *cover* with an arbitrary period `T`: adjacency (one-bit steps) plus coverage (surjection). -/
structure GrayCover (d T : Nat) [NeZero T] where
  path : Fin T → Pattern d
  complete : Function.Surjective path
  oneBit_step : ∀ i : Fin T, OneBitDiff (path i) (path (i + 1))

/-! Minimality: any cover of all `d`-bit patterns needs at least `2^d` ticks. -/
theorem grayCover_min_ticks {d T : Nat} [NeZero T] (w : GrayCover d T) : 2 ^ d ≤ T :=
  Patterns.min_ticks_cover (d := d) (T := T) w.path w.complete

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

This theorem does not claim any physical process must follow the Gray code sequence. It does not claim the eight-step cycle is the only possible one. It does not derive the fine-structure constant or any coupling constant.

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: