T7_nyquist_obstruction
plain-language theorem explainer
The declaration proves that for natural numbers T and D with T strictly less than 2 to the power D, no surjective map exists from a T-element set onto the full collection of D-bit patterns. Researchers bounding distinguishable states in discrete sampling or pattern recognition within the Recognition Science framework would cite this bound when establishing minimal coverage thresholds. The proof is a direct term application of the sibling combinatorial lemma no_surj_small.
Claim. Let $T, D$ be natural numbers satisfying $T < 2^D$. Then no surjective function exists from a set of cardinality $T$ to the set of all maps from Fin $D$ to Bool.
background
In the Patterns module, Pattern D is defined as the set of all functions from Fin D to Bool, giving exactly 2^D distinct D-bit patterns. The local setting concerns finite pattern covering under the eight-tick periodicity constraints of the T7 development. The result depends on the fundamental period abbreviation T from Breath1024 and the direct combinatorial obstruction encoded in the sibling no_surj_small.
proof idea
The proof is a one-line term wrapper that applies the lemma no_surj_small to the parameters T, D and the hypothesis hT.
why it matters
This fills the Nyquist obstruction step inside the T7 eight-tick octave development of the Recognition Science forcing chain, showing that fewer than 2^D samples cannot cover all patterns before the period-8 structure can be realized. It supports the D=3 spatial dimension claim by bounding the sample requirement for full pattern distinguishability. No downstream uses are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.