Finite-Time Tomography Saturation

Abstract

All-future observability is decided by the first trace-zero carrier dimension layers.

Theorem 1.1 (The exact trace-zero dimension controls every future readout).

$$\begin{gathered} \forall d\in \mathbb{N},\mathrm{NeZero}(d),Y:Type, \\ \mathrm{AddCommGroup}(Y)\wedge \mathrm{Module}(\mathbb{R},Y), \\ A:\mathrm{LinearMap}(\mathbb{R},\mathrm{HermitianTraceZero}(\mathrm{Fin}(d)),\mathrm{HermitianTraceZero}(\mathrm{Fin}(d))),C:\mathrm{LinearMap}(\mathbb{R},\mathrm{HermitianTraceZero}(\mathrm{Fin}(d)),Y)\Rightarrow \\ {N}_{\infty }:=\mathrm{iInf}(k\in \mathbb{N},\ker (C\circ A^k));N_{d^2-1}:=\mathrm{iInf}(k\in \mathrm{Fin}(d^2-1),\ker (C\circ A^k)); \\ (N_{\infty }=\mathrm{bot}()\Rightarrow N_{d^2-1}=\mathrm{bot}())\wedge N_{\infty }=N_{d^2-1}. \end{gathered}$$

Proof. Machine-checked in Lean as D5/S3/ObserverMemory/Dynamics/FiniteTimeTomographySaturation.finite_time_tomography_saturation (✓ std3). ∎

Source. Repository-derived.

Commentary.

Fix a positive matrix dimension d. The state carrier is the imported real subspace HermitianTraceZero(Fin d), the evolution A is a real-linear endomorphism of that carrier, and C is a real-linear readout into an arbitrary real module Y.

The all-future kernel is constructed by intersecting ker(C composed with A to the kth power) over every natural k. The finite kernel uses the same source test over the exact index type Fin(d squared minus one).

The public statement contains both source clauses: a trivial all-future kernel forces the finite kernel to be trivial, and more strongly the two constructed kernels are equal.

The proof applies Cayley–Hamilton polynomial reduction to express every later evolution power through the first ambient-finrank powers. The imported finrank theorem identifies that ambient real dimension as d squared minus one.

References

• Truth anchor: D5/S3/ObserverMemory/Dynamics/FiniteTimeTomographySaturation.finite_time_tomography_saturation
• Dependency: D5/S3/Quantum/Entanglement/BipartiteSectorDecomposition
• Dependency: D5/S3/Quantum/Fibers/TraceZeroReadoutOrthogonalEquivalence