IndisputableMonolith.Algebra.F2Power
The F2Power module defines the elementary abelian 2-group of rank D as functions Fin D to Bool with pointwise XOR. Researchers modeling binary vector spaces for D-dimensional counting or geodesic arguments in Recognition Science cite it. The module consists of the core definition plus basic lemmas on group operations and Hamming weight.
claimThe elementary abelian 2-group of rank $D$, denoted $(Z/2Z)^D$, is modeled as the set of maps $Fin D to Bool$ equipped with pointwise XOR as the group operation.
background
This module sits in the Algebra section and introduces the finite vector space over GF(2) of dimension D. The group is realized concretely as functions from a D-element index set to the two-point set Bool, with addition given by symmetric difference (XOR). Basic properties supplied include the zero map, pointwise addition, self-inverse negation, and the Hamming weight function that counts the number of true entries.
proof idea
This is a definition module, no proofs.
why it matters in Recognition Science
The module supplies the algebraic model of the cube Q3 = (Z/2)^3 used in NarrativeGeodesic for structural closure on Booker's seven plot families. It also underpins the 2^D-1 Count Law in TwoToTheDMinusOne, which produces the count 7 at D=3 for both narrative families and gauge-boson classifications. This directly supports the framework landmark that fixes D=3 spatial dimensions.
scope and limits
- Does not derive physical constants or mass ladders.
- Does not invoke the J-cost function or Recognition Composition Law.
- Does not prove fixed-point or uniqueness results.
- Does not extend beyond rank-D binary groups.
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