Future Probability Residual Correlation

Abstract

Future linear-prediction error is exactly the correlation of state and effect residuals.

Theorem 1.1 (Future probability error is the exact residual correlation).

$$\begin{gathered} \forall d,[\mathrm{Fintype}\left(d\right)][\mathrm{Nonempty}\left(d\right)][\mathrm{DecidableEq}\left(d\right)], \\ \rho :\mathrm{Matrix}\left(d,d,\mathbb{C}\right),H:\mathrm{LinearMap}\left(\mathbb{R},\mathrm{HermitianTraceZero}\left(d\right),\mathrm{HermitianTraceZero}\left(d\right)\right), \\ r\in \mathbb{N},E:\mathrm{Fin}\left(r+1\right)\to \mathrm{HermitianTraceZero}\left(d\right),m,k\in \mathbb{N},a\in \mathrm{Fin}\left(r+1\right), \\ \mathrm{Density}\left(\rho \right)\Rightarrow \mathrm{let}S=\mathrm{towerSpace}\left(H,E,m\right),R=S^{\perp }, \\ {X}_{\rho }=\mathrm{densityCoordinate}\left(\rho \right),A_{a,k}=H^k(E(a)), \\ {\rho }_m=\mathrm{linearPredictionRepresentative}\left(S,X_{\rho }\right),\Delta p_{a,k}^{(m)}=\mathrm{ReTr}\left((\rho -{\rho }_m)A_{a,k}\right) \\ \Delta p_{a,k}^{(m)}=\mathrm{innerHS}\left(P\left(R,X_{\rho }\right),P\left(R,A_{a,k}\right)\right)\wedge \\ \mathrm{abs}\left(\Delta p_{a,k}^{(m)}\right)\le \sqrt{\mathrm{residualMass}\left(S,X_{\rho }\right)}\mathrm{normHS}\left(P\left(R,A_{a,k}\right)\right)\wedge \\ \neg \mathrm{PosSemidef}\left(\mathrm{linearPredictionRepresentative}\left(\mathrm{span}\left(\mathbb{R},\mathrm{diag}\left(1,0,-1\right)\right),\mathrm{densityCoordinate}\left(\mathrm{diag}\left(1,0,0\right)\right)\right)\right). \end{gathered}$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Tomography/FutureProbabilityResidualCorrelation.future_probability_residual_correlation (✓ std3). ∎

Source. Repository-derived.

Commentary.

Let rho be a positive semidefinite trace-one matrix on a finite nonempty carrier. Its centered coordinate lies in the canonical real trace-zero Hermitian space. A real-linear Heisenberg map and a finite centered-effect family construct the visible tower S, its orthogonal residual R, and every future effect A_a,k.

The linear representative retains the visible projection of the centered state and restores the trace-one identity component. The real trace error against every iterated future effect equals the Hilbert–Schmidt inner product of the state and effect residual projections.

Cauchy–Schwarz bounds the absolute error by the square root of the canonical residual mass times the future effect residual norm. The final public conjunct uses the valid density diag(1,0,0) and the visible real line spanned by diag(1,0,-1); its projected representative has diagonal entries 5/6, 1/3, and -1/6, so it is not positive semidefinite.

The proof applies the exact orthogonal-projection self-adjointness and Cauchy–Schwarz bounds from the pinned library. Repository carrier, tower, residual-space, residual-mass, and centered-state definitions are imported rather than redeclared.

References

• Truth anchor: D5/S3/Quantum/Tomography/FutureProbabilityResidualCorrelation.future_probability_residual_correlation
• Dependency: D5/S3/Quantum/Fibers/CenteredEffectTowerStability
• Dependency: D5/S3/Quantum/Tomography/ResidualControlsNaturality