Compatible Unbounded Coordinates

Abstract

Actual first-coordinate projections are compatible but the partial-one family is unbounded and unrealizable.

Definition 1.1 (The actual first-coordinate span).

$$\begin{array}{c}\forall K:Typeu,[\mathrm{RCLike}(K)],\\ \forall n:\mathbb{N},\mathrm{coordinateSpace}(K,n):\mathrm{Submodule}(K,\mathrm{lp}((i:\mathbb{N}\mapsto K),2))=\mathrm{span}(K,\mathrm{range}((i:\mathrm{Fin}(n)\mapsto \mathrm{single}(2,\mathrm{val}(i),1)))).\end{array}$$

Formalization. D5/S3/Quantum/Completion/CompatibleUnboundedCoordinates.coordinateSpace (✓ std3).

Source. Repository-derived.

Commentary.

Coordinates are numbered from zero. The range n consists of exactly the first n coordinates, and stage zero is the span of the empty set.

Definition 1.2 (The actual partial-one vectors).

$$\begin{array}{c}\forall K:Typeu,[\mathrm{RCLike}(K)],\\ \forall n:\mathbb{N},\mathrm{partialOnes}(K,n):\mathrm{lp}((i:\mathbb{N}\mapsto K),2)=\sum _{i\in \mathrm{range}(n)}\mathrm{single}(2,i,1).\end{array}$$

Formalization. D5/S3/Quantum/Completion/CompatibleUnboundedCoordinates.partialOnes (✓ std3).

Source. Repository-derived.

Commentary.

These are finite sums in the existing lp space at exponent 2, with its existing norm and inner product.

Proposition 1.3 (Finite-dimensional coordinate stages).

$$\begin{array}{c}\forall K:Typeu,[\mathrm{RCLike}(K)],\\ \forall n:\mathbb{N},\mathrm{FiniteDimensional}(K,\mathrm{coordinateSpace}(K,n)).\end{array}$$

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

Source. Repository-derived.

Commentary.

The finite range of standard coordinate vectors spans each stage.

Proposition 1.4 (Actual orthogonal projections).

$$\begin{array}{c}\forall K:Typeu,[\mathrm{RCLike}(K)],\\ \forall n:\mathbb{N},\mathrm{HasOrthogonalProjection}(\mathrm{coordinateSpace}(K,n)).\end{array}$$

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

Source. Repository-derived.

Commentary.

Finite dimensionality supplies completeness locally, so no stage-completeness hypothesis is added.

Theorem 1.5 (Projection is coordinate truncation).

$$\begin{array}{c}\forall K:Typeu,[\mathrm{RCLike}(K)],\\ \forall n:\mathbb{N},\forall x:\mathrm{lp}((i:\mathbb{N}\mapsto K),2),\mathrm{starProjection}(\mathrm{coordinateSpace}(K,n),x)=\sum _{i\in \mathrm{range}(n)}\mathrm{single}(2,i,x(i)).\end{array}$$

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

Source. Repository-derived.

Commentary.

The finite sum lies in the independently defined span. Its residual has zero first-n coordinates, so projection uniqueness applies. Mathlib’s complex inner product is conjugate linear in the first argument; the proof uses the residual in that argument and the coordinate vector in the second.

Theorem 1.6 (Compatible coordinates without a Hilbert-space realization).

$$\begin{array}{c}\forall K:Typeu,[\mathrm{RCLike}(K)],\\ (\mathrm{Monotone}((n:\mathbb{N}\mapsto \mathrm{coordinateSpace}(K,n))))\wedge \\ (\forall n:\mathbb{N},\mathrm{partialOnes}(K,n)\in \mathrm{coordinateSpace}(K,n))\wedge \\ (\forall n:\mathbb{N},\forall i:\mathbb{N},\mathrm{partialOnes}(K,n)(i)=\mathrm{ite}(i<n,1,0))\wedge \\ (\forall m:\mathbb{N},\forall n:\mathbb{N},m\le n⟹\mathrm{starProjection}(\mathrm{coordinateSpace}(K,m),\mathrm{partialOnes}(K,n))=\mathrm{partialOnes}(K,m))\wedge \\ (\forall n:\mathbb{N},\Vert \mathrm{partialOnes}(K,n){\Vert }^2=(n:\mathbb{R}))\wedge \\ (\forall n:\mathbb{N},\Vert \mathrm{partialOnes}(K,n)\Vert =\sqrt{n})\wedge \\ (\mathrm{Tendsto}((n:\mathbb{N}\mapsto \Vert \mathrm{partialOnes}(K,n)\Vert ),\mathrm{atTop}(),\mathrm{atTop}()))\wedge \\ (\neg \mathrm{BddAbove}(\mathrm{range}((n:\mathbb{N}\mapsto \Vert \mathrm{partialOnes}(K,n)\Vert ))))\wedge \\ (\forall x:\mathrm{lp}((i:\mathbb{N}\mapsto K),2),\forall n:\mathbb{N},(\Vert \mathrm{starProjection}(\mathrm{coordinateSpace}(K,n),x)\Vert \le \Vert x\Vert \wedge \Vert \mathrm{starProjection}(\mathrm{coordinateSpace}(K,n),x){\Vert }^2\le \Vert x{\Vert }^2))\wedge \\ (\neg (\exists x:\mathrm{lp}((i:\mathbb{N}\mapsto K),2),\forall n:\mathbb{N},\mathrm{starProjection}(\mathrm{coordinateSpace}(K,n),x)=\mathrm{partialOnes}(K,n)))\wedge \\ (\forall x:\mathrm{lp}((i:\mathbb{N}\mapsto K),2),\mathrm{Summable}((i:\mathbb{N}\mapsto \Vert x(i){\Vert }^2)))\wedge \\ (\neg \mathrm{Summable}((i:\mathbb{N}\mapsto \Vert (1:K){\Vert }^2)))\wedge \\ (\neg \mathrm{Mem\ell p}((i:\mathbb{N}\mapsto (1:K)),2))\wedge \\ (\neg (\exists z:\mathrm{boundedInverseLimit}((n:\mathbb{N}\mapsto \mathrm{coordinateSpace}(K,n))),\forall n:\mathbb{N},(z:\mathrm{BoundedContinuousFunction}(\mathbb{N},\mathrm{lp}((i:\mathbb{N}\mapsto K),2)))(n)=\mathrm{partialOnes}(K,n))).\end{array}$$

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

Source. Repository-derived.

Commentary.

All earlier-stage projection equations hold, while the norms tend to infinity. Projection contraction excludes a common lp preimage. Actual lp vectors have summable squared coordinate norms, whereas constant-one coefficients do not. The final exclusion concerns the existing submodule of bounded functions; compatibility alone does not supply boundedness.

References

• Truth anchor: D5/S3/Quantum/Completion/CompatibleUnboundedCoordinates.compatible_unbounded_coordinates
• Truth anchor: D5/S3/Quantum/Completion/CompatibleUnboundedCoordinates.coordinateSpace
• Truth anchor: D5/S3/Quantum/Completion/CompatibleUnboundedCoordinates.coordinateSpaceFiniteDimensional
• Truth anchor: D5/S3/Quantum/Completion/CompatibleUnboundedCoordinates.coordinateSpaceHasOrthogonalProjection
• Truth anchor: D5/S3/Quantum/Completion/CompatibleUnboundedCoordinates.coordinate_projection
• Truth anchor: D5/S3/Quantum/Completion/CompatibleUnboundedCoordinates.partialOnes
• Dependency: D5/S3/Quantum/Completion/BoundedInverseLimitReconstruction