Patterns T7 Threshold Bijection

The threshold bijection

A binary pattern is a finite string of bits, each bit either 0 or 1. For a fixed length D, there are exactly 2^D possible distinct patterns. If you want a sequence of such patterns that shows every possible one at least once, the sequence must have at least 2^D entries. This is a basic counting argument: with fewer entries than patterns, some pattern must be missing, a fact the framework proves as a lemma.

The Recognition Science framework, in its machine-checked library of formal theorems, formalizes this idea. Its declaration T7_threshold_bijection states that when the sequence length equals exactly 2^D, a bijection exists: a one-to-one pairing between the time slots and the patterns. At this threshold, each pattern appears exactly once, with no repetitions and no omissions. The framework derives this from the cardinality of the pattern space, which it computes as 2^D.

For the specific case of three-bit patterns, the result gives an eight-tick cycle. There are 2^3 = 8 possible patterns, and the framework proves that any complete pass through them needs at least 8 ticks. A complete cover of exactly 8 ticks exists, forming a cycle where each of the 8 patterns appears precisely once. This is the framework's T7 milestone, one step in its chain forcing the number 2^3.

The framework also proves a companion obstruction: if the sequence has fewer than 2^D entries, no surjection to all D-bit patterns exists. This is a Nyquist-style limit, analogous to the sampling theorem in signal processing, where undersampling loses information. At the threshold, the bijection guarantees no aliasing; below it, information is necessarily lost.

What the declaration does not claim is that this bijection is unique, that it has any particular structure, or that it relates to physical recognition events. The theorem establishes existence of a bijection at the threshold, nothing more. The framework's larger claims about an eight-tick recognition cycle and three spatial dimensions build on this result, but the bijection itself is a pure combinatorial fact about finite sets.

/-- Cardinality of the pattern space. -/
lemma card_pattern (d : Nat) : Fintype.card (Pattern d) = 2 ^ d := by
  classical
  simp [Pattern, Fintype.card_fin] at*

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

/-- 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 bijection is not claimed to be unique or to have any particular structure. The theorem does not claim any physical interpretation of the patterns or the bijection. The result does not by itself establish the framework's larger claims about recognition cycles or spatial dimensions.

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: