sub_eq_add
plain-language theorem explainer
In the elementary abelian 2-group of rank D, modeled as maps from Fin D to Bool under pointwise XOR, subtraction coincides with addition because every element equals its own inverse. Recognition Science researchers and algebraists working on the (Z/2)^D structure cite the result to rewrite differences directly as sums in group expressions. The proof is immediate reflexivity once the AddCommGroup instance is in place.
Claim. For all elements $u, v$ in the elementary abelian 2-group of rank $D$, $u - v = u + v$.
background
F2Power D is the type Fin D → Bool equipped with pointwise XOR as the group operation, yielding the vector space over GF(2) of dimension D. The module installs an AddCommGroup instance on this type and derives basic counting results such as nonzero_card = 2^D - 1. Upstream lemmas from ArithmeticFromLogic supply the associativity, commutativity, and identity properties that the instance relies on.
proof idea
The declaration is a one-line reflexivity proof. It follows directly from the sub_eq_add_neg field inside the AddCommGroup instance, which itself reduces pointwise to rfl because negation is the identity map in characteristic 2.
why it matters
The result removes a notational obstacle when manipulating the F2Power group law, which the module uses to prove that exactly seven nonzero elements exist at D = 3. This count feeds the bijection to Booker's seven plot families in the companion paper and supports later constructions in NarrativeGeodesic and CubeBridge. It closes the algebraic simplification step required before the cardinality theorems can be stated cleanly.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.