Future Statistics and the Infinite Operator System
Abstract
Future operator statistics are exactly the annihilator of the generated system.
Theorem 1.1 (Future statistics characterize the infinite-system annihilator).
Proof. Machine-checked in Lean as D5/S3/Quantum/Fibers/FutureStatisticsEquivalence.future_statistics_iff_annihilates_infinite_system (✓ std3). ∎
Source. Repository-derived.
Commentary.
The states are positive trace-one matrices on a finite complex matrix carrier. The Schrödinger map is completely positive and trace-preserving, while its Heisenberg dual is completely positive, unital, and satisfies the displayed trace-duality identity.
The initial operator system is a real subspace of the full Hermitian carrier containing the identity. The infinite prediction system is the real span of every finite Heisenberg iterate of every initial effect.
Equality of the complete initial-system readout after every finite channel iterate is equivalent to zero trace pairing of the state difference with every effect in that generated system.
References
- Truth anchor:
D5/S3/Quantum/Fibers/FutureStatisticsEquivalence.future_statistics_iff_annihilates_infinite_system - Dependency: D5/S3/Quantum/Divergence/QuantumRelativeEntropyDefectComposition
- Dependency: D5/S3/Quantum/Fibers/OperatorSystemTowerStability