min_ticks_cover
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.
claimIf $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 in Recognition Science
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.
scope and limits
- Does not construct an explicit minimal covering sequence.
- Does not address non-surjective mappings or partial covers.
- Does not incorporate adjacency constraints such as one-bit flips.
- Does not extend the bound to infinite or continuous pattern spaces.
Lean usage
lemma eight_tick_min {T : Nat} (pass : Fin T → Pattern 3) (covers : Function.Surjective pass) : 8 ≤ T := by simpa using (min_ticks_cover (d := 3) (T := T) pass covers)formal statement (Lean)
57lemma min_ticks_cover {d T : Nat}
58 (pass : Fin T → Pattern d) (covers : Function.Surjective pass) : 2 ^ d ≤ T := by
proof body
Term-mode proof.
59 classical
60 by_contra h
61 exact (no_surj_small T d (lt_of_not_ge h)) ⟨pass, covers⟩
62
63/-- For 3-bit patterns, any complete pass has length at least 8. -/