spacetime_parity_count
plain-language theorem explainer
There are exactly four spacetime ℤ₂ parities on the recognition ledger: charge, spatial parity (from D=3), tick reversal, and B−L. Anyone counting the nine independent ledger parities cites this decomposition. The proof is pure reflexivity (4=4), anchoring the combinatorial claim rather than deriving it.
Claim. The spacetime sector contributes exactly four independent $\mathbb{Z}_2$ parities: charge $C$, spatial parity $P$ (forced by $D=3$), tick reversal $T$, and baryon-minus-lepton $B-L$. Their count equals $4$. The $B-L$ factor is available because three spatial dimensions support nontrivial linking (Alexander duality).
background
The module NineParities formalizes the nine independent $\mathbb{Z}_2$ symmetries that flip under conjugation and tick reversal on the double-entry recognition ledger. They split into three sources: four spacetime parities, three color parities (SU(3) Cartan), and two generation parities (rank-2 mixing among three generations forced by the eight-tick octave).
Spacetime parities are $P_{cp}$, $P_{B-L}$, $P_Y$, and $P_T$. Spatial parity exists only because the forcing chain yields $D=3$ (T8). $B-L$ is nontrivial for the same dimensional reason: Alexander duality supplies linking in three-space. Tick reversal is the ledger time-orientation flip tied to the fundamental tick $\tau_0=1$ and the eight-tick phase structure.
Upstream landmarks include the eight-tick phases, the cost-projector forcing that pins the J-cost, and the T−1-to-T8 bridge that places $D=3$ and the octave period $2^3=8$.
proof idea
Term-mode reflexivity: the statement is literally $4=4$, closed by rfl. No lemmas are applied. The mathematical content lives entirely in the doc-comment decomposition (C + P + T + B−L), not in a nontrivial derivation.
why it matters
This declaration records the spacetime half of the nine-parity census that decodes Tesla's "magnificence of the 9" as an exact ledger count rather than numerology. Together with the color (3) and generation (2) counts it underwrites parity_count_eq_nine and the claim that all nine flip under tick reversal plus conjugation.
Framework landmarks: T7 (eight-tick octave) and T8 ($D=3$) justify why spatial parity and $B-L$ appear; the Recognition Composition Law and J-uniqueness sit upstream of the ledger structure these parities act on. No downstream theorems currently depend on this name (used_by is empty); it is a local bookkeeping anchor inside the parity trichotomy and source decomposition.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.