Singleton Record Classicality

Abstract

Singleton environment-record classes leave exactly a diagonal classical algebra.

Theorem 1.1 (Singleton record classes give a classical fixed algebra).

$$\begin{gathered} \forall d,e:Nat,E:\mathrm{Fin}(d)\to \mathrm{Fin}(e)\to \mathbb{C}\Rightarrow (\forall i:\mathrm{Fin}(d),\sum _a\in \mathrm{Fin}(e)\Vert E(i,a){\Vert }^2=1\wedge \forall i,j:\mathrm{Fin}(d),i\ne j\Rightarrow \mathrm{recordGram}(E,i,j)\ne 1\Rightarrow \\ (\forall i,j:\mathrm{Fin}(d),\mathrm{recordGram}(E,i,j)=1\iff i=j)\wedge (\forall rho:\mathrm{Matrix}(\mathrm{Fin}(d),\mathrm{Fin}(d),\mathbb{C}),\mathrm{recordChannel}(E,rho)=rho\iff rho\in \mathrm{range}(\mathrm{diagonalAlgHom}(\mathbb{C})))\wedge (\forall p:\mathrm{Fin}(d)\to \mathbb{C},\mathrm{recordChannel}(E,\mathrm{diagonal}(p))=\mathrm{diagonal}(p)\wedge \mathrm{diagonalRangeEquiv}(d)(\mathrm{diagonal}(p))=p)\wedge (\forall x,y:\mathrm{range}(\mathrm{diagonalAlgHom}(\mathbb{C})),xy=yx)\wedge (\forall rho:\mathrm{Matrix}(\mathrm{Fin}(d),\mathrm{Fin}(d),\mathbb{C}),\mathrm{PosSemidef}(rho)\Rightarrow \mathrm{trace}(rho)=1\Rightarrow \mathrm{recordChannel}(E,rho)=rho\Rightarrow \exists q:\mathrm{Fin}(d)\to \mathbb{R},rho=\mathrm{diagonal}(q)\wedge \forall i:\mathrm{Fin}(d),0\le q(i)\wedge \sum _i\in \mathrm{Fin}(d)q(i)=1). \end{gathered}$$

Proof. Machine-checked in Lean as D5/S3/Quantum/FixedAlgebra/SingletonRecordClassicality.singleton_record_classicality (✓ std3). ∎

Source. Repository-derived.

Commentary.

For finite system and environment address sets, construct the record Gram overlap from normalized environment amplitudes and let the reduced channel multiply each matrix entry by that overlap. Assume unit overlap occurs only on the same address, so every record equivalence class is a singleton.

The fixed matrices are exactly the diagonal matrices. The canonical diagonal algebra map has a range isomorphic to the coordinate algebra of complex functions on the system addresses, and its coordinates are recovered by diagonal entries; this range is commutative and is the stable accessible algebra.

Finally, a positive trace-one fixed matrix has real nonnegative diagonal coordinates whose sum is one. Thus the observer state is exactly a probability vector.

References

• Truth anchor: D5/S3/Quantum/FixedAlgebra/SingletonRecordClassicality.singleton_record_classicality