grayCycle3Path
grayCycle3Path supplies the explicit mapping from the 8-cycle index to 3-bit patterns by composing the canonical Gray ordering with the bit-pattern decoder. Researchers formalizing the 8-tick octave or hypercube coverings in Recognition Science cite it to anchor the adjacent cycle structure. The definition is realized as the direct composition fun i => pattern3 (gray8At i).
claimDefine the path function $p : {0,1,2,3,4,5,6,7} / 8Z → (Fin 3 → Bool)$ by $p(i) := pattern3(gray8At(i))$, where gray8At enumerates the binary-reflected Gray code order on three bits and pattern3 decodes each codeword to its coordinate vector.
background
The module upgrades cardinality facts about 3-bit patterns to an explicit Hamiltonian cycle on the hypercube. Here Pattern 3 denotes the set of functions Fin 3 → Bool, with adjacency when two patterns differ in exactly one coordinate. The upstream gray8At supplies the canonical ordering [0,1,3,2,6,7,5,4] as a map Fin 8 → Fin 8, while pattern3 converts each integer codeword into the corresponding 3-bit vector by testing individual bits.
proof idea
This is a one-line wrapper that applies pattern3 to the output of gray8At at each index i.
why it matters in Recognition Science
grayCycle3Path provides the path component for the GrayCycle 3 and GrayCover 3 structures. It realizes the period-8 cycle that aligns with the eight-tick octave and D = 3 spatial dimensions in the Recognition Science forcing chain.
scope and limits
- Does not verify one-bit adjacency between consecutive images.
- Does not prove surjectivity onto all 3-bit patterns.
- Does not generalize the construction to dimensions other than 3.
Lean usage
def grayCycle3 : GrayCycle 3 := { path := grayCycle3Path, inj := grayCycle3_injective, oneBit_step := grayCycle3_oneBit_step }formal statement (Lean)
106def grayCycle3Path : Fin 8 → Pattern 3 :=
proof body
Definition body.
107 fun i => pattern3 (gray8At i)
108