Local Dynamics Do Not Complete Tomography

Abstract

A Heisenberg dynamics preserving the two local sectors cannot generate a nonzero cross-factor correlation direction.

Theorem 1.1 (Local-sector closure excludes nonzero correlation readouts).

$$\forall m:\mathrm{Nat},n:\mathrm{Nat},\mathrm{NeZero}(m),\mathrm{NeZero}(n),H:\mathrm{LinearMap}(\mathbb{R},\mathrm{BipartiteHermitian}(m,n),\mathrm{BipartiteHermitian}(m,n)),(\forall x:\mathrm{BipartiteHermitian}(m,n),x\in \mathrm{Sup}(\mathrm{localASector}(m,n),\mathrm{localBSector}(m,n))\Rightarrow H(x)\in \mathrm{Sup}(\mathrm{localASector}(m,n),\mathrm{localBSector}(m,n)))\Rightarrow (\forall t:\mathrm{Nat},x:\mathrm{BipartiteHermitian}(m,n),x\in \mathrm{Sup}(\mathrm{localASector}(m,n),\mathrm{localBSector}(m,n))\Rightarrow H^{t}x\in \mathrm{Sup}(\mathrm{localASector}(m,n),\mathrm{localBSector}(m,n))\wedge \forall t:\mathrm{Nat},x:\mathrm{BipartiteHermitian}(m,n),x\in \mathrm{Sup}(\mathrm{localASector}(m,n),\mathrm{localBSector}(m,n))\Rightarrow H^{t}x\in \mathrm{correlationSector}(m,n)\Rightarrow H^{t}x=0).$$

Proof. Machine-checked in Lean as D5/S3/Quantum/PredictionDepth/LocalDynamicsNoTomography.local_dynamics_no_tomography (✓ std3). ∎

Source. Repository-derived.

Commentary.

The finite bipartite Hermitian carrier is split into the canonical A-local, B-local, and correlation sectors.

For any Heisenberg linear dynamics that preserves the join of the two local sectors, every finite iterate remains local. Orthogonality of the correlation sector then forces any iterate lying in it to be zero.

References

• Truth anchor: D5/S3/Quantum/PredictionDepth/LocalDynamicsNoTomography.local_dynamics_no_tomography
• Dependency: D5/S3/Quantum/Entanglement/BipartiteSectorDecomposition