Finite Subspace Complement Absorption

Abstract

Removing a finite-dimensional subspace preserves the Hilbert dimension and unitary type of an infinite-dimensional Hilbert space.

Theorem 1.1 (A finite extraction leaves a full-dimensional complement).

$$\forall K\in Type,H\in Type,M\in \mathrm{Submodule}\left(K,H\right),\left(\mathrm{RCLike}\left(K\right)\wedge \left(\mathrm{NormedAddCommGroup}\left(H\right)\wedge \left(\mathrm{InnerProductSpace}\left(K,H\right)\wedge \left(\mathrm{CompleteSpace}\left(H\right)\wedge \left(\mathrm{FiniteDimensional}\left(K,M\right)\wedge \left(\neg \mathrm{FiniteDimensional}\left(K,H\right)\right)\right)\right)\right)\right)\right)\Rightarrow \left(\exists I\in Type,\exists bperp\in \mathrm{HilbertBasis}\left(I,K,\mathrm{orthogonalComplement}\left(M\right)\right),\exists b\in \mathrm{HilbertBasis}\left(I,K,H\right),\exists U\in \mathrm{LinearIsometryEquiv}\left(K,\mathrm{orthogonalComplement}\left(M\right),H\right),\exists Q\in \mathrm{LinearIsometryEquiv}\left(K,\mathrm{SubmoduleQuotient}\left(H,M\right),H\right),U=\mathrm{trans}\left(\mathrm{repr}\left(bperp\right),\mathrm{symm}\left(\mathrm{repr}\left(b\right)\right)\right)\wedge Q=\mathrm{trans}\left(\mathrm{quotientEquivOrthogonal}\left(M\right),U\right)\right)$$

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

Source. Repository-derived.

Commentary.

A common index type carries an explicit Hilbert basis of the orthogonal complement and an explicit Hilbert basis of the ambient space, which states equality of Hilbert dimension.

The complement unitary is the composition of the two basis representations. The quotient unitary then composes the canonical quotient-to-orthogonal-complement isometry with that unitary.

The proof extends a finite orthonormal basis of the extracted subspace to an ambient Hilbert basis. It applies the frozen basis-tail construction to the remaining coordinates and uses finite-cardinal absorption only to reindex that tail.

References

• Truth anchor: D5/S3/Observer/Completion/FiniteSubspaceComplementAbsorption.finite_subspace_complement_absorption
• Dependency: D5/S3/Quantum/Algebra/QuotientOrthogonalComplement
• Dependency: D5/S3/Quantum/Completion/TransfiniteBasisResidualTower