Add Hu (2026) Gauss circle bound 573/914

[hxypqr]

This adds the Gauss-circle bound from Xiyu Hu's 2026 preprint to the blueprint, together with a bibliography entry and an external Lean formalization link. The change is limited to two files. Li–Yang's statement and historical entry are retained, and the existing historical plot is explicitly labelled as ending in 2023.

Bound and normalization

The manuscript proves, for every $\varepsilon>0$,

$$R(X),\Delta(X)\ll_\varepsilon X^{573/1828+\varepsilon},$$

where $R(X)=#{(m,n)\in\mathbb Z^2:m^2+n^2\le X}-\pi X$. Since ANTEDB uses the radius variable, substituting $X=R^2$ and rescaling $\varepsilon$ gives

$$\theta_2^{\operatorname{Gauss}}\le 2\cdot\frac{573}{1828}=\frac{573}{914}=0.6269146608315098\ldots.$$

Public sources

All links below are pinned to commit 2e2cc1aa2ae937bf7822889fc73b364444aa61b3:

• Manuscript source: A remark on first spacing in Gauss's circle problem and Dirichlet's divisor problem.
• September 8 reference PDF, under the earlier title Amplitude-dependent first spacing and the circle and divisor problems. The repository's publication note explains the title/editorial changes; the theorem statements, estimates, and proofs are unchanged.
• Lean theorem CircleDivisor.EnergyV3.circle_and_divisor_error, proof map, and external-input audit.

Formalization scope

The Lean development checks the manuscript-specific derivation: the first-spacing estimate, parameter inequalities and case splits, exact rational optimization, and reduction to the actual circle and divisor errors.

The final theorem retains four explicit input parameters: Guth–Maldague's amplitude-dependent cone estimate; the fixed-moment Li–Yang arithmetic interface; Graham–Kolesnik reciprocal-phase estimates; and a bundle of five classical inputs. These external propositions are hypotheses, not theorems proved by this repository. The external-input audit records the source matching and remaining manual verification limits, including incomplete full-text checks of Graham–Kolesnik and Vaaler. An axiom audit does not establish those hypotheses.

No Lean code is imported into ExpDB and no \leanok annotation is added. The manuscript also treats the divisor problem, but this PR is limited to the Gauss-circle chapter; a divisor-chapter update is left separate.

Validation

• Exact fraction conversion and git diff --check passed.
• The complete blueprint/src/print.tex compiled with XeLaTeX, BibTeX, and two further XeLaTeX passes. No unresolved references remained. The new theorem, historical table, and bibliography entry were visually checked. BibTeX reported four warnings concerning the existing motohashi_1973 and odlyzko entries.
• All 107 public Lean files were compared with the local cached project and matched after line-ending/encoding normalization; the dependency pins also matched. Fresh runs of Audit.lean and verification/EnergyV3Axioms.lean against that compiled cache passed, with 2,133 exported project theorems using only propext, Classical.choice, and Quot.sound. This was not a fresh full Lean rebuild.