basis1
plain-language theorem explainer
The second computational-basis pure state on the eight-tick signal space: the unit vector with a 1 at index 1 and zeros elsewhere. Downstream density and swap lemmas use it as the image of the 0-1 swap on the first basis vector, and as one of two pure densities that any universal density mediator would have to treat inconsistently. The body is the standard Pi.single constructor.
Claim. Let $e_1 \in \mathbb{C}^8$ be the standard basis vector with a $1$ in coordinate $1$ and $0$ in every other coordinate (indices in $\mathrm{Fin}\,8$).
background
The ambient space is Signal8, the eight-component complex amplitude vector tied to the Recognition eight-tick octave (period $2^3$). Pure states are ordinary vectors; the module lifts them to density matrices via the outer-product map densityOf.
This file sits after the vector-level no-go (amplitude-linear, density-only, and nonzero cannot hold together). Here the question is density-level mediation: for each fixed unitary update $U$, the conjugation channel $\rho \mapsto U\rho U^H$ exists and is well-behaved, but no single fixed map can implement every unitary update at once.
The pair of basis vectors $e_0$ and $e_1$ is the minimal witness. The 0-1 swap unitary sends $e_0$ to $e_1$, so any candidate universal density map is forced to send $\mathrm{densityOf}(e_0)$ to $\mathrm{densityOf}(e_1)$ under that update and to itself under the identity, which is impossible once those two densities are distinct.
proof idea
Definition, not a proof. The vector is constructed as Pi.single (1 : Fin 8) (1 : Complex), the pointwise indicator of index 1 with value $1\in\mathbb{C}$. No lemmas are applied.
why it matters
Local scaffolding for the density-level universality boundary. It is the codomain of swapMatrix_mulVec_basis0 (swap sends $e_0$ to $e_1$), one side of densityOf_basis0_ne_densityOf_basis1, and thereby part of the concrete clash inside no_universal_density_mediator: no single fixed density map $\Phi$ can reproduce every unitary conjugation.
In the Recognition gravity channel story this pins the strong reading of universality (one $\Phi$ for all $U$) as false, while leaving update-dependent conjugation channels intact. It does not touch the vector-level no-go or the MODEL premise of parameterized families; it only makes the quantifier-order distinction kernel-checked on the eight-tick space.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.