trace_densityOf
plain-language theorem explainer
For any eight-component complex signal, the trace of its pure-state density equals the sum of squared component moduli. Gravity quantum-channel work at the density-level mediator boundary cites this as the elementary pure-state normalization identity. The proof is a one-line simplification unfolding the outer-product density and the matrix trace.
Claim. For every eight-slot complex amplitude vector $\psi$, writing $\rho=|\psi\rangle\langle\psi|$ for the pure density with entries $\rho_{ij}=\psi_i\overline{\psi_j}$, one has $\operatorname{Tr}(\rho)=\sum_{k=0}^{7}|\psi_k|^2$.
background
The module treats the density-level boundary of mediator universality for gravity quantum channels on eight-slot signals. Upstream, the vector-level no-go already rules out a response that is simultaneously amplitude-linear, density-only, and nonzero. This file does not re-prove that; it records what algebra forces once one works with pure densities.
A pure density is the outer product of a Signal8 amplitude vector with itself: the $(i,j)$ entry is $\psi_i$ times the conjugate of $\psi_j$. The ambient dimension eight is the RS eight-tick octave (period $2^3$). Trace is the ordinary matrix trace over $\mathrm{Fin},8$.
The sibling pure-density constructor supplies $\rho=|\psi\rangle\langle\psi|$. The present identity states that $\operatorname{Tr}(\rho)$ equals the squared $\ell^2$ norm of $\psi$, i.e. the sum of squared amplitudes.
proof idea
One-line tactic proof: simplify after unfolding the pure-density constructor and the matrix-trace definition. The diagonal entries become $\psi_k\overline{\psi_k}$, and the trace collapses exactly to the finite sum over $\mathrm{Fin},8$ of those products.
why it matters
Bookkeeping lemma inside the mediator-universality-boundary development. The module's positive half shows that for each fixed unitary update $U$, the conjugation map $\rho\mapsto U\rho U^\dagger$ exists, reproduces amplitude dynamics on pure states, is phase-insensitive on pure densities, and is trace-preserving when $U$ is unitary. Trace preservation and pure-state reproduction both rest on the pure density having the correct trace (the squared amplitude norm).
The same module formalizes the density-level no-go as a quantifier-order fact: no single fixed map serves every unitary update at once (identity versus the $0$-$1$ swap already clash on one pure density). The module honesty note stresses this does not forbid update-dependent density mediation; weaker MODEL readings remain open. The dependency graph lists no downstream users yet, but neighboring results on conjugation channels and nonzero pure densities sit beside this identity. The eight-slot carrier is the RS eight-tick octave (T7).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.