Trace-Zero Hermitian Readout Fibers

Abstract

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

Lemma 1.1 (Removing the scalar trace component gives a trace-zero Hermitian matrix).

$$\forall (d:Type\ast ),[\mathrm{Fintype}(d)][\mathrm{Nonempty}(d)][\mathrm{DecidableEq}(d)]\forall (E:\mathrm{Matrix}(d,d,\mathbb{C})),\mathrm{IsHermitian}(E)\Rightarrow (\mathrm{IsHermitian}((E-\mathrm{smul}(\frac{\mathrm{trace}(E)}{(\mathrm{card}(d):\mathbb{C})},(1:\mathrm{Matrix}(d,d,\mathbb{C})))))\wedge \mathrm{trace}((E-\mathrm{smul}(\frac{\mathrm{trace}(E)}{(\mathrm{card}(d):\mathbb{C})},(1:\mathrm{Matrix}(d,d,\mathbb{C})))))=0)$$

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

Source. Repository-derived.

Commentary.

For a Hermitian matrix on a nonempty finite index type, subtracting its trace divided by the dimension times the identity preserves Hermiticity and makes the trace zero. These two conditions are precisely membership in the real trace-zero Hermitian subspace. The formula expands both that membership and the centered matrix.

Theorem 1.2 (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.centered_effect_mem
• Truth anchor: D5/S3/Quantum/Fibers/TraceZeroReadoutOrthogonalEquivalence.readout_fiber_orthogonal_equivalence
• Dependency: D5/S3/Quantum/Fibers/ReadoutOrthogonalEquivalence