Trace-Zero Hermitian Readout Fibers

Abstract

Real trace-zero Hermitian readout fibers equal residual and projection fibers.

Theorem 1.1 (Trace readout fibers are residual and projection fibers on the real carrier).

$$\begin{gathered} \forall d:\mathrm{Type},m:Nat,[\mathrm{Fintype}(d)],[\mathrm{Nonempty}(d)],[\mathrm{DecidableEq}(d)] \\ E:\mathrm{Fin}(m+1)\to \mathrm{Matrix}(d,d,\mathbb{C}),\rho ,\sigma :\mathrm{Matrix}(d,d,\mathbb{C}),\rho \mathrm{PosSemidef}\wedge \mathrm{trace}(\rho )=1,\sigma \mathrm{PosSemidef}\wedge \mathrm{trace}(\sigma )=1, \\ \forall i:\mathrm{Fin}(m+1),(E(i)\mathrm{PosSemidef}\wedge (1-E(i))\mathrm{PosSemidef})\Rightarrow \\ V=\mathrm{HermitianTraceZero}(d),V0(V,E)={\mathrm{span}}_{\mathbb{R}}(\mathrm{range}(\mathrm{centeredEffect}(E(i)))),R0(V,E)=V{0}^{\perp }, \\ ((\mathrm{finiteTraceReadout}(E,\rho )=\mathrm{finiteTraceReadout}(E,\sigma ))\iff (\forall i,\mathrm{Tr}((\rho -\sigma )E(i))=0))\wedge \\ ((\forall i,\mathrm{Tr}((\rho -\sigma )E(i))=0)\iff (X_{\rho }-X_{\sigma }\in R_0))\wedge \\ ((X_{\rho }-X_{\sigma }\in R_0)\iff (P_{V_0}(X_{\rho })=P_{V_0}(X_{\sigma }))). \end{gathered}$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Fibers/TraceZeroReadoutOrthogonalEquivalence.readout_fiber_orthogonal_equivalence (✓ std3). ∎

Source. Repository-derived.

Commentary.

The public carrier is the real subspace HermitianTraceZero(d) of complex d by d matrices that are Hermitian and trace zero. Raw effects and density matrices retain their source positivity and trace-one predicates; centered effects and centered states are constructed in this carrier.

Let V_0 be the real span of the centered effects and R_0 its orthogonal complement in HermitianTraceZero(d). Equality of the finite trace readouts is equivalent to every trace pairing being zero, to the centered-state difference lying in R_0, and to equal orthogonal projections onto V_0.

The frozen finite expectation-word residual theorem is applied on the real subtype. Matrix trace and complex-inner-product identities bridge its real pairing to the source’s complex trace equation.

References

• Truth anchor: D5/S3/Quantum/Fibers/TraceZeroReadoutOrthogonalEquivalence.readout_fiber_orthogonal_equivalence
• Dependency: D5/S3/Quantum/Fibers/ReadoutOrthogonalEquivalence