CompleteCover

formal source

  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