conjugationChannel
plain-language theorem explainer
Defines the density-level conjugation channel on 8×8 complex matrices: ρ maps to U ρ U†. Anyone working the mediator-universality boundary cites it as the canonical per-update density map. The body is the standard three-factor matrix product; no unitarity is built into the definition.
Claim. For $8\times 8$ complex matrices $U$ and $\rho$, the conjugation channel is the map $\rho \mapsto U\,\rho\,U^{\dagger}$, where $U^{\dagger}$ denotes the conjugate transpose of $U$.
background
The ambient setting is the gravity quantum-channel layer on the eight-tick octave: states live in $\mathbb{C}^8$ (Signal8), and densities are $8\times 8$ complex matrices. The sibling pure-state density is the rank-one projector built from a vector $\psi$.
The module sits past the vector-level no-go (amplitude-linear, density-only, and nonzero cannot hold together on Signal8). Here the question is what algebra still allows at density level. The module doc states the positive half explicitly: for every fixed update $U$, the map $\rho \mapsto U\rho U^{\dagger}$ exists, reproduces amplitude dynamics on pure states, and is trace-preserving when $U$ is unitary.
Conjugate transpose is the usual Hilbert-space adjoint on matrices; the eight-dimensional index set is the T7 octave period $2^3$, not an arbitrary matrix size.
proof idea
Pure definition: the body is the matrix product $U * \rho * U^{\dagger}$. No lemmas, no tactics, no hypotheses. Downstream theorems unfold this abbreviation and simplify.
why it matters
This is the constructive witness for the positive half of the mediator-universality boundary. It feeds three local theorems: conjugation reproduces the amplitude update on pure densities (no unitarity needed); conjugation by a unitary is trace-preserving; and for every fixed $U$ there exists a density mediator $\Phi$ with $\Phi(\mathrm{density}(\psi)) = \mathrm{density}(U\psi)$.
Together those results pin the honesty note in the module: algebra alone does not forbid update-dependent density mediation. The matching no-go is only against one fixed map serving all unitary updates at once (identity versus a 0-1 swap already clash). Weaker readings (update-parameterized families, a single CP architecture) remain the MODEL premise. The construction lives on the eight-tick carrier forced at T7.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.