axis123_weight
The theorem states that the all-true vector in the rank-3 elementary abelian 2-group has Hamming weight exactly 3. Researchers counting the 1+3+3+1 weight classes in (Z/2)^3 cite it to anchor the bijection from nonzero vectors to 1-dimensional subspaces. The proof is a one-line wrapper that unfolds the two definitions and invokes a decision procedure.
claimLet $v = (1,1,1) : (F_2)^3$. The Hamming weight of $v$, defined as the cardinality of the set of coordinates equal to true, equals 3.
background
F2Power D is defined as the type Fin D → Bool equipped with pointwise XOR as the group operation, yielding the elementary abelian 2-group of rank D. Hamming weight of a vector v is the cardinality of the Finset of indices i where v i equals true. axis123 is the constant-true vector in dimension 3, described in its definition as the unique weight-3 vector. The module establishes the full weight distribution at D=3 as the partition 1+3+3+1 and the bijection from the 7 nonzero vectors to the 7 one-dimensional subspaces.
proof idea
The proof is a one-line wrapper that unfolds hammingWeight and axis123, then applies the decide tactic to confirm the resulting numerical equality.
why it matters in Recognition Science
This theorem supplies the weight-three term in the 1+3+3+1 decomposition required for the subgroup count in the F2Power module. The module document states that the count of 7 for Booker's basic plot families is proved here rather than asserted, enabling downstream chaining in Aesthetics.NarrativeGeodesic and Patterns.TwoToTheDMinusOne. It directly supports the combinatorial step from (Z/2)^3 to the seven 1-dimensional subspaces used in the companion paper Seven_Plots_Three_Dimensions.tex.
scope and limits
- Does not compute Hamming weights for vectors outside dimension 3.
- Does not address the full group law or addition table.
- Does not derive the weight distribution for general D.
- Does not connect the weight to any physical or Recognition-Science quantity.
formal statement (Lean)
227theorem axis123_weight : hammingWeight axis123 = 3 := by
proof body
Term-mode proof.
228 unfold hammingWeight axis123
229 decide
230
231/-! ## Subgroup count
232
233Every non-zero `v : F2Power D` generates the 1-dimensional subspace
234`{0, v}` (closed under XOR because `v + v = 0`). The map
235`v ↦ {0, v}` from non-zero vectors to 1-dimensional subspaces is a
236bijection: every 1-dimensional `F2`-subspace consists of exactly two
237elements (`0` and a single non-zero generator), and the generator is
238unique. -/
239
240/-- The 1-dimensional subspace generated by a non-zero `v`. -/