sub_eq_add
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.
claimFor 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 in Recognition Science
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.
scope and limits
- Does not prove the AddCommGroup axioms themselves.
- Does not extend to groups of odd characteristic.
- Does not compute concrete element tables for any fixed D.
- Does not address non-abelian or infinite-dimensional analogues.
formal statement (Lean)
83@[simp] theorem sub_eq_add (u v : F2Power D) : u - v = u + v := rfl
proof body
Tactic-mode proof.
84
85instance : AddCommGroup (F2Power D) where
86 add := (· + ·)
87 zero := 0
88 neg := Neg.neg
89 add_assoc u v w := by
90 funext i
91 show xor (xor (u i) (v i)) (w i) = xor (u i) (xor (v i) (w i))
92 cases u i <;> cases v i <;> cases w i <;> rfl
93 zero_add v := by
94 funext i
95 show xor false (v i) = v i
96 cases v i <;> rfl
97 add_zero v := by
98 funext i
99 show xor (v i) false = v i
100 cases v i <;> rfl
101 neg_add_cancel v := by
102 funext i
103 show xor (v i) (v i) = false
104 cases v i <;> rfl
105 add_comm u v := by
106 funext i
107 show xor (u i) (v i) = xor (v i) (u i)
108 cases u i <;> cases v i <;> rfl
109 nsmul := nsmulRec
110 zsmul := zsmulRec
111 sub_eq_add_neg u v := by funext i; rfl
112