card_pattern
plain-language theorem explainer
The d-bit pattern space has cardinality exactly 2^d. Researchers constructing threshold bijections or Gray-cycle covers cite the result to equate the sizes of Fin (2^d) and the pattern set before proving surjectivity or injectivity. The argument is a one-line simplification that unfolds the function-space definition and applies the standard cardinality of maps out of Fin.
Claim. Let $P_d$ be the set of all functions from a $d$-element set to a two-element set. Then $|P_d| = 2^d$.
background
In the Patterns module the type Pattern d is introduced as the function space (Fin d → Bool). This is the set of all binary strings of length d, equivalently the power set of a d-element index set. The module imports only Mathlib and works alongside the Measurement alias that re-exports the same finite-window notion from PatternLayer.
proof idea
The proof is a one-line wrapper. It opens classical reasoning and then applies simp with the local definition of Pattern together with the library fact Fintype.card_fin, which directly yields the power-of-two cardinality of the function type.
why it matters
The lemma supplies the exact count required by no_surj_small (no surjection exists when T < 2^d) and by T7_threshold_bijection (a bijection exists precisely when T = 2^D). It is also invoked inside the GrayCycle and GrayCycleBRGC constructions to certify that brgcPath realises a complete cover. Within the Recognition framework the result underwrites the eight-tick octave (T7) by confirming that the pattern space size matches the period 2^3 when d = 3, and it closes the cardinality step needed for the D = 3 spatial-dimension claim.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.