instFintypePattern
plain-language theorem explainer
The type of binary patterns of length d is finite for any natural number d. Researchers working on discrete pattern recognition or stream processing in Recognition Science would cite this to ensure that pattern spaces admit finite enumeration and cardinality arguments. The proof is a one-line wrapper that reduces the definition to the standard Fintype instance for function spaces over finite domains.
Claim. For every natural number $d$, the set of functions from the finite set Fin $d$ to the two-element set is finite.
background
In the Patterns module, Pattern d is defined as the function type Fin d → Bool, representing all binary sequences of exact length d. This matches the finite-window definitions appearing in Measurement, Streams, and Streams.Blocks, where such patterns serve as the domains for integer functionals that count ones or other discrete properties. The local setting is the discrete layer of Recognition Science that prepares finite pattern spaces for the eight-tick octave constructions.
proof idea
The proof is a one-line wrapper: it applies dsimp to unfold Pattern d into Fin d → Bool, then lets infer_instance supply the standard Fintype structure on finite function spaces.
why it matters
This instance supplies the finite-type structure required by sibling results such as card_pattern, cover_exact_pow, min_ticks_cover, and the T7 statements eight_tick_min, T7_nyquist_obstruction, and T7_threshold_bijection. It thereby supports the finite enumeration steps that feed the Recognition Composition Law and the phi-ladder counting arguments. No open questions are directly addressed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.