T7_threshold_bijection
plain-language theorem explainer
For any natural number D the set of all maps from D bits to boolean values stands in bijection with the finite set of size 2^D. Workers on the Recognition Science forcing chain at T7 would cite the result to confirm saturation without aliasing at the octave threshold. The argument obtains the Fintype equivalence for Pattern D, invokes the cardinality fact card_pattern D, builds explicit Fin casts, and composes to a bijection.
Claim. For every natural number $D$ there exists a bijective function from the set of integers from 0 to $2^D-1$ to the set of all maps from a $D$-element index set to the two-element boolean set.
background
Pattern D denotes the type of all functions from Fin D to Bool, hence the full space of 2^D binary assignments of length D. The Patterns module develops counting facts that support complete covers and the eight-tick regime. The proof depends on the sibling lemma card_pattern D, which establishes that the cardinality of this pattern space equals exactly 2^D.
proof idea
The tactic proof begins with classical logic and the Fintype.equivFin equivalence for Pattern D. It records the cardinality equality via card_pattern D, defines forward and backward casts between Fin (2^D) and Fin of that cardinality, proves the casts are mutual inverses by case analysis, obtains the induced bijection on the casts, and finally composes with the inverse equivalence.
why it matters
The declaration supplies the T7 threshold bijection required by the Patterns module to guarantee that pattern space saturates exactly at size 2^D. It directly supports the eight-tick octave landmark (period 2^3) in the forcing chain by ruling out aliasing. No downstream results are recorded.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.