axis3_weight
plain-language theorem explainer
axis3_weight establishes that the third standard basis vector in F_2^3 has Hamming weight exactly 1. Researchers partitioning the seven nonzero elements of F_2^3 by weight classes cite it when building the 1+3+3+1 decomposition. The argument is a one-line wrapper that unfolds the weight definition and decides the equality by direct computation.
Claim. Let $v = (0,0,1) ∈ (ℤ/2ℤ)^3$. The Hamming weight of $v$, defined as the number of coordinates equal to 1, equals 1.
background
F2Power D is the type Fin D → Bool equipped with pointwise XOR, forming the elementary abelian 2-group of rank D. Its cardinality is 2^D, with exactly 2^D - 1 nonzero elements. Hamming weight of a vector v counts the positions where the coordinate is true (i.e., 1). The vector axis3 is defined as the function that is true only at the third coordinate: ![false, false, true]. The module proves the weight decomposition 1+3+3+1 for D=3 as the combinatorial basis for the seven nonzero vectors and their one-dimensional subgroups.
proof idea
The proof unfolds hammingWeight and axis3 to obtain the concrete Finset cardinality expression, then applies the decide tactic to verify the resulting equality by exhaustive computation over the three coordinates.
why it matters
This lemma supplies one of the three weight-1 vectors required for the card_weight_one_three count in the same module, which in turn feeds the subgroup enumeration used by Aesthetics.NarrativeGeodesic. It closes the D=3 case of the forcing chain (T7 eight-tick octave, T8 spatial dimensions) by replacing an asserted count of seven with a proved partition. No open scaffolding remains in this module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.