Encyclopedia Patterns Patterns Gray Cycle
ARTICLE 4 claims 3 theorems 1 model
Patterns Gray Cycle
The gray cycle is the formal one-bit adjacency structure that turns the eight-pattern counting bound into a closed Hamiltonian cycle on the three-bit cube.
Gray cycle and the eight-tick adjacency
In Recognition Science, a gray cycle is a closed walk through all patterns of a given bit length such that consecutive patterns differ in exactly one coordinate, with the last and first patterns also differing in one coordinate. Patterns here are functions from a finite set of coordinates to booleans, so a three-bit pattern is a triple of bits. The gray cycle is the stronger object needed to align the ledger-compatible adjacency story with a formal definition: the earlier counting fact only certified that eight patterns cover the three-bit space, not that they can be visited one bit at a time.
The module establishes, with no axioms beyond the standard recursive binary reflected Gray code construction, that a gray cycle exists for three-bit patterns with period exactly eight. The explicit witness is the canonical order [0,1,3,2,6,7,5,4], encoded as a path through the eight patterns. The proof shows the path is injective, hence visits every pattern exactly once, and that each consecutive pair, including the wrap-around pair, differs in exactly one bit. This is a fully decidable, brute-force-checked construction; it does not rely on the Gray-code axioms in the legacy module.
The consequence for Recognition Science is that the eight-tick cycle, which the forcing chain derives as the recognition cycle, carries the required one-bit adjacency structure, not merely a coverage fact. The module also proves a minimality theorem: any gray cover of all d-bit patterns needs at least 2^d ticks, and for d=3 that lower bound is exactly eight. Thus the gray cycle is not an extra assumption; it is the unique minimal adjacency-compatible way to traverse the three-bit state space.
MODEL GrayCycle · IndisputableMonolith/Patterns/GrayCycle.lean
structure GrayCycle (d : Nat) where
/-- Phase-indexed path through patterns (period is fixed to `2^d`). -/
path : Fin (2 ^ d) → Pattern d
/-- No repeats (Hamiltonian cycle candidate). -/
inj : Function.Injective path
/-- Consecutive phases differ in exactly one bit (with wrap-around). -/
oneBit_step : ∀ i : Fin (2 ^ d), OneBitDiff (path i) (path (i + 1))
THEOREM grayCycle3 · grayCycle3_period · IndisputableMonolith/Patterns/GrayCycle.lean
/-- 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
}
theorem grayCycle3_period : (2 ^ 3) = 8 := by decide
THEOREM grayCycle3_injective · grayCycle3_oneBit_step · IndisputableMonolith/Patterns/GrayCycle.lean
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_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 ⊢
THEOREM grayCover_min_ticks · grayCover_eight_tick_min · IndisputableMonolith/Patterns/GrayCycle.lean
/-- 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
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)
What this page does not claim
Not a derivation of the eight-tick cycle from the cost function; the gray cycle is a formal structure, not a physical forcing result. Not a claim that the gray cycle is the only possible adjacency structure for three bits. Not a proof that the physical recognition-to-linking bridge uses the gray cycle; that bridge remains open.
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:
- How does the gray cycle on three bits relate to the eight-tick recognition cycle derived from the forcing chain?
- What physical interpretation does the one-bit adjacency structure carry in the ledger model?
- Does a gray cycle exist for all dimensions d, and is the recursive construction the unique minimal one?
- How does the gray cycle's injectivity interact with the ledger's requirement of no repeated recognition events?
MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND
- MODELA gray cycle is a closed walk through all patterns of a given bit length such that consecutive patterns differ in exactly one coordinate, with the last and first patterns also differing in one coordinate. GrayCycle · IndisputableMonolith/Patterns/GrayCycle.lean
- THEOREMThe module establishes, with no axioms beyond the standard recursive binary reflected Gray code construction, that a gray cycle exists for three-bit patterns with period exactly eight. grayCycle3 · grayCycle3_period · IndisputableMonolith/Patterns/GrayCycle.lean
- THEOREMThe proof shows the path is injective, hence visits every pattern exactly once, and that each consecutive pair, including the wrap-around pair, differs in exactly one bit. grayCycle3_injective · grayCycle3_oneBit_step · IndisputableMonolith/Patterns/GrayCycle.lean
- THEOREMThe module also proves a minimality theorem: any gray cover of all d-bit patterns needs at least 2^d ticks, and for d=3 that lower bound is exactly eight. grayCover_min_ticks · grayCover_eight_tick_min · IndisputableMonolith/Patterns/GrayCycle.lean