GrayCycle
plain-language theorem explainer
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.
Claim. A 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.