Patterns Min Ticks Cover

The fewest ticks

A machine that, at each tick of a clock, displays one pattern of lights. The patterns are drawn from all possible arrangements of d binary lights, so there are 2^d distinct patterns. The question is simple: how many ticks must the machine run before it has displayed every possible pattern at least once? The answer, proved in the machine-checked library of formal theorems, is that no listing can succeed in fewer than 2^d ticks. This is the content of the declaration min_ticks_cover.

The proof is a counting argument, and it is airtight. If a listing of length T shows every pattern, then it defines a function from the T tick positions onto the set of all patterns. A function that lands on every one of 2^d targets must have at least 2^d inputs. The library formalizes this as: if T < 2^d, then no such covering function exists. A companion result shows the bound is sharp: at exactly 2^d ticks, a listing exists that shows each pattern precisely once, a bijection. So the minimum is not merely a lower bound; it is attained.

For the special case of three lights, there are 2^3 = 8 patterns, and the declaration eight_tick_min states the consequence: any complete listing needs at least 8 ticks. The library also records a threshold bijection at T = 2^D, meaning at the boundary there is no aliasing: each pattern appears exactly once. The same counting principle appears in signal processing as the Nyquist obstruction, and the library names it so: if you sample fewer than 2^D times, you cannot distinguish all D-bit patterns.

In Recognition Science, this counting fact is the seed of the framework's eighth tick. The framework models a ledger, a discrete record of events, and asks how many ticks are needed to cover all possible three-bit states. The answer, eight, is forced by the pigeonhole principle alone, before any physics enters. The framework's larger claim is that this eight-tick cycle then propagates through the forcing chain to yield three spatial dimensions, but that chain is a separate, much larger theorem. The declaration min_ticks_cover itself establishes only the counting bound, nothing more.

What the declaration does not claim is just as important. It does not say that an eight-tick listing is unique, only that one exists and none shorter does. It does not assert that the bound holds for patterns with any other structure, such as continuous values or weighted states; it concerns only finite binary patterns. And it does not, by itself, derive the golden ratio, the fine-structure constant, or any physical constant. Those results live elsewhere in the framework and depend on additional structure beyond a simple counting argument.

/-- Minimal ticks lower bound for a complete cover. -/
lemma min_ticks_cover {d T : Nat}
  (pass : Fin T → Pattern d) (covers : Function.Surjective pass) : 2 ^ d ≤ T := by
  classical
  by_contra h
  exact (no_surj_small T d (lt_of_not_ge h)) ⟨pass, covers⟩

/-- 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

/-- At threshold T=2^D there is a bijection (no aliasing). -/
theorem T7_threshold_bijection (D : Nat) : ∃ f : Fin (2 ^ D) → Pattern D, Function.Bijective f := by
  classical
  let e := (Fintype.equivFin (Pattern D))
  have hcard : Fintype.card (Pattern D) = 2 ^ D := by exact card_pattern D
  -- Manual cast equivalence between Fin (2^D) and Fin (Fintype.card (Pattern D))
  let castTo : Fin (2 ^ D) → Fin (Fintype.card (Pattern D)) :=
    fun i => ⟨i.1, by
      -- rewrite the goal via hcard and close with i.2
      have : i.1 < 2 ^ D := i.2
      simp [this]⟩
  let castFrom : Fin (Fintype.card (Pattern D)) → Fin (2 ^ D) :=
    fun j => ⟨j.1, by simpa [hcard] using j.2⟩
  have hLeft : Function.LeftInverse castFrom castTo := by intro i; cases i; rfl
  have hRight : Function.RightInverse castFrom castTo := by intro j; cases j; rfl
  have hCastBij : Function.Bijective castTo := ⟨hLeft.injective, hRight.surjective⟩
  refine ⟨fun i => (e.symm) (castTo i), ?_⟩
  exact (e.symm).bijective.comp hCastBij

/-‑ ## T6 alias theorems -/
 theorem T6_exist_exact_2pow (d : Nat) : ∃ w : CompleteCover d, w.period = 2 ^ d :=
  cover_exact_pow d

 theorem T6_exist_8 : ∃ w : CompleteCover 3, w.period = 8 :=
  period_exactly_8

/-‑ ## Minimal counting facts and eight‑tick lower bound -/

/-- 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

The declaration does not assert uniqueness of the minimal listing. The declaration does not apply to patterns with continuous or weighted states. The declaration does not by itself derive any physical constant such as the golden ratio or the fine-structure constant.

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: