swapMatrix
plain-language theorem explainer
The standard 0–1 transposition matrix on ℂ⁸, used as a concrete unitary witness against a single density-level mediator for every update. Anyone citing the density-level universality no-go needs this matrix (with the identity) as the clash pair. It is a one-line Mathlib wrapper: Matrix.swap on indices 0 and 1.
Claim. Let $S \in M_8(\mathbb{C})$ be the permutation matrix that swaps the standard basis vectors $e_0$ and $e_1$ and fixes $e_2,\ldots,e_7$. Equivalently, $S$ is the matrix of the transposition $(0\;1)$ acting on $\mathbb{C}^8$.
background
The ambient space is the eight-tick signal space $\mathbb{C}^8$ (indexed by $\mathrm{Fin},8$), the discrete carrier for the Recognition gravity quantum-channel analysis. Density operators are $8\times 8$ complex matrices; pure densities arise as outer products of amplitude vectors.
The module sits downstream of the vector-level no-go (amplitude-linear, density-only, and nonzero cannot hold together on Signal8). Here the question is weaker and sharper: at density level, conjugation $\rho \mapsto U\rho U^\dagger$ works for each fixed unitary $U$, but can one fixed map $\Phi$ implement every unitary update at once?
The 0–1 swap is the second unitary in the clash pair (with the identity). Sibling objects include the standard basis vectors $e_0,e_1$ and the index transposition used to build $S$.
proof idea
Pure definition: one-line application of Mathlib's Matrix.swap at indices $0$ and $1$ over $\mathbb{C}$. No proof obligations; unitarity and the action $S e_0 = e_1$ are discharged in the sibling lemmas that cite this def.
why it matters
This matrix is the concrete second unitary in the density-level universality no-go: no single fixed $\Phi$ can serve all unitary updates, because the identity and the 0–1 swap already disagree on one pure density. Downstream, swapMatrix_unitary records $S^\dagger S = I$, and swapMatrix_mulVec_basis0 records $S e_0 = e_1$; both feed no_universal_density_mediator.
In the Recognition gravity channel story this pins the quantifier-order reading of universality (one $\Phi$ for all $U$) as false, while leaving update-parameterized families and the MODEL premise untouched. The eight-dimensional carrier matches the eight-tick octave (T7) of the forcing chain; the construction itself is pure linear algebra on that carrier.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.