Off-Line Curvature Dipole

Abstract

A reflected pair of logarithmic squared-distance potentials has an explicit zero-mass curvature with a negative core and positive wings.

Theorem 1.1 (A reflected logarithmic pair produces a curvature dipole).

$$\begin{gathered} \forall delta,gamma\in \mathrm{Real}\left(\right), \\ 0<delta\Rightarrow \\ \mathrm{let}potential:=(u,t\mapsto \frac{\log \left((u-delta{)}^2+(t-gamma{)}^2\right)}{2}+\frac{\log \left((u+delta{)}^2+(t-gamma{)}^2\right)}{2}), \\ \mathrm{let}curvature:=(t\mapsto \mathrm{deriv}\left(\mathrm{deriv}\left((u\mapsto potential\left(u,t\right))\right),0\right)), \\ \left(\forall t\in \mathrm{Real}\left(\right),curvature\left(t\right)=2\times \frac{(t-gamma{)}^2-(delta{)}^2}{((t-gamma{)}^2+(delta{)}^2{)}^2}\right)\wedge \left(curvature\left(gamma\right)=-\frac{2}{(delta{)}^2}\wedge \left(\left(\forall t\in \mathrm{Real}\left(\right),curvature\left(t\right)=0\iff \left(t=gamma-delta\vee t=gamma+delta\right)\right)\wedge \left(\mathrm{Integrable}\left(curvature\right)\wedge \left(\mathrm{integral}\left(t,\mathrm{Real}\left(\right),curvature\left(t\right),\mathrm{volume}\left(\right)\right)=0\wedge \left(\left(\forall t\in \mathrm{Real}\left(\right),\left|t-gamma\right|<delta\Rightarrow curvature\left(t\right)<0\right)\wedge \left(\forall t\in \mathrm{Real}\left(\right),delta<\left|t-gamma\right|\Rightarrow 0<curvature\left(t\right)\right)\right)\right)\right)\right)\right). \end{gathered}$$

Proof. Machine-checked in Lean as D5/S3/Analytic/Adelic/OffLineCurvatureDipole.off_line_curvature_dipole (✓ std3). ∎

Source. Repository-derived.

Commentary.

The potential is constructed from the two reflected squared-distance logarithms. The curvature is its second derivative in the normal coordinate at zero, rather than an alias for the target formula.

Direct differentiation supplies the rational expression and its sign profile. A decaying rational primitive proves integrability and zero total mass over the real line.

References

• Truth anchor: D5/S3/Analytic/Adelic/OffLineCurvatureDipole.off_line_curvature_dipole