Operational Readout Quotient Representation

Abstract

Operational state classes are canonically and affinely represented by realized readouts.

Theorem 1.1 (The operational quotient is canonically its readout range).

$$\begin{array}{c}\forall d:\mathrm{Type},\mathrm{Fintype}(d)\wedge \mathrm{DecidableEq}(d)\Rightarrow \\ \forall S:\mathrm{MatrixOperatorSystem}(d),\\ r_S:=\mathrm{operatorSystemReadout}(S),E_S:=\mathrm{quotientKerEquivRange}(r_S):\mathrm{Quotient}(\ker (r_S))\equiv \mathrm{range}(r_S),\\ \forall \rho :\mathrm{DensityState}(d),E_S(\mathrm{class}(\rho ))=\mathrm{rangePoint}(r_S(\rho ))\wedge \\ \forall EPrime:\mathrm{Quotient}(\ker (r_S))\equiv \mathrm{range}(r_S),\forall \rho :\mathrm{DensityState}(d),EPrime(\mathrm{class}(\rho ))=\mathrm{rangePoint}(r_S(\rho ))\Rightarrow EPrime=E_S\wedge \\ \forall t:\mathbb{R},\rho :\mathrm{DensityState}(d),\Sigma :\mathrm{DensityState}(d),0\le t\le 1\Rightarrow \\ \exists !{\rho }_t:\mathrm{DensityState}(d),\mathrm{matrix}({\rho }_t)=t\cdot \mathrm{matrix}(\rho )+1-t\cdot \mathrm{matrix}(\Sigma )\wedge \\ \mathrm{value}(E_S(\mathrm{class}({\rho }_t)))=t\cdot \mathrm{value}(E_S(\mathrm{class}(\rho )))+1-t\cdot \mathrm{value}(E_S(\mathrm{class}(\Sigma ))).\end{array}$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Completion/OperationalReadoutQuotientRepresentation.operational_readout_quotient_representation (✓ std3). ∎

Source. Repository-derived.

Commentary.

Density states are identified exactly when every effect in the chosen operator system has the same trace expectation.

The named kernel-range equivalence sends each state class to its realized readout and is uniquely determined by this rule.

Positive trace-one matrices are closed under binary mixtures. Trace linearity then shows that the canonical equivalence preserves every such convex combination pointwise.

References

• Truth anchor: D5/S3/Quantum/Completion/OperationalReadoutQuotientRepresentation.operational_readout_quotient_representation
• Dependency: D5/S3/Quantum/Fibers/FutureStatisticsEquivalence