6 The trace-one counts

Let \(F=F_1\) consist of the monic integral trace-one cubics with Galois group \(C_3\). The coefficients \(d_n\) are those of \(Z_0(z)=\sum _{n\geq 1}d_n n^{-z}\). First we remove the split polynomials from the torus-point count. We then estimate the sum of the coefficients and change from toric height to root height. The polynomial \(Q\) is the one in Corollary 1.

Lemma 9 Normality

✓

Let \(K/\mathbb {Q}\) be a \(C_3\)-algebra and let \(x\in K\) have characteristic polynomial \(t^3-e_1t^2+e_2t-e_3\). Then \(x\) is normal if and only if \(e_1(e_1^2-3e_2)\neq 0\).

Proof in Lean ▼

The Gram determinant of the trace pairing on the conjugates of \(x\) is the square of the group determinant. Use its factorization \(\Delta =e_1(e_1^2-3e_2)\) and nondegeneracy of the trace form.

Lemma 10 Removing split polynomials

✓

Let \(d_n\) be the coefficients of \(Z_0(z)=\sum _{n\geq 1}d_n n^{-z}\). For \(X\geq 1\),

\begin{equation*} \sum _{\substack {f\in F\\ { H_{\mathrm{tor}}(f)\leq \sqrt X }}}1 =\frac12\sum _{n\leq X}d_n -\frac{\pi }{9\sqrt3}X+O(\sqrt X). \end{equation*}

Proof in Lean ▼

Use the multiplicities of the characteristic-polynomial map. Count the split points by cyclic orbits of integer triples and compare the corresponding ellipse lattice count with its area.

Equation 30

✓

\begin{equation*} \sum _{\substack {f\in F\\ { H_{\mathrm{tor}}(f)\leq \sqrt X }}}1 =\frac12\sum _{n\leq X}d_n -\frac{\pi }{9\sqrt3}X+O(\sqrt X). \end{equation*}

Proof in Lean ▼

The linked Lean proof establishes this statement.

Lemma 11 A uniform mean-square estimate

✓

Let \(\eta {\gt}0\). For \(1/2\leq \sigma \leq 2\) and \(U\geq 2\),

\begin{equation*} \int _U^{2U}|\xi (\sigma +it)|^2\, dt \ll _\eta U^{1+\eta }. \end{equation*}

Proof in Lean ▼

Apply the residue theorem to an exponentially decaying kernel. A reflected kernel keeps the estimate uniform as \(\sigma \) approaches \(1/2\). Integrate over the height interval and apply the critical-line mean-square bound. The paper instead uses Titchmarsh, [ 30 , § 7.8, (7.8.3) ] .

The proof assumes the Chandrasekharan–Narasimhan estimate (Cited theorem 2).

Equation 31 The strip bound

✓

\begin{equation*} \int _U^{2U}|\xi (\sigma +it)|^2\, dt \ll _\eta U^{1+\eta }. \end{equation*}

Proof in Lean ▼

This is the bound proved in Lemma 11, with the same uniformity in \(\sigma \).

The proof assumes the Chandrasekharan–Narasimhan estimate (Cited theorem 2).

Equation 32

✓

\begin{equation*} \int _1^T|\xi (1/2+it)|^2\, dt \ll T\log ^2T. \end{equation*}

Proof in Lean ▼

The linked Lean proof establishes this statement.

The proof assumes the Chandrasekharan–Narasimhan estimate (Cited theorem 2).

Equation 33 The coefficient sum

✓

For every \(\varepsilon {\gt}0\), the following asymptotic holds as \(X\to \infty \).

\begin{equation*} \sum _{n\leq X}d_n =XQ\left(\tfrac 12\log X\right) +O_\varepsilon (X^{1/2+\varepsilon }), \end{equation*}

Proof in Lean ▼

Apply truncated Perron at a half-integer, move the contour across the double pole at \(1\), and estimate the new contour using the strip mean-square bound. The residue supplies the main term. This is the direct argument retained in Lean in place of [ 1 , Theorem 1.1 ] .

The proof assumes Poisson summation (Equation 15) and the Chandrasekharan–Narasimhan estimate (Cited theorem 2).

Equation 34

✓

For each \(\eta {\gt}0\) there is a constant \(A_\eta \), depending only on \(\eta \), such that the following holds for all \(\sigma \geq 1/2+\eta \).

\begin{equation*} \int _U^{2U}|Z_0(\sigma +it)|\, dt \leq A_\eta \int _U^{2U}|\xi (\sigma +it)|^2\, dt \qquad (U \geq 2). \end{equation*}

Proof in Lean ▼

The linked Lean proof establishes this statement.

Equation 35

✓

For every \(\varepsilon {\gt}0\), the following asymptotic holds as \(X\to \infty \).

\begin{equation*} \sum _{\substack {f\in F\\ { H_{\mathrm{tor}}(f)\leq \sqrt X }}}1 =\frac12XQ\left(\tfrac 12\log X\right) -\frac{\pi }{9\sqrt3}X +O_\varepsilon (X^{1/2+\varepsilon }). \end{equation*}

Proof in Lean ▼

The linked Lean proof establishes this statement.

The proof assumes Poisson summation (Equation 15) and the Chandrasekharan–Narasimhan estimate (Cited theorem 2).