densityOf_single_ne_zero
plain-language theorem explainer
The pure-state density matrix of the first eight-tick basis vector is nonzero. Anyone building density-level mediator or conjugation-channel arguments that need a nontrivial pure input cites this. The proof is a one-entry contradiction: the (0,0) matrix entry equals 1.
Claim. Let $e_0 \in \mathbb{C}^8$ be the first standard basis vector (value $1$ at index $0$, zero elsewhere). Its pure-state density $|e_0\rangle\langle e_0|$ is not the zero $8\times 8$ complex matrix.
background
This module sits at the density-level boundary of the gravity quantum-channel story. The vector-level no-go (amplitude-linear, density-only, and nonzero cannot hold together on Signal8) lives upstream; here the focus is what algebra does and does not force once one passes to densities.
densityOf builds the pure-state density matrix of an eight-component complex amplitude vector $\psi$: the $(i,j)$ entry is $\psi_i \overline{\psi_j}$. The eight-tick index set $\mathrm{Fin},8$ is the RS octave period $2^3$ (forcing chain T7). The input here is the Kronecker spike at slot $0$ with value $1$, i.e. the first computational basis vector.
The module's positive half shows that for each fixed unitary update $U$ the conjugation channel $\rho \mapsto U\rho U^H$ exists, reproduces amplitude dynamics on pure states, is phase-insensitive on pure densities, and is trace-preserving. Nondegeneracy of a reference pure density is the elementary substrate for those statements and for the density-level universality clash.
proof idea
Proof by contradiction on matrix equality. Assume densityOf of the spike equals the zero matrix. Apply function extensionality twice to read the $(0,0)$ entry. Unfolding the definition gives $1 \cdot \overline{1} = 0$, which simp reduces to the false equality $1 = 0$. No external lemmas beyond the definition of densityOf are required.
why it matters
In the Recognition gravity channel development this is a kernel-checked nondegeneracy fact: the pure density used as the witness input for conjugation-channel and mediator-universality arguments is actually nonzero. The module doc stresses honesty of strength: algebra does not forbid update-dependent density mediation; it only kills the strongest reading (one fixed map for every unitary at once), witnessed by identity versus the $0$-$1$ swap on a single pure density.
This lemma underwrites that witness by guaranteeing the reference pure density is nontrivial. It does not itself state the no-go or the positive conjugation theorems (siblings such as conjugationChannel_reproduces, conjugationChannel_trace_preserving, per_update_density_mediator_exists). No downstream consumers are recorded yet; it is local infrastructure inside the mediator-universality boundary file. Framework landmarks touched only indirectly: the eight-tick carrier (T7) and the density-level reading of recognition updates.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.