basisVector_nonzero
plain-language theorem explainer
Each standard basis vector in the nine-dimensional ℤ₂ parity space is distinct from the vacuum (zero) vector. Anyone building linear independence or spanning arguments for the ledger parities will cite this. The proof evaluates the assumed equality at the defining index and obtains 1 = 0 after unfolding.
Claim. For every parity index $i$ among the nine $\mathbb{Z}_2$ indices $\{P_{cp}, P_{B-L}, P_Y, P_T, P_C^{(1)}, P_C^{(2)}, P_C^{(3)}, P_\tau^{(1)}, P_\tau^{(2)}\}$, the standard basis vector $e_i$ (value $1$ at $i$ and $0$ elsewhere) is not equal to the vacuum parity vector $0$.
background
The module formalizes nine independent $\mathbb{Z}2$ parities on the recognition ledger under tick reversal and conjugation: four spacetime parities ($P{cp}$, $P_{B-L}$, $P_Y$, $P_T$), three color Cartan parities, and two generation-mixing parities. Their exact count is the content of Tesla's "magnificence of the 9" in this framework: not numerology, but the dimension of the parity space of the vacuum page.
A parity vector assigns a bit in $\mathbb{Z}_2$ to each of the nine indices. The vacuum parity is the zero assignment. The standard basis vector at index $i$ is the function that is $1$ only at $i$ and $0$ elsewhere. These are the elementary generators one needs before stating algebraic independence or a basis theorem for the parity space.
proof idea
Assume $e_i$ equals the vacuum vector. Apply function extensionality (congruence of application) at the coordinate $i$. Unfolding the definitions of the basis vector and the vacuum vector yields $1 = 0$ in $\mathbb{Z}_2$, a contradiction. The argument is a short term-mode contradiction with no external lemmas beyond definitional simplification.
why it matters
This is a basic non-degeneracy fact for the nine-parity ledger model: the coordinate axes are genuinely nonzero, so they can serve as generators when proving that the parity space is nine-dimensional and that the nine parities are independent over $\mathbb{Z}_2$. The module's key theorems (parity_count_eq_nine, parity_independence, vacuum vanishing, and flip under tick reversal) all sit on this linear-algebraic substrate.
In the broader Recognition Science chain, the nine $\mathbb{Z}_2$ symmetries constrain which ledger configurations remain admissible after conjugation and tick reversal. No downstream uses are wired yet in the graph, but the lemma is the natural first step toward any spanning or independence argument for the parity page.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.