grayCycle3Path
plain-language theorem explainer
grayCycle3Path supplies the explicit function realizing the 3-bit Gray cycle path of period 8 by mapping each index through the canonical Gray ordering and then decoding to a 3-bit pattern. Workers on hypercube Hamiltonian cycles or Recognition Science ledger adjacency would reference this path when constructing GrayCycle 3. The definition proceeds by direct composition of the ordering map with the pattern decoder.
Claim. Let $g : [0..7] → [0..7]$ be the canonical 3-bit Gray ordering with values $[0,1,3,2,6,7,5,4]$. Let $p : [0..7] → {0,1}^3$ decode an integer to its 3-bit pattern via bit tests. The path is the composite $p ∘ g$.
background
In the GrayCycle module the state space consists of all functions from a d-element set to Bool, i.e., the vertices of the d-dimensional hypercube. Two patterns are adjacent when they differ in exactly one coordinate. A Gray cycle is a Hamiltonian cycle: a closed walk of length 2^d visiting each vertex once. The module upgrades the earlier cardinality result (a surjection Fin 8 → Pattern 3) to an explicit adjacent cycle. This construction relies on the canonical Gray ordering that enumerates 0 through 7 in the sequence 0,1,3,2,6,7,5,4 and on the decoder that converts each integer into the corresponding 3-bit pattern by testing individual bits.
proof idea
The definition is a one-line composition that applies the pattern decoder to the value of the Gray ordering at each index.
why it matters
This path is the core object from which GrayCycle 3 and GrayCover 3 are assembled by adjoining the injectivity, surjectivity, and one-bit step theorems. It supplies the explicit 8-tick cycle required to align the Recognition Science counting bound with the ledger-compatible adjacency condition. The construction sits inside the eight-tick octave (T7) of the forcing chain and furnishes the concrete representative for D = 3.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.