Patterns Gray Cycle

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

THEOREM grayCycle3 · grayCycle3_period · IndisputableMonolith/Patterns/GrayCycle.lean

THEOREM grayCycle3_injective · grayCycle3_oneBit_step · IndisputableMonolith/Patterns/GrayCycle.lean

THEOREM grayCover_min_ticks · grayCover_eight_tick_min · IndisputableMonolith/Patterns/GrayCycle.lean

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: