Patterns Cover Exact Pow

Exact covering

A row of d switches, each either on or off. A pattern is one setting of all d switches. With d switches there are 2^d possible patterns: for d=1 that is 2, for d=2 it is 4, for d=3 it is 8, and so on. The question is whether a single sequence of patterns, one per tick of a clock, can visit every possible pattern exactly once and then stop. The answer is yes, and the sequence needs exactly 2^d ticks.

This is a pure counting fact, not a physical claim. If your sequence has fewer than 2^d entries, it cannot possibly show all patterns, because there are more patterns than entries. If it has exactly 2^d entries, you can simply list the patterns in any order, for example in binary counting order: 000, 001, 010, 011, 100, 101, 110, 111 for d=3. That list is a complete cover: it hits every pattern, and its length is exactly 2^d. The machine-checked theorem cover_exact_pow in the framework's library of formal theorems proves this for every dimension d.

In Recognition Science, this exact cover is the counting backbone of the eight-tick cycle. The framework derives an eight-tick recognition cycle from its cost forcing chain, and this theorem supplies the combinatorial reason eight is the minimal complete length for three-bit patterns: with three switches there are exactly eight patterns, so a complete pass needs at least eight ticks, and eight ticks suffice. The same theorem gives the general d-dimensional statement, of which the three-bit case is the instance d=3.

What the theorem does not claim is just as important. It does not say that the binary counting order is the only complete cover, nor that any particular ordering is physically preferred. It does not say that a complete cover exists for every period, only for the exact period 2^d. And it does not say anything about which patterns are meaningful or how they relate to each other; it is purely a statement about counting and listing. The framework's larger claims about why eight ticks arise from the cost function are separate theorems, not consequences of this counting lemma alone.

/-- There exists a complete cover of exact length `2^d` for d‑dimensional patterns. -/
theorem cover_exact_pow (d : Nat) : ∃ w : CompleteCover d, w.period = 2 ^ d := by
  classical
  let e := (Fintype.equivFin (Pattern d)).symm
  refine ⟨{ period := Fintype.card (Pattern d)
          , path := fun i => e i
          , complete := (Fintype.equivFin (Pattern d)).symm.surjective }, ?_⟩
  have : Fintype.card (Pattern d) = 2 ^ d := by
    simp [Pattern, Fintype.card_bool, Fintype.card_fin]
  exact this

/-- No surjection to all d-bit patterns if T < 2^d. -/
lemma no_surj_small (T d : Nat) (hT : T < 2 ^ d) :
  ¬ ∃ f : Fin T → Pattern d, Function.Surjective f := by
  classical
  intro h; rcases h with ⟨f, hf⟩
  obtain ⟨g, hg⟩ := hf.hasRightInverse
  have hginj : Injective g := by
    intro y₁ y₂ hgy
    have : f (g y₁) = f (g y₂) := by simp [hgy]
    simpa [RightInverse, hg y₁, hg y₂] using this
  have hcard : Fintype.card (Pattern d) ≤ Fintype.card (Fin T) :=
    Fintype.card_le_of_injective _ hginj
  have : 2 ^ d ≤ T := by
    simpa [Fintype.card_fin, card_pattern d] using hcard
  exact (lt_of_le_of_lt this hT).false

/-- For 3-bit patterns, any complete pass has length at least 8. -/
lemma eight_tick_min {T : Nat}
  (pass : Fin T → Pattern 3) (covers : Function.Surjective pass) : 8 ≤ T := by
  simpa using (min_ticks_cover (d := 3) (T := T) pass covers)

What this page does not claim

This theorem does not claim that binary counting order is the only complete cover. It does not claim that any particular ordering of patterns is physically meaningful. It does not claim that eight ticks arise from the cost function; that is a separate forcing-chain result.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Patterns.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: