eight_tick_min
plain-language theorem explainer
Any surjective assignment of T steps to the 3-bit boolean patterns must use at least 8 steps. Researchers working on minimal recognition cycles or octave periods in forcing chains cite this bound to anchor period-8 results. The proof is a direct specialization of the general min_ticks_cover lemma to dimension 3.
Claim. Let $P$ denote the set of all maps from a 3-element index set to the booleans. For any natural number $T$ and any surjective function $f$ from a $T$-element index set to $P$, one has $T ≥ 8$.
background
Pattern d is the type of d-bit patterns, defined as maps from Fin d to Bool. The sibling lemma min_ticks_cover supplies the general lower bound: any surjective pass of length T over d-bit patterns satisfies 2^d ≤ T. The present declaration instantiates that bound at d = 3, where 2^3 = 8. Upstream results include the definition of T as a natural-number period in Breath1024 and the triangular-number T in Gap45, both supplying the ambient counting framework for discrete recognition steps.
proof idea
One-line wrapper that applies min_ticks_cover with the explicit instantiation d := 3, reducing the target inequality 8 ≤ T to the already-proved general statement 2^d ≤ T.
why it matters
The lemma supplies the concrete numerical anchor for the eight-tick octave (T7) in the forcing chain. It is invoked directly by eight_tick_uniqueness to conclude that every recognition loop on a simplicial manifold has length at least 8, and by octavePeriod_eq_eight and octavePeriod_is_minimal_cover to certify that the octave period equals the minimal cover size. The same bound appears in volcanic-forcing certificates and eight-tick Navier-Stokes dynamics.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.