Four Typed Completion Modes

Abstract

Target, state-family, algebra, and uniform completion remain distinct typed claims.

Theorem 1.1 (The four completion modes form a strict typed hierarchy).

$$\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,\\ ((\mathrm{UniformBall}\left(V\right)\Rightarrow \mathrm{StateFamily}\left(V,T\right))\wedge (x\in T\Rightarrow \mathrm{StateFamily}\left(V,T\right)\Rightarrow \mathrm{Target}\left(V,x\right)))\wedge \\ (\text{let}V0:\mathbb{N}\to \mathrm{Submodule}\left(\mathbb{R},\mathbb{R}\right):=n\mapsto bot;T0:\mathrm{Set}\left(\mathbb{R}\right):=\{0,1\};((\mathrm{Target}\left(V0,0\right))\wedge (\neg \mathrm{StateFamily}\left(V0,T0\right))))\wedge \\ (\text{let}e0:\mathrm{EuclideanSpace}\left(\mathbb{C},\mathrm{Fin}\left(2\right)\right):=toLp2\left(1,0\right);W:\mathrm{Submodule}\left(\mathbb{C},\mathrm{EuclideanSpace}\left(\mathbb{C},\mathrm{Fin}\left(2\right)\right)\right):=\mathbb{C}\cdot e0;V1:\mathbb{N}\to \mathrm{Submodule}\left(\mathbb{C},\mathrm{EuclideanSpace}\left(\mathbb{C},\mathrm{Fin}\left(2\right)\right)\right):=n\mapsto W;T1:\mathrm{Set}\left(\mathrm{EuclideanSpace}\left(\mathbb{C},\mathrm{Fin}\left(2\right)\right)\right):=\{e0\};((\mathrm{StateFamily}\left(V1,T1\right))\wedge (\neg \mathrm{UniformBall}\left(V1\right))))\wedge \\ (\text{let}A2:\mathrm{Matrix}\left(\mathrm{ZMod}\left(2\right),\mathrm{ZMod}\left(2\right),\mathbb{C}\right):=\mathrm{single}\left(0,1,1\right);s2:\mathrm{EuclideanSpace}\left(\mathbb{C},\mathrm{Fin}\left(2\right)\right):=toLp2\left(\mathrm{entry}\left(A2,0,0\right),\mathrm{entry}\left(A2,0,1\right)\right);V2:\mathbb{N}\to \mathrm{Submodule}\left(\mathbb{C},\mathrm{EuclideanSpace}\left(\mathbb{C},\mathrm{Fin}\left(2\right)\right)\right):=n\mapsto bot;T2:\mathrm{Set}\left(\mathrm{EuclideanSpace}\left(\mathbb{C},\mathrm{Fin}\left(2\right)\right)\right):=\{s2\};((A2\in \mathrm{windowGeneratedAlgebra}\left(2\right))\wedge (\mathrm{windowGeneratedAlgebra}\left(2\right)=top)\wedge (s2=toLp2\left(0,1\right))\wedge (\neg \mathrm{Target}\left(V2,s2\right))\wedge (\neg \mathrm{StateFamily}\left(V2,T2\right))\wedge (\neg \mathrm{UniformBall}\left(V2\right))))\wedge \\ (\text{let}A3:\mathrm{Matrix}\left(\mathrm{Fin}\left(2\right),\mathrm{Fin}\left(2\right),\mathbb{C}\right):=\mathrm{single}\left(1,0,1\right);s3:\mathrm{EuclideanSpace}\left(\mathbb{C},\mathrm{Fin}\left(2\right)\right):=toLp2\left(\mathrm{entry}\left(A3,1,0\right),\mathrm{entry}\left(A3,1,1\right)\right);V3:\mathbb{N}\to \mathrm{Submodule}\left(\mathbb{C},\mathrm{EuclideanSpace}\left(\mathbb{C},\mathrm{Fin}\left(2\right)\right)\right):=n\mapsto top;T3:\mathrm{Set}\left(\mathrm{EuclideanSpace}\left(\mathbb{C},\mathrm{Fin}\left(2\right)\right)\right):=\{s3\};((\mathrm{UniformBall}\left(V3\right))\wedge (\mathrm{StateFamily}\left(V3,T3\right))\wedge (\mathrm{Target}\left(V3,s3\right))\wedge (\mathrm{primeDiagonalAlgebra}\left(2,\varnothing \right)\ne top)\wedge (\neg (A3\in \mathrm{primeDiagonalAlgebra}\left(2,\varnothing \right))))).\\ \text{where}\mathrm{Target}\left(V,x\right):=\lim \left(n,\infty ,\Vert P\left(V(n{)}^{\perp }\right)(x)\Vert \right)=0;\mathrm{StateFamily}\left(V,T\right):=\lim \left(n,\infty ,{\sup }_{y\in T}\Vert P\left(V(n{)}^{\perp }\right)(y)\Vert \right)=0;\mathrm{UniformBall}\left(V\right):=\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/FourTypedCompletionHierarchy.four_typed_completion_hierarchy (✓ std3). ∎

Source. Repository-derived.

Commentary.

For arbitrary scalar and Hilbert carriers K and H, with RCLike K, a normed additive commutative group H, an inner-product structure, orthogonally complemented stages V, a state family T, and a target x, uniform projection convergence implies convergence of the canonical family residual. If x belongs to T, family convergence then implies target convergence.

A constant zero tower on the real line resolves target zero but not the two-point family. A constant one-dimensional complex subspace resolves its displayed nonzero member family while every stage remains proper, so uniform convergence fails.

For algebra completion, the two-address clock-and-shift algebra is the full matrix algebra and contains the displayed off-diagonal observable. The state constructed from that observable nevertheless fails target, singleton-family, and uniform projection convergence for the constant zero tower.

Conversely, the constant top tower resolves the displayed matrix-derived state, its singleton family, and the uniform ball. The finite prime-diagonal operational algebra is still proper and omits the same constructed off-diagonal observable. Thus every completion claim in the statement remains attached to its target, family, operator algebra, or uniform-ball object.

References

• Truth anchor: D5/S3/Observer/Completion/FourTypedCompletionHierarchy.four_typed_completion_hierarchy
• Dependency: D5/S3/Observer/Completion/HilbertResolutionHierarchy
• Dependency: D5/S3/Observer/WindowAlgebra/WindowGeneration
• Dependency: D5/S3/Quantum/FixedAlgebra/PrimeDiagonalSaturation