Patterns

Patterns

A pattern in Recognition Science is a fixed-length string of bits, a row of true and false values of some length d. The set of all d-bit patterns is finite, and its size is exactly 2^d. The Patterns module studies how many of these patterns a recognition process must pass through to see every one at least once. A complete cover is a sequence of patterns, one per tick, that hits every possible pattern. The module proves that for any dimension d there is a complete cover whose length is exactly 2^d, and that no shorter sequence can cover them all.

The central result is a counting argument. If a sequence has fewer than 2^d entries, it cannot list every d-bit pattern, because there are simply more patterns than entries. A surjective function from a set of size T to the set of patterns exists only when T is at least 2^d. This lower bound is sharp: at exactly T = 2^d, a bijection exists, so a complete cover of that length is possible. The theorem cover_exact_pow constructs such a cover directly, and the lemma no_surj_small rules out anything shorter.

For three-bit patterns, the theorem forces an eight-tick minimum. Any complete pass through all 3-bit patterns needs at least 8 ticks, and a cover of exactly 8 ticks exists. This is the same structure that appears elsewhere in Recognition Science as the eight-tick recognition cycle, and the module names the obstruction a Nyquist-style limit: below the threshold of 2^D, no surjection to D-bit patterns is possible. The threshold is where aliasing disappears, because the map becomes bijective.

The module is a formal backbone for a counting fact. It does not say which patterns are meaningful, nor how a recognition process chooses its path. It fixes the size of the pattern space and the minimum length of a complete traversal. Everything else about patterns, their order, their use, or their relation to physical recognition, is a separate question.

THEOREM card_pattern · IndisputableMonolith/Patterns.lean

THEOREM cover_exact_pow · IndisputableMonolith/Patterns.lean

THEOREM min_ticks_cover · IndisputableMonolith/Patterns.lean

THEOREM eight_tick_min · IndisputableMonolith/Patterns.lean

THEOREM T7_threshold_bijection · IndisputableMonolith/Patterns.lean

What this page does not claim

Not claiming which patterns are physically realized. Not claiming that patterns themselves are derived from the cost function. Not claiming that the eight-tick minimum is the same object as the recognition cycle's eight ticks.

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: