Finite-Stage Orthogonal Expansion

Abstract

Finite orthogonal shell towers expand into the initial space, extracted shells, and residual.

Theorem 1.1 (Finite orthogonal shell towers expand stagewise).

$$\begin{gathered} \forall H:\mathrm{Type},[\mathrm{NormedAddCommGroup}(H)][\mathrm{InnerProductSpace}(\mathbb{R},H)][\mathrm{CompleteSpace}(H)],\forall S,E:\mathbb{N}\to \mathrm{ClosedSub}(\mathbb{R},H),(\forall k,S_{k+1}=\mathrm{join}(S_k,E_{k+1}))\Rightarrow (\forall k,E_{k+1}\subseteq S_k^{\perp })\Rightarrow \forall n\in \mathbb{N},S_n=\mathrm{join}(S_0,\mathrm{finiteShellSpan}(E,n))\wedge \\ \mathrm{top}=\mathrm{join}(\mathrm{join}(S_0,\mathrm{finiteShellSpan}(E,n)),S_n^{\perp })\wedge \\ {S}_n^{\perp }=\mathrm{join}(E_{n+1},S_{n+1}^{\perp }). \end{gathered}$$

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

Source. Repository-derived.

Commentary.

Let H be a complete real inner-product space. Let S and E be sequences of closed subspaces. At each stage, S(k+1) is the join of S(k) and E(k+1), while E(k+1) lies in the orthogonal complement of S(k).

For every finite stage n, S(n) is the join of S(0) with the first n shells. The whole space is the join of that accumulated stage and its orthogonal residual. The current residual is itself the join of the next shell and the next residual.

Pinned Mathlib and Loogle returned Submodule.sup_orthogonal_inf_of_hasOrthogonalProjection as the exact one-step splitting result, which the Lean proof imports and applies. Repository and library searches found no exact finite-stage expansion, so the shell accumulation is proved by induction.

The closed-subspace formulation preserves arbitrary complete Hilbert spaces and therefore includes finite-dimensional extracted shells without restricting the ambient space to finite dimension.

References

• Truth anchor: D5/S3/Observer/Tomography/FiniteStageExpansion.finite_stage_expansion