hammingWeight
plain-language theorem explainer
Hamming weight on a nine-component parity vector counts how many of the independent ℤ₂ ledger parities are nonzero. Anyone working the nine-parity vacuum page, tick-reversal conjugation, or F₂-power axis weights cites it as the standard sparsity measure. The definition is a direct Finset cardinality of the support over the finite parity index.
Claim. For a parity vector $v$, i.e. a map from the nine parity indices to $\mathbb{Z}/2\mathbb{Z}$, the Hamming weight is $\mathrm{wt}(v) := \#\{p : v(p) \neq 0\}$.
background
The NineParities module fixes the nine independent ℤ₂ symmetries of the recognition ledger under tick reversal and conjugation: four spacetime parities (CP, B−L, hypercharge, tick), three color Cartan sign flips, and two generation-mixing signs. A parity vector assigns a value in ℤ₂ to each of these nine indices; the zero vector is the vacuum page.
Hamming weight is the usual coding-theory count of nonzero coordinates. The same pattern appears for F₂-power vectors (coordinates equal to true) and for eight-vertex holographic cells (set vertex bits). Here the ambient space is exactly the nine-dimensional parity assignment space, so weight ranges in ${0,\ldots,9}$ and vanishes only on the vacuum assignment.
proof idea
Definitional, not a proof. Filter the finite universe of parity indices to those $p$ with $v(p)\neq 0$, then take Finset cardinality. Noncomputable only because the ambient Finset machinery is marked that way; the set is finite and decidable.
why it matters
Weight is the basic numerical invariant on the nine-parity space. Downstream F₂-power results use the same notion to pin axis weights (single axes weight 1, the triple axis weight 3) and to count the unique weight-zero vector. In the ledger story it separates the vacuum page (all parities off) from excited configurations that flip under conjugation and tick reversal, tying directly to the module claim that Tesla’s “9” is the exact independent parity count rather than numerology. It does not itself force dimension or the J-cost; it only measures support inside the already-forced nine-parity package.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.