card_pattern
The lemma establishes that the set of all binary patterns of length d has cardinality exactly 2^d. Researchers proving threshold bijections or Gray-code coverings in the Recognition framework cite this when they need the exact size of the pattern space. The proof is a one-line term simplification that unfolds the definition of Pattern as maps from Fin d to Bool and applies the standard Fintype cardinality rule for function spaces.
claimThe cardinality of the set of all functions from a $d$-element set to a two-element set equals $2^d$. In symbols, $|Fin d → Bool| = 2^d$.
background
In the Patterns module, Pattern d is defined as the type (Fin d → Bool), i.e., the set of all binary strings of length d. This matches the alias in the Measurement module for finite windows of length n. The local setting concerns counting distinct patterns to support covering arguments and bijective thresholds. Upstream results supply the basic Fintype.card_fin lemma and the definition of T as natural numbers, but the cardinality step itself rests only on the function-space rule.
proof idea
The proof is a term-mode simplification. It invokes classical, then applies simp with the lemmas Pattern and Fintype.card_fin to reduce the cardinality of the function space directly to 2^d.
why it matters in Recognition Science
This cardinality result is invoked by no_surj_small to prove absence of surjections when T < 2^d and by T7_threshold_bijection to obtain a bijection exactly at T = 2^D. It supplies the counting step required for the eight-tick octave (T7) in the forcing chain and for the Gray-cycle constructions that appear in the downstream GrayCycle modules. The result closes the finite-pattern counting prerequisite before any adjacency or covering properties are imposed.
scope and limits
- Does not impose any ordering or adjacency relation on the patterns.
- Does not extend the count to infinite d.
- Does not prove existence of a surjective or injective map.
- Does not reference phi, the forcing chain, or physical constants.
Lean usage
have hcard : Fintype.card (Pattern D) = 2 ^ D := card_pattern Dformal statement (Lean)
36lemma card_pattern (d : Nat) : Fintype.card (Pattern d) = 2 ^ d := by
proof body
Term-mode proof.
37 classical
38 simp [Pattern, Fintype.card_fin] at*
39
40/-- No surjection to all d-bit patterns if T < 2^d. -/