IndisputableMonolith.Algebra.F2Power
The module defines the elementary abelian 2-group of rank D as the set of functions from a D-element index set to boolean values with pointwise XOR. Researchers on combinatorial structures in three dimensions cite it for the cube Q3 and for counting laws that produce 2^D minus one. It supplies the basic group operations and cardinality facts that enable downstream narrative and pattern constructions. The module is purely definitional with elementary verifications of the group axioms.
claimThe elementary abelian 2-group of rank $D$, realized as the set of all maps from a finite set of cardinality $D$ to the two-element set, equipped with componentwise addition modulo 2.
background
Recognition Science uses this algebraic object to encode binary choices across D dimensions, where the forcing chain fixes D at three. The group operation is the symmetric difference of boolean vectors, yielding an abelian group that is also a vector space over the field with two elements. The module records the order 2^D together with the count of nonzero elements 2^D minus one.
proof idea
This is a definition module, no proofs.
why it matters in Recognition Science
The module supplies the group-theoretic substrate for the narrative geodesic on the cube Q3 and the 2^D minus 1 count law. The former deepens the structural analysis of Booker's seven plot families; the latter extends the same counting principle to gauge-boson families at D equals 3 and to opponent-color channels at D equals 2. It closes the algebraic prerequisite for these applications in the Recognition framework.
scope and limits
- Does not connect the group to the J-uniqueness or phi fixed point.
- Does not derive the value of D from upstream forcing steps.
- Does not include any physical constants or mass formulas.
- Does not treat non-elementary groups or higher-rank cases beyond the definition.
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