card_eq
The theorem establishes that the elementary abelian 2-group modeled by F2Power D has cardinality exactly 2 raised to D. Researchers modeling finite geometries or chaining cardinalities in the Recognition Science framework cite this result when defining coupled axes and weight distributions. The proof is a term-mode wrapper that unfolds the definition of F2Power and simplifies via library lemmas on the cardinality of finite types and Booleans.
claimLet $F_2^D$ denote the set of all functions from a finite set of cardinality $D$ to a two-element set. Then $|F_2^D| = 2^D$.
background
The module defines F2Power D as the type Fin D → Bool equipped with pointwise XOR, making it the elementary abelian 2-group of rank D. This construction appears in the companion paper Seven_Plots_Three_Dimensions.tex, where the count of 7 non-zero elements at D=3 is asserted to arise from (Z/2Z)^3 excluding zero; the theorem supplies the rigorous cardinality proof so that downstream modules can chain from a proved statement rather than a hardcoded value. The Fintype instance follows directly from the finiteness of the domain and codomain.
proof idea
The proof unfolds F2Power to Fin D → Bool and applies simp with Fintype.card_bool and Fintype.card_fin. These lemmas reduce the cardinality of the function type to the product of the cardinalities of the domain and codomain, which is 2^D.
why it matters in Recognition Science
This theorem is invoked by nonzero_card to obtain the count of non-zero vectors as 2^D - 1, and by RSCoupledAxis to equip CoupledAxis structures with prescribed cardinalities. It further supports the definitions of atmosphereAxis, earthAxis, and oceanAxis in PlanetStrataC2. In the Recognition Science framework it supplies the algebraic foundation for the D=3 case that produces exactly seven non-zero elements, consistent with the eight-tick octave and the derivation of three spatial dimensions. The result replaces an asserted count in the companion paper with a fully proved statement.
scope and limits
- Does not establish the group operation or its axioms for F2Power D.
- Does not apply when D is infinite.
- Does not compute explicit bases, isomorphisms, or enumerations.
- Does not address hamming weights or weight distributions.
Lean usage
example (D : ℕ) : Fintype.card (F2Power D) = 2 ^ D := card_eqformal statement (Lean)
121theorem card_eq : Fintype.card (F2Power D) = 2 ^ D := by
proof body
Term-mode proof.
122 unfold F2Power
123 simp [Fintype.card_bool, Fintype.card_fin]
124
125/-- The number of non-zero vectors in `F2Power D` is `2 ^ D - 1`. -/