parity_space_dimension
plain-language theorem explainer
The finite type of ledger parity indices has cardinality exactly 9, so the independent ℤ₂ parities form a 9-dimensional space over the two-element field. Anyone constraining the vacuum page under tick reversal or conjugation cites this count. The proof is a one-line wrapper of the decidable enumeration of the inductive index type.
Claim. The set of independent parity indices has cardinality $9$. Equivalently, the parity space of the recognition ledger is $9$-dimensional over $\mathbb{Z}_2$.
background
The NineParities module counts the independent ℤ₂ symmetries that govern the double-entry recognition ledger under tick reversal and conjugation. Module overview lists nine named generators: four spacetime (charge-parity, $B-L$, hypercharge, tick), three color (SU(3) Cartan sign flips), and two generation-mixing signs.
ParityIndex is the inductive type with exactly those nine constructors. Its finite cardinality is the dimension of the free $\mathbb{Z}_2$-vector space of parity assignments on a ledger page. Upstream, parity_count_eq_nine already states the same equality and proves it by decide on the inductive type.
The local setting is pure foundation bookkeeping: no dynamics yet, only the discrete symmetry count that later filters admissible vacuum configurations.
proof idea
One-line term wrapper: the goal Fintype.card ParityIndex = 9 is discharged by applying the sibling theorem parity_count_eq_nine, which itself is a decide proof on the finite inductive type. No further rewriting or case analysis appears here.
why it matters
This declaration is the named bridge from the raw inductive count to the geometric slogan in the doc-comment: the nine parities span a 9-dimensional ℤ₂ vector space. It underwrites the module's decoding of Tesla's "magnificence of the 9" as an exact ledger symmetry count rather than numerology (theory spec lines 1189, 3332-3333).
Sibling results that rely on the same count include the 4+3+2 source decomposition, the trichotomy into spacetime/color/generation classes, and the theorem that all nine flip under conjugation plus tick reversal. In the broader Recognition chain the count sits downstream of ledger forcing and dimension forcing imports; it does not itself invoke T5-T8, but supplies the discrete symmetry dimension that later vacuum-page and source-balance arguments consume. No downstream theorems currently depend on this alias specifically (used_by is empty); the value is naming and documentation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.