min_ticks_cover
plain-language theorem explainer
Any surjective mapping from a set of T elements onto all d-bit patterns requires T at least 2^d. Pattern theorists and engineers designing minimal sampling periods cite this cardinality bound. The argument proceeds by contradiction, feeding the assumed surjection into the upstream no-surjection lemma after negating the size inequality.
Claim. If $f :$ Fin $T$ $→$ (Fin $d$ $→$ Bool) is surjective, then $T ≥ 2^d$.
background
Pattern d is the set of all binary strings of length d, defined as the functions from Fin d to Bool. The lemma supplies a lower bound on the length T of any complete covering sequence of these patterns. It lives in the Patterns module, which develops minimal covering sequences and Gray-cycle constructions. The proof depends on the upstream no_surj_small lemma, which asserts that no surjection from Fin T to Pattern d exists whenever T < 2^d.
proof idea
The proof is a one-line wrapper that applies no_surj_small after a contradiction assumption. Classical logic negates the target inequality to obtain T < 2^d, then packages the given surjective pass as a witness and hands it directly to the upstream lemma.
why it matters
This bound feeds the eight_tick_min specialization for d = 3 and the grayCover_min_ticks theorem for Gray covers. It instantiates the eight-tick octave (period 2^3) from the T7 step of the forcing chain and supplies the basic counting obstruction for D = 3 spatial dimensions. The result closes a foundational cardinality argument used throughout the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.