grayCover_min_ticks
plain-language theorem explainer
Any Gray cover of the d-dimensional hypercube patterns requires at least 2^d ticks in its period. Researchers formalizing minimal adjacent traversals of the state space would cite this bound when tightening coverage arguments to one-bit steps. The proof is a one-line wrapper that feeds the path and surjectivity fields of the GrayCover structure directly into the general min_ticks_cover lemma.
Claim. Let $w$ be a Gray cover of dimension $d$ with period $T$, i.e., a surjective map from the cyclic interval of length $T$ onto the set of all $d$-bit patterns such that consecutive patterns differ in exactly one coordinate. Then $2^d ≤ T$.
background
Pattern d denotes the set of functions Fin d → Bool, i.e., the vertices of the d-dimensional hypercube. OneBitDiff p q holds precisely when p and q differ in exactly one coordinate, the standard Hamming-distance-1 adjacency. GrayCover d T packages a path Fin T → Pattern d that is surjective (complete) together with the oneBit_step condition enforcing adjacency at every step. The module upgrades plain coverage facts to this adjacent setting to match ledger-compatible traversal requirements. The key upstream result is the lemma min_ticks_cover, which states that any surjective map from Fin T to Pattern d satisfies 2^d ≤ T; it is proved by contradiction via the auxiliary no_surj_small predicate.
proof idea
One-line wrapper that applies Patterns.min_ticks_cover to the path and complete fields of the supplied GrayCover structure, discarding the oneBit_step field because the lower bound depends only on surjectivity.
why it matters
This bound closes the minimal-period claim for adjacent covers inside the GrayCycle module, which exists to strengthen the 2^D counting facts (T8) with explicit one-bit adjacency. It sits downstream of the general coverage lemma and supports later constructions such as grayCycle3Path and gray8At that target the eight-tick octave for D = 3. No downstream uses are recorded yet, leaving open whether the bound will be invoked inside larger cycle-existence arguments.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.