IndisputableMonolith.Algebra.F2Power
This module defines the elementary abelian 2-group of rank D as the set of maps from Fin D to Bool with pointwise XOR. It is cited by downstream modules that apply the structure to combinatorial counts in D dimensions. The module consists entirely of definitions and basic lemmas establishing the group operations and cardinality.
claimThe elementary abelian 2-group of rank \(D\) is modeled as the set of maps \(\mathrm{Fin}(D) \to \mathrm{Bool}\) equipped with pointwise XOR.
background
The module introduces the standard model of the vector space (\mathbb{F}_2^D) over the field with two elements. The doc-comment states that the group is realized concretely as functions from a finite index set of size D to the boolean type, with the group law given by pointwise XOR.
This algebraic object supplies the hypercube structure used for counting arguments. The module imports only Mathlib and defines the group together with its zero element, addition, negation, and Hamming weight function.
proof idea
this is a definition module, no proofs
why it matters in Recognition Science
The module supplies the algebraic model of the D-dimensional hypercube that feeds NarrativeGeodesic (narrative geodesic on Q3) and TwoToTheDMinusOne (the 2^D-1 count law). These downstream results use the construction to obtain the count of seven for Booker's plot families and for gauge-boson families at D=3.
scope and limits
- Does not extend the definition beyond finite rank D.
- Does not include any theorems from the forcing chain or J-function.
- Does not provide physical interpretations or mass formulas.
used by (2)
declarations in this module (28)
-
def
F2Power -
theorem
zero_apply -
theorem
add_apply -
theorem
neg_eq_self -
theorem
sub_eq_add -
theorem
add_self -
theorem
card_eq -
theorem
nonzero_card -
theorem
nonzero_card_three -
def
hammingWeight -
theorem
hammingWeight_zero -
theorem
hammingWeight_le -
theorem
weight_zero_iff -
theorem
card_weight_zero_three -
def
axis1 -
def
axis2 -
def
axis3 -
theorem
axis1_weight -
theorem
axis2_weight -
theorem
axis3_weight -
def
axis12 -
def
axis13 -
def
axis23 -
def
axis123 -
theorem
axis123_weight -
def
oneDimSubspace -
theorem
oneDimSubspace_card -
theorem
oneDimSubspace_closed