Observer Refinement, Visibility, and Residuals

Abstract

Physical observer refinement is dual to visible and residual subspace inclusion.

Theorem 1.1 (Observer refinement has dual visible and residual criteria).

$$\begin{array}{r}\forall d:Nat,\mathrm{NeZero}\left(d\right),IndexOne,IndexTwo:\mathrm{Type},\\ effectsOne:IndexOne\to \mathrm{HermitianSpace}\left(d\right),effectsTwo:IndexTwo\to \mathrm{HermitianSpace}\left(d\right),\\ \mathrm{let}stateOperator:\mathrm{DensityState}\left(\mathrm{Fin}\left(d\right)\right)\to \mathrm{HermitianSpace}\left(d\right):=\rho \mapsto \mathrm{HermitianMk}\left(\mathrm{ofMatrixSymm}\left(\mathrm{val}\left(\rho \right)\right)\right),\\ \mathrm{let}signatureOne:=\rho \mapsto i\mapsto \mathrm{innerR}\left(\mathrm{stateOperator}\left(\rho \right),\mathrm{effectsOne}\left(i\right)\right),\\ \mathrm{let}signatureTwo:=\rho \mapsto i\mapsto \mathrm{innerR}\left(\mathrm{stateOperator}\left(\rho \right),\mathrm{effectsTwo}\left(i\right)\right),\\ \mathrm{let}visibleOne:=\mathrm{span}\left(\mathbb{R},\mathrm{insert}\left(\mathrm{identityHermitian}\left(d\right),\mathrm{range}\left(effectsOne\right)\right)\right),visibleTwo:=\mathrm{span}\left(\mathbb{R},\mathrm{insert}\left(\mathrm{identityHermitian}\left(d\right),\mathrm{range}\left(effectsTwo\right)\right)\right),\\ \mathrm{let}residualOne:=\mathrm{orthogonal}\left(visibleOne\right),residualTwo:=\mathrm{orthogonal}\left(visibleTwo\right),\\ \mathrm{let}refines:=\forall \rho ,\sigma :\mathrm{DensityState}\left(\mathrm{Fin}\left(d\right)\right),\mathrm{signatureTwo}\left(\rho \right)=\mathrm{signatureTwo}\left(\sigma \right)\Rightarrow \mathrm{signatureOne}\left(\rho \right)=\mathrm{signatureOne}\left(\sigma \right),\\ (refines⟺residualTwo\subseteq residualOne)\wedge \\ (residualTwo\subseteq residualOne⟺visibleOne\subseteq visibleTwo).\end{array}$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Measurement/ObserverRefinementVisibleResidualEquivalence.observer_refinement_visible_residual_equivalence (✓ std3). ∎

Source. Repository-derived.

Commentary.

Each observer signature is constructed from real Hilbert–Schmidt pairings between density-state matrices and its Hermitian effect family. Its visible space is the real span of the identity and those effects, and its residual is the orthogonal complement of that span.

Refinement means that equality of the second observer’s signature on two physical density states forces equality of the first. Perturbations around the maximally mixed state turn every residual direction into a difference of density states.

Consequently refinement is exactly reverse inclusion of residuals. The pinned orthogonal-complement order theorem then identifies that condition with forward inclusion of visible spaces.

References

• Truth anchor: D5/S3/Quantum/Measurement/ObserverRefinementVisibleResidualEquivalence.observer_refinement_visible_residual_equivalence
• Dependency: D5/S3/Quantum/Tomography/InformationalCompletenessEquivalence