Canonical Strongest Separating Observer

Abstract

The normalized orthogonal residual is the canonical strongest separating observer.

Theorem 1.1 (Optimal residual readout and its exact maximizers).

$$\forall H\in \mathrm{RealHilbertSpace}\left(\right),M\in \mathrm{ClosedSubspace}\left(H\right),x\in H,\mathrm{proj}\left(\mathrm{orthogonalComplement}\left(M\right),x\right)\ne 0\Rightarrow \left({\sup }_{g:g\in \mathrm{orthogonalComplement}\left(M\right)\wedge \Vert g\Vert \le 1}\Vert \mathrm{inner}\left(g,x\right)\Vert =\Vert \mathrm{proj}\left(\mathrm{orthogonalComplement}\left(M\right),x\right)\Vert \wedge \left(\left(\forall g\in H,\left(g\in \mathrm{orthogonalComplement}\left(M\right)\wedge \Vert g\Vert \le 1\right)\Rightarrow \left(\Vert \mathrm{inner}\left(g,x\right)\Vert =\Vert \mathrm{proj}\left(\mathrm{orthogonalComplement}\left(M\right),x\right)\Vert \iff \left(g=\mathrm{proj}\left(\mathrm{orthogonalComplement}\left(M\right),x\right)/\Vert \mathrm{proj}\left(\mathrm{orthogonalComplement}\left(M\right),x\right)\Vert \vee g=-\mathrm{proj}\left(\mathrm{orthogonalComplement}\left(M\right),x\right)/\Vert \mathrm{proj}\left(\mathrm{orthogonalComplement}\left(M\right),x\right)\Vert \right)\right)\right)\wedge \left(\forall g\in H,\left(\left(g\in \mathrm{orthogonalComplement}\left(M\right)\wedge \Vert g\Vert \le 1\right)\wedge \mathrm{inner}\left(g,x\right)=\Vert \mathrm{proj}\left(\mathrm{orthogonalComplement}\left(M\right),x\right)\Vert \right)\Rightarrow g=\mathrm{proj}\left(\mathrm{orthogonalComplement}\left(M\right),x\right)/\Vert \mathrm{proj}\left(\mathrm{orthogonalComplement}\left(M\right),x\right)\Vert \right)\right)\right)$$

Proof. Machine-checked in Lean as D5/S3/Observer/CanonicalStrongestSeparatingObserver.canonical_strongest_separating_observer (✓ std3). ∎

Source. Repository-derived.

Commentary.

Let M be a closed subspace of a real Hilbert space, let x be a target, and let r be the orthogonal projection of x onto the orthogonal complement of M. Assume r is nonzero.

The supremum of the absolute readout over observers in the orthogonal unit ball is the norm of r, and both signs of the normalized residual attain it.

These are the only absolute-value maximizers. After requiring positive alignment, the normalized residual is the unique maximizer. This corrects the source’s false uniqueness claim for an absolute objective.

References

• Truth anchor: D5/S3/Observer/CanonicalStrongestSeparatingObserver.canonical_strongest_separating_observer