add_apply
plain-language theorem explainer
Addition on the elementary abelian 2-group F2Power D acts componentwise by XOR on the Boolean-valued functions. Researchers modeling the (Z/2)^D structure for the seven-plot count in Recognition Science cite this to confirm the group law matches the function definition. The proof is a one-line term reflexivity that follows directly from the pointwise addition rule.
Claim. Let $V_D$ be the elementary abelian 2-group of rank $D$, realized as maps from Fin $D$ to Bool with pointwise XOR. For any $u,v$ in $V_D$ and index $i$ in Fin $D$, the $i$-th component of $u+v$ equals the exclusive-or of the $i$-th components of $u$ and $v$.
background
The module defines F2Power D as the type Fin D → Bool equipped with pointwise XOR to realize the elementary abelian 2-group of rank D. This supplies the carrier and operation for the AddCommGroup instance, the cardinality result 2^D, and the nonzero count 2^D-1 that yields exactly seven elements when D=3. The companion paper Seven_Plots_Three_Dimensions.tex asserts that this count equals the number of basic plot families; the present module replaces that assertion with a theorem.
proof idea
The proof is a term-mode reflexivity. It matches (u + v) i against xor (u i) (v i) by the definition of addition on the function type F2Power D.
why it matters
This lemma records the explicit group law inside F2Power, which directly supports the nonzero_card and weight-decomposition theorems at D=3. Those results enable the subgroup bijection used in Aesthetics.NarrativeGeodesic and the downstream modules that chain off the seven-plot count. It supplies the algebraic prerequisite for the claim in Seven_Plots_Three_Dimensions.tex that the number of basic plots is 2^3-1.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.