nine_parities_master
plain-language theorem explainer
The recognition ledger carries exactly nine independent ℤ₂ parities: they all flip under conjugation plus tick reversal, vanish on the scalar vacuum page, decompose as 4+3+2 (spacetime, color, generation), and are algebraically independent over ℤ₂. Anyone citing the nine-parity structure of the double-entry ledger packages this master statement. The proof is a term-mode conjunction of five already-proved component theorems.
Claim. There are exactly nine parity indices. For every parity assignment $v$ and every index $p$, the tick-reversal conjugate of $v$ at $p$ differs from $v(p)$. The vacuum parity assignment is identically zero. The count decomposes as $4+3+2=9$, and the standard basis vectors of the parity space are pairwise distinct, so the nine parities are algebraically independent over $\mathbb{Z}_2$ (configuration space size $2^9=512$).
background
This module formalizes the nine independent ℤ₂ parities that govern the double-entry recognition ledger under tick reversal and conjugation. The index type enumerates them by origin: four spacetime parities (charge-parity, baryon-minus-lepton, hypercharge, tick reversal), three color parities from the SU(3) Cartan generators, and two generation-mixing parities from the rank-2 three-generation structure. A parity vector is an assignment of each index to a value in ℤ₂.
The fundamental time quantum is one tick (τ₀ = 1 in RS-native units); one octave is eight ticks. Tick-reversal conjugation flips every parity bit. The vacuum page is the zero assignment. Standard basis vectors place a single 1 at a chosen index and 0 elsewhere; pairwise distinctness of those vectors is the algebraic independence statement over ℤ₂.
Upstream component results already establish the card count by decision, the universal flip under tick-reversal conjugation (because adding 1 in ℤ₂ never fixes a bit), vacuum vanishing, the 4+3+2 source split, and basis independence.
proof idea
Term-mode packaging: the goal is a five-fold conjunction, discharged by exact ⟨..., ..., ..., ..., ...⟩ on the five component theorems already proved in-module. Count is parity_count_eq_nine (Fintype card of the inductive index type equals 9, by decide). Flip is parities_flip_under_tick_reversal (tick-reversal conjugate differs pointwise because $x+1 \neq x$ in ℤ₂). Vacuum vanishing is vacuum_parities_vanish. Decomposition is the arithmetic identity source_decomposition ($4+3+2=9$). Independence is parity_independence, which reduces to pairwise distinctness of the standard basis vectors. No new algebra is done here.
why it matters
This is the master packaging for the nine ℤ₂ parities of the recognition ledger. The module doc ties the count to Tesla's "magnificence of the 9": not numerology, but the exact number of independent ℤ₂ symmetries constraining the vacuum page and admissible configurations. Theory-spec lines cited in the module (1189, 3332–3333) state that nine independent parities flip under conjugation and tick reversal.
The 4+3+2 split links spacetime structure (including tick reversal), color Cartan signs, and generation rank to a single ledger object. Configuration space size $2^9=512$ is the discrete state count those parities generate. In the broader forcing chain, tick structure and the eight-tick octave (T7) sit nearby; the spacetime side of the split is the natural contact with D=3 (T8) and ledger forcing imported by this module.
No downstream used_by edges are recorded yet; the declaration is the closed summary other foundation developments would cite when they need the full parity package rather than a single facet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.