`Pattern`

definition

show as: view math explainer →

module: IndisputableMonolith.Patterns
domain: Patterns
line: 9 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Patterns on GitHub at line 9.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

used by

formal source

   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

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.