IndisputableMonolith.Patterns

   1import Mathlib
   2
   3namespace IndisputableMonolith
   4namespace Patterns
   5
   6open Classical
   7open Function
   8
   9@[simp] def Pattern (d : Nat) := (Fin d → Bool)
  10
  11instance instFintypePattern (d : Nat) : Fintype (Pattern d) := by
  12  dsimp [Pattern]
  13  infer_instance
  14
  15structure CompleteCover (d : Nat) where
  16  period : ℕ
  17  path   : Fin period → Pattern d
  18  complete : Function.Surjective path
  19
  20/-- There exists a complete cover of exact length `2^d` for d‑dimensional patterns. -/
  21theorem cover_exact_pow (d : Nat) : ∃ w : CompleteCover d, w.period = 2 ^ d := by
  22  classical
  23  let e := (Fintype.equivFin (Pattern d)).symm
  24  refine ⟨{ period := Fintype.card (Pattern d)
  25          , path := fun i => e i
  26          , complete := (Fintype.equivFin (Pattern d)).symm.surjective }, ?_⟩
  27  have : Fintype.card (Pattern d) = 2 ^ d := by
  28    simp [Pattern, Fintype.card_bool, Fintype.card_fin]
  29  exact this
  30
  31/-- There exists an 8‑tick complete cover for 3‑bit patterns. -/
  32 theorem period_exactly_8 : ∃ w : CompleteCover 3, w.period = 8 := by
  33  simpa using cover_exact_pow 3
  34
  35/-- Cardinality of the pattern space. -/
  36lemma card_pattern (d : Nat) : Fintype.card (Pattern d) = 2 ^ d := by
  37  classical
  38  simp [Pattern, Fintype.card_fin] at*
  39
  40/-- No surjection to all d-bit patterns if T < 2^d. -/
  41lemma no_surj_small (T d : Nat) (hT : T < 2 ^ d) :
  42  ¬ ∃ f : Fin T → Pattern d, Function.Surjective f := by
  43  classical
  44  intro h; rcases h with ⟨f, hf⟩
  45  obtain ⟨g, hg⟩ := hf.hasRightInverse
  46  have hginj : Injective g := by
  47    intro y₁ y₂ hgy
  48    have : f (g y₁) = f (g y₂) := by simp [hgy]
  49    simpa [RightInverse, hg y₁, hg y₂] using this
  50  have hcard : Fintype.card (Pattern d) ≤ Fintype.card (Fin T) :=
  51    Fintype.card_le_of_injective _ hginj
  52  have : 2 ^ d ≤ T := by
  53    simpa [Fintype.card_fin, card_pattern d] using hcard
  54  exact (lt_of_le_of_lt this hT).false
  55
  56/-- Minimal ticks lower bound for a complete cover. -/
  57lemma min_ticks_cover {d T : Nat}
  58  (pass : Fin T → Pattern d) (covers : Function.Surjective pass) : 2 ^ d ≤ T := by
  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. -/
  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
  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
 105    exact pow_pos (by decide : 0 < (2 : ℕ)) d
 106  exact ⟨w, by simp [hp]⟩
 107
 108/-- The 3‑bit complete cover of period 8 has positive period. -/
 109 theorem period_exactly_8_pos : ∃ w : CompleteCover 3, 0 < w.period := by
 110  obtain ⟨w, hp⟩ := period_exactly_8
 111  have : 0 < (8 : ℕ) := by decide
 112  exact ⟨w, by simp [hp]⟩
 113
 114end Patterns
 115end IndisputableMonolith
 116