T7_nyquist_obstruction

formal source

  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
  95
  96 theorem T6_exist_8 : ∃ w : CompleteCover 3, w.period = 8 :=
  97  period_exactly_8
  98
  99/-‑ ## Minimal counting facts and eight‑tick lower bound -/