vacuum_hamming_weight
plain-language theorem explainer
The vacuum parity vector on the recognition ledger has Hamming weight zero: every one of the nine independent ℤ₂ parities vanishes. Anyone working the nine-parity ledger, vacuum page, or tick-reversal conjugation will cite this as the baseline. The proof is a one-line simplification that unfolds the weight and the constant-zero vacuum assignment.
Claim. The Hamming weight of the vacuum parity vector equals $0$: if $v$ assigns $0$ to every parity index among the nine independent $\mathbb{Z}_2$ parities, then the number of nonzero coordinates of $v$ is zero.
background
The module formalizes nine independent ℤ₂ parities of the double-entry recognition ledger under tick reversal and conjugation: four spacetime parities (charge-parity, $B-L$, hypercharge, tick), three color Cartan sign flips, and two generation-mixing signs. Their exact count is the content of Tesla's "magnificence of the 9" in this framework: not numerology, but the dimension of the parity space that constrains admissible ledger pages.
A parity vector assigns an element of ℤ₂ to each of the nine indices. The vacuum parity vector is the constant-zero assignment (the scalar vacuum page). Hamming weight counts how many coordinates are nonzero; it is the cardinality of the set of parity indices where the vector differs from zero. Upstream, the same weight notion appears for finite-dimensional $\mathbb{F}_2$-power vectors as the number of true coordinates.
proof idea
One-line tactic proof: simp unfolds the local Hamming-weight definition (cardinality of indices with nonzero value) and the vacuum parity vector (the constant map sending every parity index to $0$). After unfolding, the filter is empty, so the card is $0$. No external lemmas are required beyond definitional reduction.
why it matters
This pins the vacuum baseline for the nine-parity story: the scalar vacuum page carries no parity charge. The module's key theorems include exact count nine, flip of all nine under conjugation plus tick reversal, vanishing of vacuum parities, and algebraic independence over ℤ₂. Weight zero for vacuum is the quantitative form of vacuum vanishing and the reference point against which excited or tick-reversed pages are measured (the sibling note that tick-reversed vacuum has weight 9 is the complementary extreme).
In the broader Recognition Science ledger, these parities decide which configurations keep double-entry balance. The result sits in Foundation alongside dimension and ledger forcing; it does not itself invoke the T0–T8 chain, RCL, or the mass ladder, but it supplies the discrete parity bookkeeping those layers assume when they talk about vacuum pages and conjugation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.