Chebyshev Signed-Distance Separator

Abstract

First Chebyshev slack separates nonnegative and negative squared distances.

Theorem 1.1 (First Chebyshev Slack Separates Signed Squared Distance).

$$\begin{gathered} \forall a,x,\delta :\mathbb{R}, \\ (\frac{1}{4}<a)\wedge (0\le x)\wedge (0<\delta )\wedge ({\delta }^2<a)\Rightarrow \\ \mathrm{let}{u}_{on}=\frac{x-a}{x+a}, \\ \mathrm{let}{s}_{on}=1-T_1(u_{on}{)}^2, \\ \mathrm{let}{u}_{off}=\frac{-{\delta }^2-a}{-{\delta }^2+a}, \\ \mathrm{let}{s}_{off}=1-T_1(u_{off}{)}^2, \\ ((u_{on}\in [-1,1])\wedge \\ (s_{on}\in [0,1])\wedge \\ (u_{off}<-1)\wedge \\ (s_{off}<0)). \end{gathered}$$

Proof. Machine-checked in Lean as D5/S3/Weil/CayleyLaguerre/ChebyshevSignedDistanceSeparator.first_chebyshev_slack_separates_signed_squared_distance (✓ std3). ∎

Source. Repository-derived.

Commentary.

Above the stated scale thresholds, a nonnegative squared-distance input has compact coordinate in the closed unit interval and first Chebyshev slack in the interval from zero to one. The negative signed value has coordinate below negative one and strictly negative slack.

This is only a finite algebraic separator under the four explicit hypotheses. It makes no converse claim and does not claim that a xi spectrum supplies the signed-distance observation.

References

• Truth anchor: D5/S3/Weil/CayleyLaguerre/ChebyshevSignedDistanceSeparator.first_chebyshev_slack_separates_signed_squared_distance
• Dependency: D5/S3/Weil/CayleyLaguerre/ChebyshevSlackPositivity