Orthogonal Residual Recurrence

Abstract

Recursive orthogonal extraction splits each residual and the ambient Hilbert space.

Theorem 1.1 (Recursive orthogonal extraction splits residuals).

$$\begin{gathered} \forall H:\mathrm{Type},[\mathrm{NormedAddCommGroup}(H)][\mathrm{InnerProductSpace}(\mathbb{R},H)][\mathrm{CompleteSpace}(H)],\forall M:\mathrm{ClosedSub}(\mathbb{R},H),E:\mathbb{N}\to \mathrm{ClosedSub}(\mathbb{R},H),(\forall k,E_{k+1}\subseteq \mathrm{recursiveResidual}(M,E,k))\Rightarrow \forall n\in \mathbb{N},\mathrm{recursiveResidual}(M,E,n+1)=\mathrm{accumulatedSubspace}(M,E,n+1{)}^{\perp }\wedge \\ \mathrm{IsOrtho}(E_{n+1},\mathrm{recursiveResidual}(M,E,n+1))\wedge \mathrm{recursiveResidual}(M,E,n)=\mathrm{join}(E_{n+1},\mathrm{recursiveResidual}(M,E,n+1))\wedge \\ \mathrm{IsOrtho}(\mathrm{accumulatedSubspace}(M,E,n+1),\mathrm{recursiveResidual}(M,E,n+1))\wedge \mathrm{top}=\mathrm{join}(\mathrm{accumulatedSubspace}(M,E,n+1),\mathrm{recursiveResidual}(M,E,n+1)). \end{gathered}$$

Proof. Machine-checked in Lean as D5/S3/Observer/Tomography/OrthogonalResidualRecurrence.orthogonal_residual_recurrence (✓ std3). ∎

Source. Repository-derived.

Commentary.

Let H be a complete real inner-product space, let M be a closed subspace, and let E be a sequence of closed shells. Construct the accumulated tower from joins with E(n+1), and independently construct the residual tower from intersections with the orthogonal complements of E(n+1).

If every next shell lies in the current residual, then the next residual is the orthogonal complement of the next accumulated space. The current residual is the orthogonal direct sum of the next shell and next residual, and the ambient space is the orthogonal direct sum of the next accumulated space and residual.

Pinned Mathlib and Loogle returned ClosedSubmodule.inf_orthogonal and Submodule.sup_orthogonal_inf_of_hasOrthogonalProjection as exact one-step identities. The Lean proof applies both directly.

References

• Truth anchor: D5/S3/Observer/Tomography/OrthogonalResidualRecurrence.orthogonal_residual_recurrence