Verification Nyquist Obstruction Cert

The sampling limit

In signal processing, the Nyquist–Shannon sampling theorem says that to capture a signal faithfully a system must sample it at least twice as fast as its highest frequency. Sampling too slowly causes high frequencies to disguise themselves as low ones, an effect called aliasing. The Nyquist obstruction certificate is the Recognition Science version of that same limit, applied not to audio or radio waves but to the framework's own ledger, a discrete record of events. The certificate is a machine-checked theorem in the framework's library of formal proofs, and it establishes a precise counting fact: if a system samples at rate T, it cannot resolve D bits of information when T is less than 2^D.

The classical mathematics is simple. A set of T sampling positions can produce at most T distinct outcomes. A pattern of D bits has exactly 2^D possible values. If T is smaller than 2^D, there are more patterns than samples, so by the pigeonhole principle at least two patterns must share a sample, meaning some information is lost. The framework's proof formalizes this as a theorem about functions: there is no surjection from a set of size T onto the set of D-bit patterns when T < 2^D. At the threshold T = 2^D, the proof also shows a bijection exists, meaning every pattern gets its own sample and no information is lost.

The framework applies this to its model of spatial dimensions. Its forcing chain derives that space has three dimensions, so D = 3. The certificate then plugs in that number: with three dimensions, the minimum sampling period is 2^3 = 8. A period shorter than eight ticks cannot cover all possible three-dimensional states, and a period of exactly eight ticks can. This is the information-theoretic reason the framework's recognition cycle has eight ticks, neither more nor less. The proof is purely structural, using cardinality comparisons and finite-type equivalences, with no empirical constants and no unproved assumptions.

In Recognition Science, this certificate is one half of a pair. Together with a separate lower-bound certificate, it shows the eight-tick period is both sufficient and necessary. The practical upshot is a clean statement about information and geometry: three dimensions require at least eight distinct states in the ledger, and eight is exactly enough. The framework's library records this as a proved theorem, not a heuristic or a fitted parameter.

/-- Information-theoretic interpretation: D bits require 2^D samples minimum. -/
theorem information_lower_bound (D : ℕ) :
    ∀ T : ℕ, T < 2^D → ¬∃ f : Fin T → Pattern D, Function.Surjective f :=
  fun T hT => T7_nyquist_obstruction hT

structure NyquistObstructionCert where
  deriving Repr

structure NyquistObstructionCert where
  deriving Repr

/-- The eight-tick period is forced by Nyquist: neither more nor less. -/
theorem eight_tick_nyquist_forced :
    (∀ T : ℕ, T < 8 → ¬∃ f : Fin T → Pattern 3, Function.Surjective f) ∧
    (∃ f : Fin 8 → Pattern 3, Function.Bijective f) :=
  ⟨fun T hT => T7_nyquist_obstruction (by simpa using hT),
   by simpa using T7_threshold_bijection 3⟩

What this page does not claim

This certificate does not derive the value of three dimensions; it assumes D = 3 as an input. This certificate does not prove the Nyquist–Shannon theorem for continuous signals; it proves a discrete counting analogue. This certificate does not claim that physical sampling in the real world obeys this limit; it is a statement about the framework's ledger model.

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/Verification/NyquistObstructionCert.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: