grayCycle3
plain-language theorem explainer
The definition constructs an explicit Gray cycle on the 3-bit hypercube as an 8-phase path that visits each pattern once with single-bit flips between consecutive phases. Researchers formalizing the eight-tick octave in Recognition Science cite it to obtain a Hamiltonian cycle with one-bit adjacency. The definition packages a precomputed path, an injectivity proof, and a one-bit transition lemma into the required structure.
Claim. A Gray cycle for dimension 3 is an injective map $p : Fin 8 → (Fin 3 → Bool)$ such that for every phase $i$, the patterns $p(i)$ and $p(i+1)$ differ in exactly one coordinate.
background
The GrayCycle module upgrades cardinality facts on 3-bit patterns to an explicit adjacent cycle. Pattern d denotes maps from Fin d to Bool. OneBitDiff asserts that two patterns disagree in exactly one coordinate. The GrayCycle structure requires a path of length 2^d that is injective and satisfies the one-bit transition condition with wrap-around. This local setting uses the binary-reflected Gray code without external axioms, strengthening the surjection from the earlier period-exactly-8 result to a full Hamiltonian cycle.
proof idea
The definition is a record constructor that directly supplies the path from the composition of pattern3 with gray8At, the injectivity theorem that reduces via pattern3_injective and gray8At_injective, and the transition theorem proved by fin_cases on the eight steps.
why it matters
This supplies the concrete 8-tick cycle for dimension 3, matching the eight-tick octave and D=3 in the forcing chain. It provides the adjacency structure needed for ledger-compatible patterns. The module strengthens the coverage fact to a Hamiltonian cycle while remaining self-contained.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.