Hilbert Resolution Hierarchy

Abstract

Uniform Hilbert resolution controls state-family and member-target residuals, while proper projection stages obstruct uniform resolution.

Theorem 1.1 (Uniform resolution implies family and target resolution).

$$\begin{array}{c}\forall K,H:Type,\\ \mathrm{RCLike}\left(K\right)\wedge \mathrm{NormedAddCommGroup}\left(H\right)\wedge \mathrm{InnerProductSpace}\left(K,H\right),\\ V:\mathbb{N}\to \mathrm{Submodule}\left(K,H\right),(\forall n\in \mathbb{N},\mathrm{HasOrthogonalProjection}\left(V(n)\right)),\\ T:\mathrm{Set}\left(H\right),x:H,\\ (\lim \left(n,\infty ,\Vert I-P\left(V(n)\right)\Vert \right)=0\Rightarrow \lim \left(n,\infty ,{\sup }_{y\in T}\Vert P\left(V(n{)}^{\perp }\right)(y)\Vert \right)=0)\wedge \\ (x\in T\Rightarrow \lim \left(n,\infty ,{\sup }_{y\in T}\Vert P\left(V(n{)}^{\perp }\right)(y)\Vert \right)=0\Rightarrow \lim \left(n,\infty ,\Vert P\left(V(n{)}^{\perp }\right)(x)\Vert \right)=0)\wedge \\ ((\forall n\in \mathbb{N},V(n)\ne top)\Rightarrow ((\forall n\in \mathbb{N},\Vert I-P\left(V(n)\right)\Vert =1)\wedge \neg \lim \left(n,\infty ,\Vert I-P\left(V(n)\right)\Vert \right)=0)).\end{array}$$

Proof. Machine-checked in Lean as D5/S3/Observer/Completion/HilbertResolutionHierarchy.hilbert_resolution_hierarchy (✓ std3). ∎

Source. Repository-derived.

Commentary.

For arbitrary orthogonally complemented Hilbert subspaces V(n), the residual is the canonical orthogonal complement V(n)-perp. The family residual is the extended nonnegative supremum of its projection norms, so empty and unbounded families remain defined.

Operator-norm convergence to the identity forces the visible stage to be the whole space eventually, since every proper stage remains exactly one unit away. The family residual is then eventually zero.

A member target is bounded by the same family’s supremum. Finally, the frozen uniform-completion obstruction supplies both the norm-one identity and nonconvergence when every stage is proper.

References

• Truth anchor: D5/S3/Observer/Completion/HilbertResolutionHierarchy.hilbert_resolution_hierarchy
• Dependency: D5/S3/Observer/Completion/ResidualProgressMeasure
• Dependency: D5/S3/Quantum/Completion/UniformCompletionObstruction