Patterns T7 Nyquist Obstruction

The sampling bound

In signal processing, the Nyquist–Shannon sampling theorem says that to reconstruct a continuous signal without losing information, sampling must occur at least twice per cycle of its highest frequency. Sampling too slowly makes high frequencies masquerade as low ones, a failure called aliasing. The Recognition Science declaration T7_nyquist_obstruction proves a discrete, combinatorial cousin of that idea: if fewer than 2^D distinct time slots are available, then no unique pattern can be assigned to every possible sequence of D bits.

The formal statement is stark. Let a pattern of dimension D be a string of D bits, so there are exactly 2^D possible patterns. A complete cover is a finite list of such patterns that includes every possible one at least once. The theorem says: if the list has length T and T is strictly less than 2^D, then no such complete cover exists. In other words, to cover all D-bit patterns without omission, at least 2^D entries are needed. The proof is a counting argument: a list of T entries can contain at most T distinct patterns, so if T is smaller than the number of patterns, some pattern must be missing. The machine-checked library of formal theorems records this as T7_nyquist_obstruction, and the matching positive result, T7_threshold_bijection, shows that at exactly T = 2^D a perfect one-to-one listing exists.

The name comes from the analogy to sampling. In the classical setting, sampling below the Nyquist rate loses information because different continuous signals become indistinguishable. Here, sampling with fewer than 2^D ticks loses information because different bit patterns become indistinguishable: two patterns must map to the same slot. The theorem is a pure cardinality statement, so it holds for any D, not just D = 3. For D = 3, it specializes to the claim that an eight-tick cycle is the minimum needed to cover all three-bit patterns, a result the framework's forcing chain uses to derive the number 2^3.

What the theorem does not claim is just as important. It does not say that any list of length 2^D is a valid cover, only that at least that many entries are necessary. It does not say anything about the order of the patterns, about noise, or about reconstructing a continuous signal from samples. It is a statement about finite sets and surjections, not about physics. The framework may later use this combinatorial fact as a building block, but the theorem itself is a piece of discrete mathematics, proved by counting.

/-- Nyquist-style obstruction: if T < 2^D, no surjection to D-bit patterns. -/
theorem T7_nyquist_obstruction {T D : Nat}
  (hT : T < 2 ^ D) : ¬ ∃ f : Fin T → Pattern D, Function.Surjective f :=
  no_surj_small T D hT

/-- 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 theorem does not guarantee that any list of length 2^D is a valid cover. The theorem says nothing about continuous signals, noise, or reconstruction. The theorem does not by itself derive any physical constant or dimension.

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: