Finite Operator-System Stability

Abstract

Finite operator-system stability at one step persists at every later step.

Theorem 1.1 (One stable operator-system step is permanently stable).

$$\begin{array}{c}\forall d,\mathrm{Finite}\left(d\right),\\ H:\mathrm{CompletelyPositiveMap}\left(\mathrm{Matrix}\left(d,d,\mathbb{C}\right),\mathrm{Matrix}\left(d,d,\mathbb{C}\right)\right),H(I)=I,\\ S_0:\mathrm{OperatorSystem}\left(\mathrm{Hermitian}\left(\mathrm{Matrix}\left(d,d,\mathbb{C}\right)\right)\right),m\in \mathbb{N},\\ \mathrm{predictionTower}\left(H,S_0,m\right)=\mathrm{predictionTower}\left(H,S_0,m+1\right)\Rightarrow \\ \forall r\in \mathbb{N},\mathrm{predictionTower}\left(H,S_0,m+r\right)=\mathrm{predictionTower}\left(H,S_0,m\right).\end{array}$$

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

Source. Repository-derived.

Commentary.

The finite carrier is the full real self-adjoint part of a complex matrix algebra. The initial operator system and prediction tower are the canonical objects supplied by the operator-system tower family.

The Heisenberg action is a unital completely positive map. Each tower step joins the current system with its image under that map, so the tower is constructed from the source channel and initial accessible system.

The imported permanent-stability theorem applies directly to equality of stages m and m plus one, yielding equality of every stage m plus r with stage m.

References

• Truth anchor: D5/S3/Quantum/Fibers/FiniteOperatorSystemStability.finite_operator_system_once_stable_permanently
• Dependency: D5/S3/Quantum/Fibers/OperatorSystemTowerStability