Golden Two-Shadow Bound

Abstract

A contractive continuous linear map satisfies one six-entry golden Gram equivalence, and the spectral threshold is sharp.

Theorem 1.1 (Six golden Gram criteria agree at the maximal threshold).

$$\begin{array}{r}\forall V,W:\mathrm{Type}(),\\ [\mathrm{NormedAddCommGroup}(V)]\wedge [\mathrm{InnerProductSpace}(\mathbb{C},V)]\wedge [\mathrm{CompleteSpace}(V)],\\ [\mathrm{NormedAddCommGroup}(W)]\wedge [\mathrm{InnerProductSpace}(\mathbb{C},W)]\wedge [\mathrm{CompleteSpace}(W)],\\ (\forall H:\mathrm{ContinuousLinearMap}(\mathbb{C},V,W),\Vert H\Vert \le 1\Rightarrow \\ letD:\mathrm{ContinuousLinearMap}(\mathbb{C},V,V)=H^{\ast }\circ H;\\ List.TFAE([D^2\le I-D,D+D^2\le I,\Vert D\Vert \le {\varphi }^{-1},\Vert H\Vert \le \sqrt{{\varphi }^{-1}},\exists C:\mathrm{Units}(\mathrm{ContinuousLinearMap}(\mathbb{C},V,V)),\mathrm{val}(C)=I-D\wedge \mathrm{val}(C^{-1})\le \mathrm{algebraMap}(\mathbb{R},\mathrm{ContinuousLinearMap}(\mathbb{C},V,V),{\varphi }^2),\exists C:\mathrm{Units}(\mathrm{ContinuousLinearMap}(\mathbb{C},V,V)),\mathrm{val}(C)=I-D\wedge D\cdot \mathrm{val}(C^{-1})\le \mathrm{algebraMap}(\mathbb{R},\mathrm{ContinuousLinearMap}(\mathbb{C},V,V),\varphi )]))\wedge (\\ \mathrm{Nontrivial}(V)\Rightarrow \mathrm{Nontrivial}(W)\Rightarrow \\ \forall t:\mathbb{R},{\varphi }^{-1}<t\Rightarrow \\ \exists H:\mathrm{ContinuousLinearMap}(\mathbb{C},V,W),\Vert H\Vert \le 1\wedge \Vert H^{\ast }\circ H\Vert \le t\\ \wedge \neg ({H^{\ast }\circ H}^2\le I-H^{\ast }\circ H)).\end{array}$$

Proof. Machine-checked in Lean as D5/S3/Observer/Hankel/GoldenTwoShadowBound.golden_two_shadow_bound (✓ std3). ∎

Source. Repository-derived.

Commentary.

For every contractive continuous linear map, the positive operator D is constructed as its adjoint composed with the map. The six displayed formulas are entries of one List.TFAE statement.

The inverse criteria quantify units whose values are exactly I-D, so the display records invertibility together with each order bound.

When both Hilbert spaces are nontrivial, every spectral threshold strictly above the inverse golden ratio admits a contractive rank-one map with Gram norm below that threshold for which the positive two-shadow inequality fails. Thus the golden threshold is maximal.

References

• Truth anchor: D5/S3/Observer/Hankel/GoldenTwoShadowBound.golden_two_shadow_bound