basisVector
plain-language theorem explainer
Defines the standard basis vectors on the nine-dimensional parity space over ℤ₂: eᵢ equals 1 at index i and 0 elsewhere. Anyone proving algebraic independence of the ledger parities, or counting the 2⁹ configuration space, cites this. The body is the characteristic function of a single ParityIndex.
Claim. For each parity index $i$ among the nine $\mathbb{Z}_2$ labels $\{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 basis vector $e_i$ is the map sending $i$ to $1 \in \mathbb{Z}/2\mathbb{Z}$ and every other index to $0$.
background
The NineParities module formalizes the nine independent ℤ₂ symmetries of the recognition double-entry ledger under tick reversal and conjugation. They split as four spacetime parities (charge-parity, B−L, hypercharge, tick), three color Cartan sign flips, and two generation-mixing signs.
A parity index is one of those nine labels. A parity vector is any assignment of values in ℤ/2ℤ to the nine indices, i.e. an element of (ℤ/2ℤ)⁹. The zero vector is the vacuum page of the ledger.
These basis vectors are the standard Kronecker generators of that function space; they are the raw material for the independence and master-count theorems later in the module.
proof idea
Pure definition, not a theorem. The body is the pointwise characteristic function: evaluate at the target index to 1, elsewhere to 0 in ZMod 2. No lemmas are applied.
why it matters
This is the generator set for the parity space. Downstream, basisVector_nonzero shows each eᵢ differs from the vacuum page; basisVectors_distinct shows distinct indices give distinct vectors; parity_independence packages that into algebraic independence over ℤ₂; and nine_parities_master cites the whole package as the claim that the ledger carries exactly nine independent ℤ₂ parities spanning a 2⁹ = 512-state configuration space.
In the Recognition framework this is the concrete linear-algebra backbone of Tesla's "magnificence of the 9": the count is forced by spacetime + color Cartan + generation rank, not numerology. It sits under the ledger-forcing and dimension-forcing imports that pin D = 3 and the eight-tick structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.