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. -/
used by (2)
From the project-wide theorem graph. These declarations reference this one in their body.