Prime Reciprocal-Log Approximation

Abstract

Prime reciprocal logarithms approximate positive offsets with quadratic error.

Theorem 1.1 (A single prime sees every positive offset).

$$(\forall delta:\mathbb{R},0<delta\Rightarrow \exists Y:\mathbb{R},N,q:\mathbb{N},Y=\exp (\frac{1}{delta})\wedge N=\mathrm{natCeil}(Y)\wedge \mathrm{Prime}(q)\wedge N<q\wedge q\le 2\times N\wedge 2\times N\le 4\times Y\wedge \frac{1}{delta}<\log (q)\wedge \log (q)\le \frac{1}{delta}+\log (4)\wedge 0\le delta-\frac{1}{\log (q)}\wedge delta-\frac{1}{\log (q)}<\log (4)\times delt{a}^2)\wedge (\mathrm{IsBigO}((delta\mapsto \mathrm{infDist}(delta,primeReciprocalLogSpectrum)),\mathrm{nhdsWithin}(0,\mathrm{Ioi}(0)),(delta\mapsto delt{a}^2))).$$

Proof. Machine-checked in Lean as D5/S3/AnalyticClosure/PrimeReciprocalLogApproximation.prime_reciprocal_log_quadratic_approximation (✓ std3). ∎

Source. Repository-derived.

Commentary.

For every positive real offset delta, set Y = exp(1/delta) and N = ceil(Y). Bertrand’s theorem supplies a prime q between N and 2N, while the ceiling estimate puts 2N below 4Y.

Monotonicity of the logarithm gives the displayed logarithmic window. Taking reciprocals then yields a nonnegative error strictly below log(4) times delta squared.

The same witnesses bound the infimum distance to the set of prime reciprocal logarithms, proving the right-hand big-O statement at zero. No uniform nearest-prime selector is asserted.

References

• Truth anchor: D5/S3/AnalyticClosure/PrimeReciprocalLogApproximation.prime_reciprocal_log_quadratic_approximation