Sequential Word Observation Residual

Abstract

Instrument word expectations agree exactly on the generated orthogonal residual.

Theorem 1.1 (Bounded instrument words characterize the orthogonal residual).

$$\begin{gathered} \forall d:Nat,A,S:\mathrm{Type},J:A\to \mathrm{HermitianSpace}(d)\to \mathrm{HermitianSpace}(d),X:S\to \mathrm{HermitianSpace}(d),rho,sigma:S,n:Nat\Rightarrow \\ (\forall w:\mathrm{List}(A),\mathrm{length}(w)\le n\Rightarrow (\mathrm{inner}(\mathbb{R},X(rho),\mathrm{sequentialWordEffect}(J,w))=\mathrm{inner}(\mathbb{R},X(sigma),\mathrm{sequentialWordEffect}(J,w))))\iff (X(rho)-X(sigma)\in (\mathrm{span}(\mathbb{R},(\exists e:\mathrm{HermitianSpace}(d),\exists w:\mathrm{List}(A),\mathrm{length}(w)\le n\wedge e=\mathrm{sequentialWordEffect}(J,w))){)}^{\perp }). \end{gathered}$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Completion/SequentialWordObservationResidual.sequential_observation_iff (✓ std3). ∎

Source. Repository-derived.

Commentary.

For a real Hermitian operator carrier, each instrument dual map acts on the identity effect. The public word-effect construction folds those maps in source order, matching the Heisenberg composition of a finite instrument word.

Two represented states have equal expectations for every word of length at most n exactly when their difference is orthogonal to the real span of all generated word effects.

References

• Truth anchor: D5/S3/Quantum/Completion/SequentialWordObservationResidual.sequential_observation_iff
• Dependency: D5/S3/Quantum/Algebra/FutureWordOrthogonalResidual
• Dependency: D5/S3/Quantum/Entanglement/BipartiteSectorDecomposition