grayCycle3_oneBit_step
plain-language theorem explainer
The theorem shows that consecutive states in the explicit 3-bit Gray cycle path differ by exactly one bit flip. Workers on discrete evolution rules or hypercube Hamiltonians in Recognition Science cite it to certify adjacency for the 8-tick cycle. The proof runs exhaustive case analysis over the eight indices, using fin_cases and simplification against the path definition to locate the single differing coordinate in each transition.
Claim. For every index $i$ in the set of eight elements, the 3-bit pattern at position $i$ and the pattern at position $i+1$ (modulo 8) differ in exactly one coordinate.
background
Pattern $d$ denotes the set of functions from Fin $d$ to Bool, i.e., the $2^d$ possible bit strings of length $d$. OneBitDiff $p$ $q$ holds precisely when there exists a unique coordinate $k$ such that $p(k) ≠ q(k)$, the formal statement of Hamming distance one. The module upgrades earlier cardinality results on 3-bit patterns to an explicit cycle whose successive states obey this adjacency. Upstream results supply the fundamental tick (one octave equals eight ticks) and the local rule application from cellular automata, both of which presuppose single-coordinate updates.
proof idea
The proof introduces the index $i$ and applies fin_cases to split into eight exhaustive subgoals. Each subgoal refines a witness for the unique differing bit together with two subgoals: one that the chosen bit actually flips under the explicit grayCycle3Path definition, and one that no other bit differs. Both subgoals are discharged by simp against grayCycle3Path, gray8At and pattern3.
why it matters
This adjacency lemma is the final ingredient that lets grayCycle3 and grayCover3 be assembled as a GrayCycle and a GrayCover of period 8. It therefore supplies the concrete Hamiltonian cycle on the 3-dimensional hypercube required by the eight-tick octave (T7) in the forcing chain. The construction remains internal to the Patterns module and does not yet link to the J-cost or phi-ladder mass formulas.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.