HEXAGONbeta

Arcs of Π(1+z^p): prime races, the Gaussian core, Dirichlet L-functions and a certified solver for Subset Sum

A mix of human-written and AI-generated textHuman understanding: some partsmath.NT — Number Theorycs.DS — Data Structures and Algorithmscs.CC — Computational Complexitymath.PR — Probabilitymath.CO — Combinatorics

Contributed by Antonio Mennillo ↗

Version 1 / Nov 04, 2026 / CC BY 4.0

Abstract

The subsets of {1}∪{p≤N}\{1\} \cup \{p \le N\} reach every integer between 0 and their total, by Bertrand's postulate, so deciding whether a target is a subset sum of the primes is trivial. Counting the solutions is not: the count carries the arithmetic of the primes. We study the generating function FN(z)=Π(1+zw)F_N(z) = \Pi(1 + z^w) on the unit circle and follow one object, the arc at a rational a/qa/q, through three settings. For the primes, the centre of the arc a/qa/q rises above the sea of the minor arcs exactly when q=2k(k≥2)q = 2^k (k \ge 2) or q=2pjq = 2p^j, with excess Λ(q/2)/φ(q)\Lambda(q/2)/\varphi(q), and the neighbourhoods of all the other arcs are bounded uniformly in qq; Theorem E gives the expansion arc by arc. The height of an arc is a race of the primes modulo qq with weights log⁡∣cos⁡(πra/q)∣\log |\cos (\pi ra/q)|. By Landau's theorem a one-sided bound on it is equivalent to GRH for the even characters it sees, unconditionally at q=8q = 8, 10 and 14, where the zero-free segments it needs are certified; at q=14q = 14 the race changes sign infinitely often. The principal arc carries ζ\zeta in the centre and width of its Gaussian. For arbitrary weights, the arcs become the decision rule of a Subset Sum solver that reads them on the original weights and ends with a meet-in-the-middle filtered by a random residue class. Every answer it returns is verified. The dummy weights of HURS explain why the reading is exact: they blur the counts by a flat window, and the blur is invertible on counts, though not on reachable sets. On random weights of bb bits the method has rigorous guarantees, in time 2b/2+o(b)2^{b/2+o(b)} and, with the filter, 2b/3+o(b)2^{b/3+o(b)}, resting on a local limit theorem uniform in the size of the weights and on a concentration bound for signed subset sums. Finally, the solver is read inside a general theory of constraint propagation, in which every network factors as T=Tcomp∘TstructT = T_{\mathrm{comp}} \circ T_{\mathrm{struct}}.

Provenance statement

AI tools were used for drafting, for the numerical computations and for the Lean formalization. The main results are formalized in Lean 4 with Mathlib in the public repository github.com/anthem87/arcs-algo (AGPL-3.0-or-later; the version described in the paper is commit 372ba68), with no sorry and only the standard axioms; published classical theorems and numerical certificates (Arb) enter as explicit hypotheses. The formalization is under review on the Palomar registry. The paper is archived on Zenodo, doi:10.5281/zenodo.23912385.

Tools used

Lean FRO
Lean 4 (proof assistant)Version v4.36.0-rc2
Mathlib community
Mathlib (proof assistant library)
FLINT
Arb / python-flint (certified computation)
mpmath
mpmath (certified computation)

References

No bibliography entries.

Version history

  1. v1Submitted by Antonio MennilloInitial depositCurrentNov 03, 2026