Limit-Stage Residual Intersection

Abstract

A limit-stage residual is the intersection of all predecessor residuals.

Theorem 1.1 (Limit-stage residuals are predecessor intersections).

$$\begin{array}{r}\forall K,H,I:\mathrm{Type},\\ [\mathrm{RCLike}\left(K\right)]\wedge [\mathrm{NormedAddCommGroup}\left(H\right)]\wedge [\mathrm{InnerProductSpace}\left(K,H\right)]\wedge \\ [\mathrm{CompleteSpace}\left(H\right)]\wedge [\mathrm{Preorder}\left(I\right)],\\ \forall V,R:I\to {\mathrm{ClosedSubmodule}}_K(H),lambda:I,\\ \mathrm{Monotone}\left(V\right)\wedge \\ (\forall alpha:I,R(alpha)=V(alpha{)}^{\perp })\wedge \\ V(lambda)=\mathrm{ClosedSup}\left(V(alpha{)}_{alpha<lambda}\right)\Rightarrow \\ R(lambda)=\mathrm{Inf}\left(R(alpha{)}_{alpha<lambda}\right).\end{array}$$

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

Source. Repository-derived.

Commentary.

Let V be a monotone indexed tower of closed subspaces in a complete real-or-complex inner-product space. Define the residual at each stage alpha by R(alpha) = V(alpha)^perp, and fix a stage lambda.

The premise identifies the space at lambda with the closed supremum of the spaces at all strictly earlier stages. Equivalently, this supremum is the closed linear span of their union.

Orthogonal complementation sends that closed supremum to the intersection of the residuals at every predecessor. The proof directly applies the pinned Mathlib identity ClosedSubmodule.iInf_orthogonal.

References

• Truth anchor: D5/S3/Quantum/Completion/LimitStageResidualIntersection.limit_stage_residual_intersection