neg_eq_self
plain-language theorem explainer
In the elementary abelian 2-group of rank D realized as maps from Fin D to Bool under pointwise XOR, every element equals its own additive inverse. Researchers counting the seven nonzero vectors at D=3 or building the Booker bijection cite this when simplifying inverse expressions in weight or subgroup calculations. The proof is a one-line reflexivity that follows once subtraction is defined to coincide with addition.
Claim. Let $G$ be the elementary abelian 2-group of rank $D$, realized as the set of functions from a finite set of cardinality $D$ to the booleans with componentwise XOR. Then for every $v$ in $G$, the additive inverse satisfies $-v = v$.
background
The module constructs F2Power D as the type Fin D → Bool equipped with pointwise XOR, yielding the elementary abelian 2-group of rank D together with its Fintype instance. This supplies the combinatorial counts used for the seven nonzero elements at D=3 and the 1+3+3+1 weight decomposition. The upstream definition F2Power supplies the underlying type on which the AddCommGroup structure and the Sub instance are declared.
proof idea
The proof is a one-line term-mode reflexivity. It applies after the Sub instance is defined by u - v := u + v, so that negation of v reduces to 0 + v, which equals v by the characteristic-2 relation already present in the group instance.
why it matters
The result completes the additive inverse law inside the F2Power group structure, allowing the module to deliver the exact count of seven nonzero vectors at D=3 without extra hypotheses. This count feeds the Booker bijection and the subgroup enumeration required by downstream constructions such as NarrativeGeodesic. The module documentation notes that the falsifier would be any D where the nonzero cardinality deviates from 2^D - 1, which is combinatorially impossible.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.