no_surj_small
plain-language theorem explainer
If T is strictly less than 2^d then no map from a T-element domain onto the full space of d-bit patterns can exist. Workers on the T7 octave and Nyquist obstructions in the Recognition forcing chain cite this bound to control minimal cover sizes. The argument assumes a surjection, extracts a right inverse, proves the inverse is injective, and obtains the contradictory inequality 2^d <= T via the card_pattern cardinality lemma.
Claim. If $T < 2^d$, then there does not exist a surjective function $f$ from the set of $T$ elements to the set of all maps from a $d$-element index set to the two-element boolean set.
background
Pattern d is defined as the type Fin d → Bool, the finite set of all possible d-bit strings. Its cardinality is given by the sibling lemma card_pattern, which states that Fintype.card (Pattern d) equals 2^d. The Patterns module assembles covering arguments that feed the T7 step of the forcing chain; the present lemma supplies the strict inequality direction needed for Nyquist-style obstructions. Upstream results include the complete predicate from SAT back-propagation and the T abbreviation from Breath1024, both used to frame finite windows and periods.
proof idea
The tactic proof opens with classical, assumes a surjection f, obtains a right inverse g via hasRightInverse, then shows g is injective by transporting equality through f and the right-inverse equations. It applies Fintype.card_le_of_injective to conclude that the pattern cardinality is at most T, rewrites via card_pattern and Fintype.card_fin to reach 2^d <= T, and finishes with a contradiction to the hypothesis T < 2^d.
why it matters
The lemma is the direct source for both min_ticks_cover (which extracts the lower bound 2^d <= T for any surjective pass) and T7_nyquist_obstruction (which is literally the same statement with renamed variables). It therefore encodes the sampling obstruction at the T7 eight-tick octave of the UnifiedForcingChain, where D spatial dimensions and the phi-ladder require at least 2^D distinct patterns to avoid aliasing. No open scaffolding remains; the result is fully proved.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.