zero_apply
plain-language theorem explainer
The zero element of F2Power D, the elementary abelian 2-group modeled as functions Fin D to Bool, evaluates to false at every coordinate i. Workers on finite vector spaces over GF(2) or on the Recognition Science count of 7 nonzero elements at D=3 would cite this base fact for pointwise operations. The proof is a one-line reflexivity after the definition of the constant-false zero function.
Claim. Let $0$ denote the zero element of the group $F_2^D := (Fin D) → {true, false}$ with pointwise XOR. Then $0(i) = false$ for all $i ∈ Fin D$.
background
F2Power D is defined as the type Fin D → Bool, the elementary abelian 2-group of rank D whose addition is pointwise XOR. The module proves that this group has cardinality 2^D and that the number of nonzero elements is exactly 2^D - 1, with the D=3 case supplying the count 7 required by the companion paper Seven_Plots_Three_Dimensions.tex. The upstream definition F2Power supplies the underlying type on which the zero element is the constant-false function.
proof idea
The proof is a one-line term that applies reflexivity (rfl) to the definition of the zero element of F2Power D.
why it matters
This supplies the base case used by hammingWeight_zero to conclude that the Hamming weight of zero is zero. It belongs to the F2Power module that replaces hardcoded counts with theorems, enabling downstream results on the 7 subgroups of (Z/2)^3 that appear in Aesthetics.NarrativeGeodesic and the Booker bijection. The module establishes the combinatorial facts asserted in the companion paper.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.