grayCover_eight_tick_min
plain-language theorem explainer
Any Gray cover of the 3-bit patterns with period T must satisfy T at least 8. Researchers modeling the Recognition Science octave would cite this to bound the shortest adjacent traversal of the 3-cube. The proof is a one-line term wrapper that extracts the path and surjectivity fields from the GrayCover and invokes the general eight_tick_min lemma.
Claim. Let $w$ be a Gray cover of the 3-bit patterns with period $T > 0$. Then $8 ≤ T$.
background
A GrayCover for dimension d and period T is a structure containing a path from Fin T to Pattern d (maps from Fin d to Bool), a surjectivity proof that the path hits every pattern, and a one-bit step condition ensuring consecutive patterns differ in exactly one coordinate. This upgrades the earlier cardinality coverage to an adjacent walk on the hypercube. The module works in the setting of explicit Hamiltonian cycles on the 3-cube without external Gray-code axioms, using the standard recursive construction. Upstream, the Constants.octave definition sets one octave to 8 ticks, and the general Patterns.eight_tick_min lemma supplies the minimality fact specialized here to d=3.
proof idea
The proof is a one-line term wrapper. It passes the path and complete fields of the input GrayCover w directly to Patterns.eight_tick_min (with T fixed), then applies simpa to obtain the inequality 8 ≤ T.
why it matters
This pins the minimal period for any adjacent 3-bit cover at exactly the eight-tick octave (T7 in the forcing chain). It supplies the rigorous lower bound needed to align the pattern module with the Recognition Science claim that the fundamental evolution period is 2^3 ticks. The result closes the minimality gap for the explicit 3-bit witness described in the module, even though no downstream uses are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.