card_pattern
plain-language theorem explainer
The lemma states that the space of all binary patterns of length d has cardinality exactly 2^d. Researchers proving threshold bijections or Gray-code covers cite this count when matching domain sizes to pattern spaces. The proof is a one-line simplification that unfolds the definition of Pattern as maps from Fin d to Bool and applies the standard cardinality of finite function spaces.
Claim. Let $P(d)$ denote the set of all functions from the finite set of $d$ elements to the two-element Boolean set. Then the cardinality of $P(d)$ equals $2^d$.
background
Pattern(d) is defined as the type of maps from Fin d to Bool, i.e., all possible binary sequences of exact length d. This definition sits in the Patterns module and is referenced by measurement abstractions that treat finite windows of length n as the same object. The module also imports standard finite-type machinery from Mathlib to support cardinality calculations.
proof idea
The proof is a one-line wrapper that applies classical reasoning followed by simplification on the definition of Pattern together with the known cardinality of Fin d and the function space to Bool.
why it matters
This cardinality feeds directly into no_surj_small (absence of surjections for T < 2^d) and T7_threshold_bijection (existence of bijection at T = 2^D). It supplies the counting step required for Gray-cycle constructions and supports the eight-tick octave (T7) by confirming that the pattern space size matches the dimension count needed for bijective covers.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.