vacuum_parities_vanish
plain-language theorem explainer
Every one of the nine independent ledger parities evaluates to zero on the scalar vacuum page. Cite this when identifying the vacuum as the unique ℤ₂-even configuration (no charge, color, generation mixing, or tick asymmetry). The proof is a one-line unfold of the constant-zero vacuum parity vector.
Claim. For every parity index $p$ in the nine-element index set $\{P_{cp}, P_{B-L}, P_Y, P_T, P_C^{(1)}, P_C^{(2)}, P_C^{(3)}, P_\tau^{(1)}, P_\tau^{(2)}\}$, the vacuum parity assignment satisfies $v_{\mathrm{vac}}(p) = 0$.
background
The module formalizes nine independent $\mathbb{Z}2$ parities of the recognition double-entry ledger under tick reversal and conjugation. They split by origin as four spacetime parities ($P{cp}$, $P_{B-L}$, $P_Y$, $P_T$), three color parities from the SU(3) Cartan ($P_C^{(1..3)}$), and two generation-mixing parities ($P_\tau^{(1..2)}$). Tesla's "magnificence of the 9" is read here as this exact independent count.
ParityIndex is the inductive type enumerating those nine labels. A parity vector assigns a bit in $\mathbb{Z}_2$ to each index. The vacuum parity vector is defined pointwise as the zero function: every component is $0$. That is the scalar vacuum page of the ledger: no net charge, color, generation mixing, or tick asymmetry.
Upstream, the count theorem records that there are exactly nine indices; the flip theorem records that conjugation plus tick reversal negates every component. The present statement isolates the vacuum fixed point of that $\mathbb{Z}_2^9$ action.
proof idea
Term-mode one-liner. Unfold the definition of the vacuum parity vector (the constant function sending every parity index to $0$) and simplify. No case split on the nine constructors is required: the definition is already index-independent.
why it matters
This is item (2) of the module's master theorem nine_parities_master, which packages count, flip-under-tick-reversal, vacuum vanishing, the $4+3+2$ source decomposition, algebraic independence (span of $\mathbb{Z}_2^9$), and the $2^9=512$ configuration count. Without vacuum vanishing, the vacuum would not be the unique $\mathbb{Z}_2$-even fixed point of parity-preserving operations.
In the broader Recognition framework the nine parities constrain which ledger pages are physically admissible under double-entry balance. The vacuum page is the reference configuration against which charged, colored, and generation-asymmetric states are measured. The result is pure foundation bookkeeping: it does not itself force $D=3$, the eight-tick octave, or the $J$-cost, but it sits in the same ledger layer those forcing steps act on.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.