basis0
plain-language theorem explainer
The computational basis vector on the eight-mode signal space with unit amplitude only at index 0. It is the pure-state witness used to separate the identity update from the 0–1 swap at density level. The definition is the standard single-support embedding of 1 into ℂ⁸.
Claim. Let $\lvert 0\rangle \in \mathbb{C}^{8}$ be the pure signal with amplitude $1$ in the zeroth coordinate and $0$ in every other coordinate: $(\lvert 0\rangle)_{k} = \delta_{k0}$.
background
This module sits in the gravity quantum-channel layer. The ambient space is Signal8, i.e. maps Fin 8 → ℂ, the eight-tick octave forced by the Recognition chain (T7). Pure states are turned into density matrices by the outer-product map densityOf.
The module’s positive half shows that for every fixed update matrix $U$ there is a density-level channel $\rho \mapsto U\rho U^{\dagger}$ that reproduces amplitude dynamics on pure states. The negative half asks whether one fixed density map can serve every unitary $U$ at once.
The two pure vectors with support only at modes 0 and 1 are the minimal witnesses for that quantifier-order clash: identity leaves $\lvert 0\rangle$ fixed, while the 0–1 swap sends it to $\lvert 1\rangle$, and those pure densities are unequal.
proof idea
One-line definition: the pointwise single-support function that places the complex unit at index $0\in\mathrm{Fin},8$ and zero elsewhere (Pi.single). No proof obligations.
why it matters
Supplies the input pure state for three local results: the swap action lemma (swapMatrix.mulVec basis0 = basis1), the pure-density separation densityOf basis0 ≠ densityOf basis1, and ultimately the density-level no-go no_universal_density_mediator.
That no-go makes precise the strongest reading of universality (one fixed $\Phi$ implementing every unitary update). It does not forbid update-dependent mediation; the positive half of the module constructs such a mediator for each fixed $U$. In the Recognition gravity story this pins the boundary between what algebra alone rules out and what remains a model premise for a classical density mediator of gravity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.