Computational-Basis Kernel Preservation

Abstract

Basis fiber projectors preserve the deterministic readout kernel.

Theorem 1.1 (Fiber projectors retain exactly the deterministic kernel).

$$\begin{array}{c}\forall X:\mathrm{Type},O:\mathrm{Type},\\ [\mathrm{Fintype}(X)],[\mathrm{DecidableEq}(X)],[\mathrm{DecidableEq}(O)],\\ q:X\to O,x:X,y:X,\\ \mathrm{let}(\rho :X\to \mathrm{Matrix}(X,X,\mathbb{C}),\forall z:X,\rho (z)=\mathrm{basisProjector}(z),\\ P:O\to \mathrm{Matrix}(X,X,\mathbb{C}),\forall o:O,P(o)=\sum _{z\in X,q(z)=o}\mathrm{basisProjector}(z))[\forall o:O,\mathrm{Tr}(\mathrm{mul}(\rho (x),P(o)))=\mathrm{indicator}(q(x)=o)]\wedge \\ [q(x)=q(y)⟺\forall o:O,\mathrm{Tr}(\mathrm{mul}(\rho (x),P(o)))=\mathrm{Tr}(\mathrm{mul}(\rho (y),P(o)))].\end{array}$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Measurements/ComputationalBasisKernelPreservation.computational_basis_kernel_preservation (✓ std3). ∎

Source. Repository-derived.

Commentary.

Let X be a finite state type and O an outcome type with decidable equality. The density matrix rho of a state is the canonical coordinate rank-one projector.

For each outcome, its projector is constructed as the finite sum of coordinate projectors over the corresponding q-fiber. The trace pairing with rho is therefore the fiber indicator.

Equality of every outcome probability follows from equal q-values. Conversely, evaluating the common signature at q(x) forces the two q-values to agree.

References

• Truth anchor: D5/S3/Quantum/Measurements/ComputationalBasisKernelPreservation.computational_basis_kernel_preservation
• Dependency: D5/S3/Quantum/Decoherence/ProjectedUnistochasticDynamics