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

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.