GrayCycle
GrayCycle d is a structure that packages an injective map from Fin(2^d) to the d-bit patterns together with the requirement that consecutive patterns (including wrap-around) differ in exactly one coordinate. Recognition Science modelers cite it to upgrade pure cardinality coverage to explicit Hamiltonian adjacency on the hypercube. The declaration is a direct structure definition with three fields and no separate proof body.
claimA Gray cycle of dimension $d$ is a map $p : {0,1,2,…,2^d-1} → ({0,1}^d)$ that is injective and satisfies that $p(i)$ and $p(i+1)$ differ in exactly one coordinate for every $i$ (indices mod $2^d$).
background
Pattern d denotes the set of all functions Fin d → Bool, i.e., the vertices of the d-dimensional hypercube. OneBitDiff p q is the predicate asserting that p and q differ in exactly one coordinate (unique k : Fin d with p k ≠ q k). The module works in the setting of Hamiltonian cycles on this hypercube: a closed walk of length exactly 2^d that visits every pattern once and moves only to an adjacent vertex at each step.
proof idea
This is a structure definition (def_or_abbrev) with an empty proof body. It simply assembles the three fields path, inj, and oneBit_step into a single named object; no lemmas are applied inside the declaration itself.
why it matters in Recognition Science
GrayCycle supplies the parent type for grayCycle3 (the explicit 3-bit eight-tick cycle) and for the BRGC constructions brgcGrayCycle in both GrayCycleBRGC and GrayCycleGeneral. It closes the gap between the surjection proved in Patterns.period_exactly_8 and the one-bit adjacency needed for the T7 eight-tick octave and ledger-compatible adjacency in the Recognition Science forcing chain.
scope and limits
- Does not construct any concrete path for arbitrary d.
- Does not prove existence of a GrayCycle for any d.
- Does not impose additional metric or cost structure beyond one-bit adjacency.
- Does not depend on external Gray-code axioms from GrayCodeAxioms.lean.
Lean usage
def grayCycle3 : GrayCycle 3 := { path := grayCycle3Path, inj := grayCycle3_injective, oneBit_step := grayCycle3_oneBit_step }formal statement (Lean)
53structure GrayCycle (d : Nat) where
54 /-- Phase-indexed path through patterns (period is fixed to `2^d`). -/
55 path : Fin (2 ^ d) → Pattern d
56 /-- No repeats (Hamiltonian cycle candidate). -/
57 inj : Function.Injective path
58 /-- Consecutive phases differ in exactly one bit (with wrap-around). -/
59 oneBit_step : ∀ i : Fin (2 ^ d), OneBitDiff (path i) (path (i + 1))
60
61/-- A Gray *cover* with an arbitrary period `T`: adjacency (one-bit steps) plus coverage (surjection). -/