Tail Residual Cross-Layer Bound

Abstract

A Lipschitz update separates a coarse defect into a fine tail and cross-layer defect.

Theorem 1.1 (Tail residual cross-layer defect bound).

$$V_m\subseteq V_n\wedge {\mathrm{Lipschitz}}_L(F)\Rightarrow \Vert P_m(F(X))-P_m(F(P_m(X)))\Vert \le L\Vert X-P_n(X)\Vert +\Vert P_m(F(P_n(X)))-P_m(F(P_m(P_n(X))))\Vert .$$

Proof. Machine-checked in Lean as D5/S3/Observer/MetricGeometryLaws/TailResidualCrossLayerBound.tail_residual_cross_layer_defect_bound (✓ std3). ∎

Source. Repository-derived.

Commentary.

Let V_m be a visible Hilbert subspace of V_n, with canonical orthogonal projections P_m and P_n. Let F be L-Lipschitz.

The coarse defect compares projecting F(X) with projecting F after the coarse projection. It is bounded by the Lipschitz image of the unresolved V_n tail plus the same defect evaluated after the fine projection.

Both defect terms are expanded directly from F and the canonical projections. The proof inserts the fine projected update, applies the triangle inequality and projection contraction, then uses P_m P_n = P_m for nested subspaces.

References

• Truth anchor: D5/S3/Observer/MetricGeometryLaws/TailResidualCrossLayerBound.tail_residual_cross_layer_defect_bound
• Dependency: D5/S3/Observer/MetricGeometry/DefectDecomposition
• Dependency: D5/S3/Quantum/Algebra/OrthogonalProjectionComplement