Finite Shell Residual

Abstract

A finite shell compression can vanish while its complementary defect remains nonzero.

Theorem 1.1 (A finite shell check does not close the residual).

$$\begin{gathered} \forall N:\mathbb{N},\mathrm{shellProjection}(N)\cdot \mathrm{defectOperator}(N)\cdot \mathrm{shellProjection}(N)=0\wedge \\ \mathrm{residualProjection}(N)\cdot \mathrm{defectOperator}(N)\cdot \mathrm{residualProjection}(N)\ne 0\wedge \\ \neg (\mathrm{shellProjection}(N)\cdot \mathrm{defectOperator}(N)\cdot \mathrm{shellProjection}(N)=0\Rightarrow \mathrm{residualProjection}(N)\cdot \mathrm{defectOperator}(N)\cdot \mathrm{residualProjection}(N)=0). \end{gathered}$$

Proof. Machine-checked in Lean as D5/S3/Observer/Residuals/FiniteShellResidual.finite_shell_check_does_not_close_residual (✓ std3). ∎

Source. Repository-derived.

Commentary.

For every finite shell size, the constructed defect vanishes after compression to the listed coordinates while its compression to the complementary residual coordinate remains nonzero.

The two explicit compressions therefore witness that the finite-shell vanishing assertion alone does not imply residual vanishing.

References

• Truth anchor: D5/S3/Observer/Residuals/FiniteShellResidual.finite_shell_check_does_not_close_residual