What question did this study set out to answer?

This work seeks to transition from asymptotic bounds of the Selberg sieve to more precise geometric properties.

June 4, 2026Open Access

Rigidity of the Selberg Majorant: Stability, Restriction, and a Quadratic Form Identity with Machine-Verified Proofs

Key Points

This work seeks to transition from asymptotic bounds of the Selberg sieve to more precise geometric properties.
Analyses the Selberg majorant on finite geometry to uncover scalar invariant behavior.
Employs Cauchy–Schwarz to derive a universal lower bound on the mass-energy product.
Formalizes all findings in Lean 4 for complete mathematical rigor.
Confirmed that the optimal Selberg weight satisfies interlocking stability and restriction constraints.
Established a strict pointwise Lipschitz bound linking prime-level perturbations to composite numbers.
Proved that the $L^2$ norm coincides with the Selberg quadratic form evaluated using divisor sums.

Abstract

This paper shifts the focus of the Selberg sieve from asymptotic bounds to exact, finite geometry. By analyzing the Selberg majorant as a discrete object on Fin (N), we uncover the structural rigidity governing its scalar invariants. We prove that the optimal Selberg weight (d = -1/2) simultaneously satisfies three interlocking constraints: Kinetic Stability: Prime-level perturbations in the sieve density propagate to composite numbers and Euler products with a strict pointwise Lipschitz bound. Universal Restriction: We establish a universal lower bound on the mass-energy product (mass² \|\|₂²) for any non-negative majorant dominating a sifted indicator, derived entirely from Cauchy–Schwarz. Quadratic Form Identity: The spatial L² norm of the majorant perfectly coincides with the arithmetic Selberg quadratic form evaluated via divisor sums in the single-prime model. 100% Machine-Verified Every theorem, lemma, and arithmetic inequality in this paper is fully formalized in Lean 4 (Mathlib). The repository contains the complete proof chain with zero sorry statements, guaranteeing absolute mathematical rigor from foundational definitions to the final restriction bounds. Keywords: Selberg sieve, Majorant, Kinetic stability, Restriction lower bound, Formal verification, Lean 4.

Ask AI

Helpful

Bookmark

View Full Paper