T7_threshold_bijection

formal source

  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 -/
 100
 101/-- For any dimension `d`, the exact cover of period `2^d` has positive period. -/
 102 theorem T6_exist_exact_pos (d : Nat) : ∃ w : CompleteCover d, 0 < w.period := by
 103  obtain ⟨w, hp⟩ := cover_exact_pow d
 104  have : 0 < (2 : ℕ) ^ d := by