Haglund's Zero-Trajectory Conjecture for the First Riemann Xi Approximant

Haglund's Conjecture 4 reads: for $k\ge1$ , the imaginary part of each non-real zero of $\Xi_k(z)+t\Phi_{k+1}(z)$ decreases monotonically as $t$ goes from 0 to 1, where the $\Phi_n$ are the incomplete-gamma summands of Riemann's series for $\Xi$ and $\Xi_k=\sum_{n\le k}\Phi_n$ . This work proves the case $k=1$ , the pencil $\Phi_1+t\Phi_2$ : every non-real zero in the closed first quadrant is simple and the imaginary part of its analytic branch strictly decreases. It adds two statements Conjecture 4 does not itself assert - no non-real branch escapes to infinity on a bounded forward parameter interval, and at a real collision of any finite multiplicity the full local Weierstrass-Puiseux multiset stays real to the right. The cases $k\ge2$ remain open, and nothing is claimed about the zeros of $\Xi$ or the Riemann hypothesis.

Result: Proved(see note)
Status: Candidate (review pending)
AI contribution: AI co-developed
Method: Computation
Field: Analytic number theory and entire-function zero dynamics
Posed by: James Haglund
Year posed: 2009
Years open: 17y
Solved: 2026-08-22
Model: OpenAI GPT-5 (Codex)
Vendor: OpenAI
Collaborators: —
Verification: Unreviewed
Publication: Preprint
Significance: 8 / 100
Disclosed cost: —
Wikipedia: No dedicated article

What was actually shown

Proves Haglund's Conjecture 4 for $k=1$ : every non-real first-quadrant zero of $\Phi_1+t\Phi_2$ is simple with strictly decreasing imaginary part, no branch escapes forward, and every finite-multiplicity real collision stays real afterwards. The cases $k\ge2$ remain open. Two readings worth separating: Conjecture 4 asserts the monotone descent alone, so the no-escape and stays-real statements are this paper's own additions rather than Haglund's text, and they are the stronger part of the theorem. The descent itself, part (i), is the part that rests on the unavailable interval-arithmetic certificate.

What the AI did

The paper's disclosure, in full: "AI systems were used extensively in mathematical derivation, Lean proof development, literature discovery, organization, and typesetting. The author remains responsible for every mathematical statement, proof, citation, and submission decision." That is substantive - mathematical derivation, not just writing - but it names no model and attributes no specific step, so under this site's rule that a vague disclosure takes the lower tier it supports co-development rather than the AI-discovered tier the submission claimed. The stronger account, that Codex produced the central proof strategy and the analytic arguments connecting the interval certificate to the global theorem, was given to this site on submission and appears nowhere in the paper. The model string is the submitter's as well: the manuscript names no system at all.

Verification

The Lean was read here on 24 August 2026 at mbaccaro-dev/mathematical-proofs: the Solution import closure (Factorization, RootMultiset, RadialEnergy, AbstractRealPersistence) carries no sorry, no admit and no declared axiom, pinned to Lean 4.33.0 and mathlib commit db584cd, with a CI job replaying Comparator, Lean4export, the Lean kernel and NanoDa; the single sorry in Challenge.lean is the comparator hole that file exists to carry. What it verifies is one abstract theorem: right-real persistence of the complete local root multiset at a finite-order analytic collision with inward positive real fibres. The repository's own certificate states that the interval atlas, the literal incomplete-gamma estimates, the global non-real continuation and the assembly into the $k=1$ theorem are not Lean consequences of it, and those are the parts carrying the result. Lean was not compiled here. Unrefereed, and deposited two days before review.

Claim issue

Part (i) of the main theorem rests on the paper's certified first-quadrant proposition, which the paper attributes to a companion verification archive of 238 patches and 60,930 source evaluations. That archive is published nowhere: the Zenodo record carries only the PDF, and the repository carries the manuscript, the Lean project and a Lean preflight script. For a claim filed under the computation method, no reader can replay the computation it rests on.

Sources

Submitted by WildHeron785 on 24 Aug 2026