Sequential Completeness

Abstract

Sequential readout completeness is equivalent to a trivial residual and full visible span.

Theorem 1.1 (Sequential completeness, zero residual, and full visible span).

$$\begin{gathered} \forall d\in \mathbb{N},\mathrm{NeZero}\left(d\right),A:\mathrm{Type}, \\ E:A\to {\mathrm{Herm}}_d^0, \\ {V}_0=span\left(\mathbb{R},(E_i:i\in A)\right),V=\mathbb{R}I+V_0, \\ N=V^{\perp }, \\ \mathrm{Injective}\left((\rho :DensityState\left(Fin\left(d\right)\right)\mapsto (i:A\mapsto \Re Tr\left(matrix\left(\rho \right)E_i\right)))\right)⟺N=\{0\}⟺V={\mathrm{Herm}}_d. \end{gathered}$$

Proof. Machine-checked in Lean as D5/S3/Observer/Tomography/SequentialCompleteness.sequential_completeness_criterion (✓ std3). ∎

Source. Repository-derived.

Commentary.

The allowed readout effects are centered Hermitian directions. Their real span is combined with the scalar identity line to construct the visible Hermitian space, and the residual is its orthogonal complement.

The canonical density-state signature is injective exactly when the centered effect span is full; finite-dimensional orthogonality then identifies a zero residual with a full visible span.

References

• Truth anchor: D5/S3/Observer/Tomography/SequentialCompleteness.sequential_completeness_criterion
• Dependency: D5/S3/Quantum/Tomography/InformationalCompletenessEquivalence