gray8At
plain-language theorem explainer
This definition supplies the canonical 3-bit Gray code ordering as a map from Fin 8 to Fin 8 with the explicit sequence 0,1,3,2,6,7,5,4. Pattern theorists formalizing Hamiltonian cycles on hypercubes cite it to ground the one-bit adjacency structure for three-dimensional state spaces in Recognition Science. The definition is realized by direct case analysis on each of the eight possible inputs.
Claim. The function $g : {0,1,2,3,4,5,6,7} → {0,1,2,3,4,5,6,7}$ is given by the assignments $g(0)=0$, $g(1)=1$, $g(2)=3$, $g(3)=2$, $g(4)=6$, $g(5)=7$, $g(6)=5$, $g(7)=4$. This encodes the standard binary-reflected Gray code order on three bits.
background
In the GrayCycle module the state space consists of patterns, defined as functions from Fin d to Bool. Two patterns are adjacent when they differ in exactly one coordinate. A cycle is a closed walk of length 2^d that visits every pattern once, i.e., a Hamiltonian cycle on the d-dimensional hypercube graph. For d=3 the space has cardinality 8, matching the eight-tick octave of the forcing chain. The module upgrades earlier cardinality results from Patterns to this adjacency-preserving notion and uses the standard binary-reflected Gray code construction rather than external axioms. The upstream period definition from PulsarEmissionRegimesFromRS sets period(k) = phi^k and supplies the scaling context for the period-8 object, although the map itself is independent of that definition.
proof idea
The definition is given by exhaustive pattern matching on the eight constructors of Fin 8. Each case returns the corresponding index in the Gray sequence with no auxiliary lemmas or computation steps.
why it matters
It is the base map for grayCycle3Path, which composes with pattern3 to produce the explicit cycle on Pattern 3, and thereby supports the downstream injectivity and one-bit-step theorems. In the Recognition Science framework this supplies the concrete Hamiltonian cycle for the 3-bit hypercube, aligning with the T7 eight-tick octave and the ledger-compatible adjacency requirement. It closes the gap between mere surjection onto patterns and an explicit adjacent path without invoking Gray-code axioms.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.