add_self
Every vector in the elementary abelian 2-group of rank D is its own additive inverse under pointwise XOR. Authors of results on plot cancellation and one-dimensional subspaces invoke the identity to replace cancellation with equality. The argument applies function extensionality followed by exhaustive case analysis on each Boolean coordinate.
claimLet $V$ be the set of maps from a finite set of cardinality $D$ to the two-element set, equipped with pointwise addition given by exclusive-or. Then $v + v = 0$ for every $v$ in $V$.
background
F2Power D is defined as the type Fin D → Bool. Pointwise XOR supplies the addition that turns this set into an elementary abelian 2-group of rank D. The module proves the full AddCommGroup instance together with cardinality and Hamming-weight facts that are used downstream for the seven nonzero elements when D equals 3.
proof idea
Function extensionality reduces the claim to pointwise equality. For each index i the Boolean expression xor (v i) (v i) is shown equal to false by case split on the value of v i, with both branches discharging by reflexivity.
why it matters in Recognition Science
The identity is applied inside plot_composition_cancels_iff to obtain the equivalence between XOR cancellation and plot equality, and inside oneDimSubspace_closed to confirm closure of the one-dimensional subspaces generated by nonzero elements. It thereby supplies the algebraic step that converts the asserted count of seven Booker plot families into a theorem, as required by the companion paper Seven_Plots_Three_Dimensions.tex.
scope and limits
- Does not prove the remaining group axioms.
- Does not compute cardinalities or weight distributions.
- Does not treat structures outside characteristic two.
- Does not address infinite-dimensional or continuous analogues.
Lean usage
example (v : F2Power 3) : v + v = 0 := add_self vformal statement (Lean)
113@[simp] theorem add_self (v : F2Power D) : v + v = 0 := by
proof body
Term-mode proof.
114 funext i
115 show xor (v i) (v i) = false
116 cases v i <;> rfl
117
118/-! ## Cardinality -/
119
120/-- `F2Power D` has `2 ^ D` elements. -/