10 Shared supporting lemmas
These lemmas occur inside several of the Lean proofs. Showing them as separate nodes makes their shared use visible in the dependency graph. Their numbering is separate from the statements of the paper.
For \(r\ne 0\) in a field of characteristic zero, the substitution \(x_1^\prime =x_1+rx_2\), \(x_2^\prime =x_1-rx_2\) has the inverse \(x_1=(x_1^\prime +x_2^\prime )/2\), \(x_2=(x_1^\prime -x_2^\prime )/(2r)\). The linked lemma checks the composition in this direction.
Substitute the two inverse expressions into the original coordinates.
Let \(f=t^3-t^2+at+b\in \mathbb {Q}[t]\) be separable, and suppose that \(f\) either has Galois group \(C_3\) or splits over \(\mathbb {Q}\). Exactly two rational torus points have characteristic polynomial \(f\).
Use the two roots of the quadratic resolvent and their distinctness in the separable case.
Two \(C_3\)-algebras with trace-one normal elements that give the same rational quotient point are isomorphic as pairs.
Identify both pairs with the fibre algebra over their common quotient point.
For the Galois-invariant parameter \((s_0,\sigma ,\sigma )\), interchanging the two conjugate coordinates leaves the support function unchanged.
Compare its values on the cones interchanged by the coordinate swap.
Each of the four sections displayed in Lemma 1 is a weight vector for its listed character.
Identify the section with the corresponding eigen-monomial divided by \(e_1^3\).
Over a field of characteristic zero containing a primitive cube root \(\zeta \), write \(g=u e_0+v e_1+w e_2\) in the idempotent basis of the group algebra. The three character evaluations are \(u,v,w\):
Evaluate the three characters on the three idempotents.
In a commutative ring, if \(\zeta ^2+\zeta +1=0\), then
Expand the cubes and use the relation satisfied by \(\zeta \).
At a finite place, the local height for \(3D_0\) is the square root of the maximum of \(1\) and the absolute values of the three nontrivial weight characters.
The support function is the minimum of the four weight pairings. Exponentiating turns this minimum into the stated maximum.
At each finite prime, the local height factor for \(3D_0\) is one on the integral locus.
Apply the local integral conditions to the four weight values.
If a rational torus point has parameter \(\nu =u+v\zeta \), its characteristic polynomial has integral coefficients exactly when
Substitute the norm and trace in the formulas for the two cubic coefficients.
If an adele has component in the maximal compact subgroup at every prime outside a finite set \(S\), its finite logarithm is the sum of the local logarithms over \(S\).
The logarithm vanishes on each maximal compact subgroup, so all other terms vanish.
For \(\operatorname {Re}(\sigma ){\gt}1\) and \(t\in \mathbb {R}\), the product of the actual local Haar integrals equals the finite Euler product in Lemma 5, with parameter \(\lambda =\sigma -\pi it\).
Identify the local integrands with the evaluated Fourier factors and multiply the convergent factors.
For \(\operatorname {Re}(s_0){\gt}0\) and \(\operatorname {Re}(\sigma ){\gt}0\), the Fourier integral in the logarithm coordinate, with Lebesgue measure, is
Integrate separately on the two half-lines and combine the resulting fractions.
For \(\operatorname {Re}(z){\gt}1/2\),
Bound each deviation by a constant times \(p^{-2\operatorname {Re}(z)}\) and compare with a convergent Dirichlet series.
For every \(\beta {\gt}1/2\) there is a constant \(C_\beta \) such that
Bound the correction products uniformly on the half-plane and bound the factor at \(3\).
The five components of the reduced boundary, in chain order, have self-intersections \(-2,-2,-1,-2,-2\).
Compute the adjacent primitive rays in the resolved fan.
On the minimal resolution, \(D_{\mathrm{red}}^2=-1\).
Add the self-intersections and twice the intersections of adjacent components.
The Euler products and prime sums defining the main-term constants converge and agree with their simplified expressions.
Combine the product identities, logarithmic derivatives, and the evaluation of the Euler–Kronecker constant.
Substituting \(s=2z\) in the Laurent expansion at \(s=2\) changes its polar part to
Use \(2z-2=2(z-1)\) in the Laurent expansion; the remainder stays bounded near \(z=1\).