Uniform Completion Obstruction

Abstract

Proper Hilbert-subspace projections remain one operator-norm unit from the identity.

Theorem 1.1 (Proper projection stages stay uniformly separated from identity).

$$\begin{array}{c}\forall K,H,I:Type,\\ [\mathrm{RCLike}\left(K\right)],[\mathrm{NormedAddCommGroup}\left(H\right)],\\ [\mathrm{InnerProductSpace}\left(K,H\right)],\\ S:I\to {\mathrm{Submodule}}_K(H),\\ [\forall i:I,\mathrm{HasOrthogonalProjection}\left(S(i)\right)],\\ stageFilter:\mathrm{Filter}\left(I\right),[\mathrm{NeBot}\left(stageFilter\right)],\\ hProper:\forall i:I,S(i)\ne top,\\ ((\forall i:I,\Vert \mathrm{id}\left(K,H\right)-\mathrm{starProjection}\left(S(i)\right)\Vert =1)\wedge \\ \neg \mathrm{Tendsto}\left(\Lambda i:I,\Vert \mathrm{id}\left(K,H\right)-\mathrm{starProjection}\left(S(i)\right)\Vert ,stageFilter,\mathrm{nhds}\left(0\right)\right)).\end{array}$$

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

Source. Repository-derived.

Commentary.

Let S be a family of proper closed subspaces of a Hilbert space, indexed along a nontrivial stage filter, and let each stage map be its canonical orthogonal projection.

Identity minus the stage projection is the orthogonal projection onto the nonzero complementary subspace. Its operator norm is exactly one at every stage.

Consequently the operator-norm distances cannot converge to zero along the stage filter.

References

• Truth anchor: D5/S3/Quantum/Completion/UniformCompletionObstruction.uniform_completion_obstruction
• Dependency: D5/S3/Quantum/Completion/InfiniteDimensionalProjectionSeparation