basisVectors_distinct
plain-language theorem explainer
Distinct parity indices yield distinct standard basis vectors in the nine-dimensional ℤ₂ parity space of the recognition ledger. Anyone establishing algebraic independence of the nine ledger parities cites this fact. The argument evaluates both vectors at the first index and reads off the Kronecker definition, giving the contradiction 1 = 0.
Claim. Let $i$ and $j$ be indices among the nine ledger parities (spacetime, color, and generation). If $i \neq j$, then the standard basis vectors $e_i$ and $e_j$ in the $\mathbb{Z}_2^9$ parity space are unequal: $e_i \neq e_j$.
background
The module formalizes nine independent $\mathbb{Z}2$ parities of the recognition ledger under tick reversal and conjugation: four spacetime parities ($P{cp}$, $P_{B-L}$, $P_Y$, $P_T$), three color parities from the SU(3) Cartan, and two generation parities. The index type ParityIndex is the inductive enumeration of these nine labels.
A parity vector is a map from indices to $\mathbb{Z}_2$. The standard basis vector at a target index is the Kronecker function: value $1$ at that index and $0$ elsewhere. Pairwise distinctness of these nine vectors is the elementary linear-algebra step toward a basis of the full $\mathbb{Z}_2^9$ space.
The module overview ties the count nine to Tesla's "magnificence of the 9" as the exact independent parity count constraining the vacuum page, not numerology.
proof idea
Short contradiction proof. Assume $e_i = e_j$ as functions. Apply function congruence at the point $i$ to obtain $e_i(i) = e_j(i)$. Unfold the basis definition: the left side is $1$ and, because $i \neq j$, the right side is $0$. Simplification yields the absurd equality $1 = 0$.
why it matters
This is the pointwise engine behind parity_independence, which packages the same statement as a universal quantifier and is listed among the module's key theorems: the nine basis parity vectors are pairwise distinct and form a basis for $\mathbb{Z}_2^9$, so the nine parities are algebraically independent over $\mathbb{Z}_2$.
In the Recognition framework the independence claim underwrites the ledger's double-entry constraints: admissible configurations must respect all nine sign flips under conjugation and tick reversal. It sits beside parity_count_eq_nine and the flip-under-tick-reversal theorems that decode the count nine as structural rather than decorative. Downstream material on the $D = 3$ connection builds on this parity space once independence is secured.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.