A Lean 4 Algebraic Selberg Sieve Core

This archive contains Version 1.1 of a fully formalised algebraic Selberg sieve core developed in Lean 4, together with complete documentation and an accompanying paper. The project isolates and mechanises the finite, structural components that underlie many classical Selberg–sieve arguments, while deliberately avoiding large-scale analytic number theory. All constructions are finite and unconditional: no asymptotics, infinite sums, or prime distribution results are assumed or proved. At the algebraic level, the development formalises: finite index sets equipped with symmetric real-valued kernels; associated quadratic forms; positive semidefiniteness (PSD) expressed purely via nonnegativity of finite quadratic forms. These components are assembled into Selberg setups that bundle a kernel with a bounded window, weights, and structural constraints. From such data, the code provides a reusable interface for producing Selberg-style average inequalities. A generic, predicate-agnostic average-to-gap combinatorial layer then converts these average bounds into bounded-gap conclusions by purely finite reasoning. The repository includes explicit, fully formalised toy models that exercise the entire pipeline end-to-end inside Lean. These examples are intentionally minimal and serve to validate the correctness and composability of the infrastructure, not to establish new arithmetic results. All results are verified by the Lean 4 kernel. There are no sorry placeholders and no additional axioms beyond the standard classical axioms already present in mathlib (Classical.choice, propext, Quot.sound). An explicit axiom audit is included. This version refines the accompanying paper and documentation, adding: a clear architectural overview of the Selberg core, improved framing of toy examples as API demonstrations, precise definitions of the average predicate and interfaces, and a concrete account of what analytic input would be required to instantiate a genuine Selberg argument at a fixed bound (for example, at gap width 246). The project is intended as verified mathematical infrastructure: a stable, auditable foundation into which future analytic Selberg arguments (e.g. involving primes) could be integrated without modifying the surrounding algebraic or combinatorial machinery. Contents Lean 4 source code (complete, builds cleanly) Accompanying paper (LaTeX source and PDF) Bibliography and developer notes Axiom audit and reproducibility information