zero_apply
plain-language theorem explainer
The theorem records that the zero element of the elementary abelian 2-group of rank D evaluates to false at every coordinate. It is invoked by the zero-Hamming-weight lemma in the same module to simplify weight calculations. The proof is a direct reflexivity step once zero is introduced as the constant-false function.
Claim. For every index $i$ in the finite set of size $D$, the zero element of the vector space $V = (Z/2Z)^D$ satisfies $0_i = 0$.
background
The module models the elementary abelian 2-group of rank D as the function type Fin D → Bool with pointwise XOR serving as addition. The companion paper Seven Plots Three Dimensions asserts that the 7 basic plot families arise from the 2^3 - 1 nonzero elements of this group when D = 3; the present module supplies the supporting theorems. The upstream definition F2Power supplies the type together with the zero element realized as the constant-false function.
proof idea
The proof is a one-line term proof consisting of reflexivity after the definition of zero as the constant-false function on Fin D.
why it matters
It supplies the base case for the hammingWeight_zero theorem, which in turn enables the weight-class cardinalities and the exact count of 7 nonzero elements at D = 3. These facts underwrite the subgroup lattice used by NarrativeGeodesic for the Booker bijection. The result closes a foundational property required by the Recognition Science forcing chain at the level of the eight-tick octave and D = 3.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.