isSpacetimeParity
plain-language theorem explainer
Predicate marking which of the nine ledger ℤ₂ parities are spacetime-origin: charge-parity, B−L, hypercharge, and tick reversal (exactly four). Anyone partitioning the nine-parity set into spacetime/color/generation sources cites it. Pure case definition on the parity index; no proof content.
Claim. A parity index $p$ is a spacetime parity precisely when $p \in \{P_{cp},\, P_{B-L},\, P_Y,\, P_T\}$; otherwise the predicate is false.
background
The module formalizes nine independent ℤ₂ parities of the recognition ledger under tick reversal and conjugation: ${P_{cp}, P_{B-L}, P_Y, P_T, P_C^{(1)}, P_C^{(2)}, P_C^{(3)}, P_\tau^{(1)}, P_\tau^{(2)}}$. They arise from three sources: four spacetime, three color (SU(3) Cartan), and two generation (rank-2 mixing).
ParityIndex is the inductive type enumerating those nine labels. Spacetime members are charge-parity, baryon-minus-lepton parity, hypercharge parity, and tick-reversal parity. The remaining five are color or generation. Tesla's "magnificence of the 9" is read here as this exact independent count constraining the vacuum page of the double-entry ledger.
proof idea
Definition by exhaustive pattern match on ParityIndex: the four constructors $P_{cp}$, $P_{B-L}$, $P_Y$, $P_T$ map to True; every other constructor maps to False. No lemmas, tactics, or algebraic reduction.
why it matters
Supplies one leg of the source trichotomy. Downstream, parity_trichotomy states every parity belongs to exactly one of spacetime, color, or generation, and discharges by cases plus simp on this predicate together with the color and generation siblings.
That partition underwrites the module's count theorems (parity_count_eq_nine) and the claim that all nine flip under conjugation plus tick reversal. In the broader forcing picture it organizes the discrete ℤ₂ data on the ledger vacuum page; it does not itself force $D=3$ or the eight-tick octave, but it is the bookkeeping layer those continuum results sit on.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.