GrayCycle
plain-language theorem explainer
GrayCycle d is the structure for a Hamiltonian cycle on the d-dimensional hypercube whose vertices are all maps Fin d to Bool. Workers on Recognition Science patterns cite it to enforce one-bit adjacency with wrap-around closure on the 2^d states. The declaration is a plain structure with three fields: the path map, its injectivity, and the OneBitDiff predicate on consecutive steps.
Claim. A Gray cycle of dimension $d$ is an injective map $p : {0,1,2,…,2^d-1} → {0,1}^d$ such that $p(i)$ and $p(i+1)$ differ in exactly one coordinate for every $i$ (indices mod $2^d$), where two maps differ in one coordinate when there exists a unique $k ∈ {0,…,d-1}$ with $p(i)(k) ≠ p(i+1)(k)$.
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 Hamming distance exactly one: there exists a unique coordinate k where the two patterns disagree. The module upgrades the earlier cardinality and coverage results (such as the surjection Fin 8 → Pattern 3) to require explicit one-bit adjacency and closure. This supplies the stronger object needed for ledger-compatible adjacency in the Recognition Science setting.
proof idea
The declaration is a structure definition. It introduces the three fields path, inj and oneBit_step directly; the predicate OneBitDiff is taken from the sibling definition in the same module. No lemmas or tactics are invoked inside the structure itself.
why it matters
GrayCycle supplies the adjacency data consumed by downstream objects grayCycle3 (the explicit 8-tick cycle) and brgcGrayCycle (the binary-reflected Gray-code realization). It closes the gap between mere coverage of Pattern 3 and a closed one-bit walk, supporting the eight-tick octave (T7) and D = 3 in the forcing chain. The module states that this adjacency notion is required beyond the counting facts already present in Patterns.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.