F2Power
plain-language theorem explainer
The definition introduces F2Power D as the type of maps from a D-element set to the two-element set, which models the vector space over F2 of dimension D. Narrative theorists and anthropologists cite it to obtain the exact count of seven Booker plot families or eight kinship systems as 2^D - 1 for D = 3. The definition is a direct type abbreviation that lets Mathlib supply the finite type and group instances automatically.
Claim. Let $F_2^D$ denote the set of all functions from the finite set Fin $D$ to the Boolean values, equipped with componentwise addition modulo 2, forming the elementary abelian 2-group of rank $D$.
background
The module Algebra.F2Power supplies the concrete model for the elementary abelian 2-group of rank D inside the Recognition Science framework. The type is defined as Fin D → Bool so that addition is componentwise XOR; the module immediately installs DecidableEq, Fintype and Inhabited instances by unfolding. This construction is used to prove that the number of nonzero elements is exactly 2^D - 1, which for D = 3 yields the seven nonzero vectors that label the Booker plot families.
proof idea
The definition is a one-line type abbreviation F2Power D := Fin D → Bool. The subsequent instances for DecidableEq, Fintype and Inhabited are obtained by unfolding the abbreviation and delegating to the corresponding instances on function types. No further lemmas are required.
why it matters
This definition supplies the algebraic substrate for the NarrativeGeodesicCert in Aesthetics.NarrativeGeodesic, which records that the seven Booker plot families stand in bijection with the nonzero elements of F2Power 3. It thereby realizes the structural claim that the count 7 arises as 2^3 - 1 from the dimension D = 3 rather than from an ad-hoc enumeration. The construction aligns with the eight-tick octave (period 2^3) and the emergence of three spatial dimensions in the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.