Negative-Square Laplace Resolvent

Abstract

A negative-square mode has an exact damping threshold and Laplace resolvent.

Definition 1.1 (The stabilization gap).

Lean statement: D5/S3/Analytic/ReflectedSpectrum/NegativeSquareLaplaceResolvent.stabilizationGap

Formalization. D5/S3/Analytic/ReflectedSpectrum/NegativeSquareLaplaceResolvent.stabilizationGap (✓ std3).

Source. Repository-derived.

Commentary.

The gap adds scalar damping to the frozen signed spectral atom. Because the atom is minus delta squared, the resulting denominator is damping minus delta squared.

Definition 1.2 (The damped forward kernel).

Lean statement: D5/S3/Analytic/ReflectedSpectrum/NegativeSquareLaplaceResolvent.dampedNegativeSquareKernel

Formalization. D5/S3/Analytic/ReflectedSpectrum/NegativeSquareLaplaceResolvent.dampedNegativeSquareKernel (✓ std3).

Source. Repository-derived.

Commentary.

The forward kernel is the real exponential with rate equal to minus the stabilization gap. Its half-line integrability detects the exact damping threshold.

Definition 1.3 (The scalar negative-square resolvent).

Lean statement: D5/S3/Analytic/ReflectedSpectrum/NegativeSquareLaplaceResolvent.negativeSquareResolvent

Formalization. D5/S3/Analytic/ReflectedSpectrum/NegativeSquareLaplaceResolvent.negativeSquareResolvent (✓ std3).

Source. Repository-derived.

Commentary.

The scalar resolvent is the inverse stabilization gap. Its pole occurs when the applied damping exactly equals the squared reflected split.

Theorem 1.4 (Threshold, integrability, integral, and pole agree).

$$\begin{array}{r}\forall delta:\mathbb{R},u:\mathbb{R},\mathrm{IntegrableOnIoi}(\mathrm{dampedNegativeSquareKernel}(delta,u),0)⟺delt{a}^2<u\wedge \\ delt{a}^2<u\Rightarrow \mathrm{IntegralIoi}(\mathrm{dampedNegativeSquareKernel}(delta,u),0)=\mathrm{negativeSquareResolvent}(delta,u)\wedge \\ 0<\mathrm{negativeSquareResolvent}(delta,u)⟺delt{a}^2<u\wedge \\ \mathrm{stabilizationGap}(delta,u)=0⟺u=delt{a}^2.\end{array}$$

Proof. Machine-checked in Lean as D5/S3/Analytic/ReflectedSpectrum/NegativeSquareLaplaceResolvent.negative_square_laplace_resolvent (✓ std3). ∎

Source. Repository-derived.

Commentary.

Pinned Mathlib improper-integral theorems show that the damped kernel is integrable on the positive half-line exactly when damping exceeds delta squared. Above this threshold, its integral is the inverse gap.

The same threshold characterizes positivity of the scalar resolvent, while equality marks its pole. This closes the local stabilization debt and does not construct a global zeta resolvent.

References

• Truth anchor: D5/S3/Analytic/ReflectedSpectrum/NegativeSquareLaplaceResolvent.dampedNegativeSquareKernel
• Truth anchor: D5/S3/Analytic/ReflectedSpectrum/NegativeSquareLaplaceResolvent.negativeSquareResolvent
• Truth anchor: D5/S3/Analytic/ReflectedSpectrum/NegativeSquareLaplaceResolvent.negative_square_laplace_resolvent
• Truth anchor: D5/S3/Analytic/ReflectedSpectrum/NegativeSquareLaplaceResolvent.stabilizationGap
• Dependency: D5/S3/Analytic/Adelic/ReflectedGrowthPairSecondOrderSpectrum