eight_tick_min

formal source

  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. -/
  64lemma eight_tick_min {T : Nat}
  65  (pass : Fin T → Pattern 3) (covers : Function.Surjective pass) : 8 ≤ T := by
  66  simpa using (min_ticks_cover (d := 3) (T := T) pass covers)
  67
  68/-- Nyquist-style obstruction: if T < 2^D, no surjection to D-bit patterns. -/
  69theorem T7_nyquist_obstruction {T D : Nat}
  70  (hT : T < 2 ^ D) : ¬ ∃ f : Fin T → Pattern D, Function.Surjective f :=
  71  no_surj_small T D hT
  72
  73/-- At threshold T=2^D there is a bijection (no aliasing). -/
  74theorem T7_threshold_bijection (D : Nat) : ∃ f : Fin (2 ^ D) → Pattern D, Function.Bijective f := by
  75  classical
  76  let e := (Fintype.equivFin (Pattern D))
  77  have hcard : Fintype.card (Pattern D) = 2 ^ D := by exact card_pattern D
  78  -- Manual cast equivalence between Fin (2^D) and Fin (Fintype.card (Pattern D))
  79  let castTo : Fin (2 ^ D) → Fin (Fintype.card (Pattern D)) :=
  80    fun i => ⟨i.1, by
  81      -- rewrite the goal via hcard and close with i.2
  82      have : i.1 < 2 ^ D := i.2
  83      simp [this]⟩
  84  let castFrom : Fin (Fintype.card (Pattern D)) → Fin (2 ^ D) :=
  85    fun j => ⟨j.1, by simpa [hcard] using j.2⟩
  86  have hLeft : Function.LeftInverse castFrom castTo := by intro i; cases i; rfl
  87  have hRight : Function.RightInverse castFrom castTo := by intro j; cases j; rfl
  88  have hCastBij : Function.Bijective castTo := ⟨hLeft.injective, hRight.surjective⟩
  89  refine ⟨fun i => (e.symm) (castTo i), ?_⟩
  90  exact (e.symm).bijective.comp hCastBij
  91
  92/-‑ ## T6 alias theorems -/
  93 theorem T6_exist_exact_2pow (d : Nat) : ∃ w : CompleteCover d, w.period = 2 ^ d :=
  94  cover_exact_pow d