Number Theory

Motivation

The main conjecture of Iwasawa theory is an identity between two objects attached to an odd prime $p$ and the tower of cyclotomic fields $\mathbb{Q}(\zeta_{p^{n+1}})$: an algebraic object built from the $p$-parts of their ideal class groups, and an analytic object, the Kubota–Leopoldt $p$-adic $L$-function, which interpolates special values of Dirichlet $L$-functions (generalized Bernoulli numbers). It was formulated by Iwasawa, partly by analogy with Weil's description of the zeta function of a curve over a finite field through the action of Frobenius on its Jacobian: the group $\Gamma$ plays the role of Frobenius, the inverse limit of class groups plays the role of the Jacobian, and the $p$-adic $L$-function plays the role of the zeta function.

Timeline:

• 1932–1976. Herbrand proved that if the $\omega^i$-part of the $p$-class group of $\mathbb{Q}(\zeta_p)$ is nontrivial then $p \mid B_{p-i}$; Ribet (1976) proved the converse using modular forms. Both directions are consequences of the main conjecture.
• 1964–1969. Iwasawa constructed the $p$-adic $L$-functions as power series and formulated the conjecture (Iwasawa 1969); he proved it for primes satisfying the Kummer–Vandiver conjecture.
• 1984. Mazur and Wiles proved the main conjecture over $\mathbb{Q}$ for all odd primes (Mazur–Wiles 1984), modelling the proof on Ribet's.
• 1990. Wiles extended it to totally real fields (Wiles 1990); Rubin later gave a proof over $\mathbb{Q}$ via Thaine's method and Kolyvagin's Euler systems.

Setting

Fix an algebraic closure $\overline{\mathbb{Q}}$ and a prime $p$. For $n \ge 0$ let $F_n = \mathbb{Q}(\mu_{p^{n+1}}) \subset \overline{\mathbb{Q}}$ (Lean: F p n), and let $A_n$ (Lean: A p n) be the $p$-primary part of the ideal class group of $F_n$; by class field theory $A_n \cong H_n = \mathrm{Gal}(L_n/F_n)$, with $L_n$ the $p$-Hilbert class field of $F_n$. The Iwasawa module is

$$H_\infty = \varprojlim_n A_n,$$

the inverse limit along the norm maps $A_{n+1} \to A_n$ (Lean: Hinf p). It is a $\mathbb{Z}_p$-module with a continuous action of $\mathrm{Gal}(\overline{\mathbb{Q}}/\mathbb{Q})$ through $\mathrm{Gal}(F_\infty/\mathbb{Q})$, $F_\infty = \bigcup_n F_n$. Put $V = H_\infty \otimes_{\mathbb{Z}_p} \mathbb{Q}_p$ (Lean: V p).

The cyclotomic character sends $\sigma$ to the unique $c \in \mathbb{Z}_p^\times$ with $\sigma(\zeta) = \zeta^c$ for every $p$-power root of unity $\zeta$. The subgroup $\Delta \cong (\mathbb{Z}/p)^\times$ consists of the elements whose character $c$ is a $(p-1)$-st root of unity, and on $\Delta$ the Teichmüller character is $\omega(\sigma) = c$. Let $V_i$ be the $\omega^i$-eigenspace of $\Delta$ on $V$ (Lean: eigenspace p i). Let $\Gamma = \mathrm{Gal}(F_\infty/F_0) \cong 1 + p\mathbb{Z}_p$, let $\gamma$ be a topological generator, and let $u \in 1 + p\mathbb{Z}_p$ be its cyclotomic character: $\gamma(\zeta) = \zeta^u$. Let $h_p(\omega^i, T) = \det(T - (\gamma - 1) \mid V_i)$, the characteristic polynomial of $\gamma$ on $V_i$ written in the Iwasawa variable $T = \gamma - 1$ (Lean: charPoly p i γ).

On the analytic side, $B_{k,\chi} = p^{k-1}\sum_{a=1}^{p} \chi(a) B_k(a/p)$ is the generalized Bernoulli number of a character $\chi$ modulo $p$. The Kubota–Leopoldt $p$-adic $L$-function satisfies $L_p(\omega^j, 1-k) = -B_{k,\omega^{j-k}}/k$ for $k \ge 1$, and $G_p(\omega^j, T) \in \mathbb{Z}_p[[T]]$ is the power series with $G_p(\omega^j, u^s - 1) = L_p(\omega^j, s)$ (Lean: IsIwasawaPowerSeries p u j G).

Formalization targets

Goal: the main conjecture (Mazur–Wiles)

For every odd integer $i \not\equiv 1 \pmod{p-1}$,

$$\big(h_p(\omega^i, T)\big) = \big(G_p(\omega^{1-i}, T)\big) \quad \text{as ideals of } \mathbb{Z}_p[[T]].$$

Milestones

1. Existence and uniqueness of $G_p(\omega^j, T) \in \mathbb{Z}_p[[T]]$ for even $j \not\equiv 0 \pmod{p-1}$ (Iwasawa).
2. $V$ is a finite-dimensional $\mathbb{Q}_p$-vector space (Iwasawa), so $h_p(\omega^i,T)$ is defined.
3. $h_p(\omega^i, T)$ has coefficients in $\mathbb{Z}_p$.
4. The Herbrand–Ribet theorem: for odd $3 \le i \le p-2$, the $\omega^i$-part of $A_0$ is nontrivial iff $p \mid B_{p-i}$.

Significance

The main conjecture describes the Galois-module structure of the class groups in the whole cyclotomic tower by $p$-adic $L$-functions. The Herbrand–Ribet theorem and the Gras conjecture follow quickly from it, and its generalizations (totally real fields, CM fields, elliptic curves and modular forms, the latter by Skinner–Urban) feed into results on the Birch–Swinnerton-Dyer conjecture. The theorem has been proved (Mazur–Wiles 1984); no machine-checked proof is known. A formal proof requires Iwasawa's structure theory of $\Lambda$-modules, the construction of $p$-adic $L$-functions, and either the Eisenstein-ideal argument of Mazur–Wiles or Rubin's Euler-system argument. Each of these is reusable well beyond this mission.

Difficulty

One divisibility can be reduced, via the analytic class number formula, to the other. The hard direction is to show that the characteristic ideal of the class-group side is divisible by the $p$-adic $L$-function. Stickelberger's theorem gives only annihilation, not the characteristic ideal. Divisibility needs a construction of many unramified abelian $p$-extensions: Ribet's method with Galois representations attached to cusp forms congruent to Eisenstein series, or Kolyvagin–Rubin Euler systems. Neither is in Mathlib today.

Formalization scope

• $F_n$ is the intermediate field of AlgebraicClosure ℚ generated by the roots of $X^{p^{n+1}} - 1$. The groups $A_n$ are the $p$-primary components of ClassGroup (𝓞 (F p n)); the norm maps come from Ideal.relNorm, and the Galois action comes from mapping ideals. The Hilbert class field does not appear: the source's own identification $H_n \cong A_n$ is used.
• $H_\infty$ is the $\mathbb{Z}_p$-submodule of norm-compatible sequences in $\prod_n A_n$. Each finite $p$-group $A_n$ is a $\mathbb{Z}_p$-module through $\mathbb{Z}_p \to \mathbb{Z}/p^{e}$.
• A Galois element $\sigma$ acts on $H_\infty$ by restricting the componentwise action, and $\gamma - 1$ acts on $V_i$ by restriction. The definitions check that these restrictions are possible: a stability or finite-dimensionality hypothesis is tested, with $0$ as the fallback value. These hypotheses always hold, but proving them is left to solvers. In particular $h_p = 0$ if $V_i$ were infinite-dimensional, so the goal includes finite-dimensionality and cannot hold for degenerate reasons.
• $\gamma$ and $u$ are both quantified, linked by "$u$ is the cyclotomic character of $\gamma$" and "$u$ topologically generates $1 + p\mathbb{Z}_p$". $G_p$ is stated existentially: the goal asserts that a power series with the interpolation property exists and generates the same ideal as $h_p$. Such a series is unique (Milestone 1).
• $h_p \in \mathbb{Q}_p[T]$ is compared with $G_p \in \mathbb{Z}_p[[T]]$ through its unique preimage in $\mathbb{Z}_p[T]$.
• Generalized Bernoulli numbers are taken modulo $p$, including for the trivial character. This builds in the Euler factor $1 - p^{k-1}$ and makes the source's formula $L_p(\omega^i, 1-k) = -B_k(\omega^{i-k})/k$ correct for every $k \ge 1$.

Selected references

• B. Mazur, A. Wiles, Class fields of abelian extensions of $\mathbb{Q}$, Invent. Math. 76 (1984), 179–330. https://doi.org/10.1007/BF01388599
• K. Iwasawa, On $p$-adic $L$-functions, Ann. of Math. 89 (1969), 198–205. https://doi.org/10.2307/1970817
• A. Wiles, The Iwasawa conjecture for totally real fields, Ann. of Math. 131 (1990), 493–540. https://doi.org/10.2307/1971468
• L. C. Washington, Introduction to Cyclotomic Fields, 2nd ed., GTM 83, Springer, 1997.
• S. Lang, Cyclotomic Fields I and II, GTM 121, Springer, 1990.
• Wikipedia, Main conjecture of Iwasawa theory, https://en.wikipedia.org/w/index.php?title=Main_conjecture_of_Iwasawa_theory&oldid=1367440598

Motivation

The Selmer group is the main computable invariant attached to the rational points of an elliptic curve (more generally, of an abelian variety) over a number field. J. W. S. Cassels named it in honour of E. S. Selmer, whose numerical work on the curves $ax^3+by^3+cz^3=0$ exposed the limits of descent methods (Selmer 1951). For an elliptic curve $E$ over a number field $K$ and an integer $n\ge 1$, the $n$-Selmer group $\mathrm{Sel}^{(n)}(E/K)$ is a finite group, computable in principle, which contains $E(K)/nE(K)$ and whose remaining part is the $n$-torsion of the Tate–Shafarevich group $\text{Ш}(E/K)$. Finiteness of the Selmer group is the cohomological core of the weak Mordell–Weil theorem, and hence of the Mordell–Weil theorem that $E(K)$ is finitely generated.

Timeline.

• 1951–1954: Selmer studies rational points on cubic curves by two descents and states a conjecture on the number of generators detected by a second descent (Selmer 1951; Selmer 1954).
• 1959–1962: Cassels, in the series Arithmetic on curves of genus 1, introduces the name "Selmer group" and studies its relation with the Tate–Šafarevič group (Cassels 1962).
• 1994: Greenberg extends the notion to $p$-adic Galois representations and motives in Iwasawa theory.

Setting

Let $K$ be a number field with algebraic closure $\bar K$ and absolute Galois group $G_K=\mathrm{Gal}(\bar K/K)$, a profinite group with its Krull topology. Let $E$ be an elliptic curve over $K$, given by a Weierstrass equation, and let $n\ge1$. For a field $L\supseteq K$ write $E(L)$ for the group of $L$-points and $E(\bar L)[n]$ for the $n$-torsion of $E(\bar L)$; the group $G_L$ acts on both.

For a topological group $G$ acting on an abelian group $M$ (regarded as discrete), the continuous first cohomology $H^1(G,M)$ is the group of locally constant maps $c:G\to M$ with $c(gh)=c(g)+g\,c(h)$, modulo the maps $g\mapsto gm-m$.

For each place $v$ of $K$ (finite or infinite), let $K_v$ be the completion, $G_{K_v}=\mathrm{Gal}(\bar K_v/K_v)$, and fix a $K$-embedding $\bar K\hookrightarrow\bar K_v$; it induces the restriction $G_{K_v}\to G_K$ and $H^1(G_K,E[n])\to H^1(G_{K_v},E[n])$. The local Kummer map is

$$\kappa_v: E(K_v)/nE(K_v)\to H^1(G_{K_v},E(\bar K_v)[n]),\qquad P\mapsto[\sigma\mapsto \sigma Q-Q],\quad nQ=P.$$

The $n$-Selmer group is

$$\mathrm{Sel}^{(n)}(E/K)=\bigcap_v \ker\Big(H^1(G_K,E(\bar K)[n])\to H^1(G_{K_v},E(\bar K_v)[n])/\mathrm{im}\,\kappa_v\Big),$$

and the Tate–Shafarevich group $\text{Ш}(E/K)$ is the set of classes in $H^1(G_K,E(\bar K))$ whose restriction to every $G_{K_v}$ is trivial.

Formalization targets

Goal

$$\mathrm{Sel}^{(n)}(E/K)\ \text{is finite}\qquad(n\ge1).$$

Milestones

1. The local identification $H^1(G_{K_v},E[n])/\mathrm{im}\,\kappa_v\cong H^1(G_{K_v},E)[n]$, stated as: $\mathrm{im}\,\kappa_v$ is the kernel of $H^1(G_{K_v},E[n])\to H^1(G_{K_v},E)$, and the image of that map is the $n$-torsion $H^1(G_{K_v},E)[n]$.
2. The exact sequence $0\to E(K)/nE(K)\to\mathrm{Sel}^{(n)}(E/K)\to\text{Ш}(E/K)[n]\to0$.
3. $\text{Ш}(E/K)[n]$ is finite.
4. The weak Mordell–Weil theorem: $E(K)/nE(K)$ is finite.

Significance

The result. Finiteness of $\mathrm{Sel}^{(n)}(E/K)$ gives, through the exact sequence, finiteness of $E(K)/nE(K)$ (weak Mordell–Weil) and of $\text{Ш}(E/K)[n]$. Combined with the theory of heights it yields the Mordell–Weil theorem. The Selmer group is also the object that descent algorithms compute, and the starting point of Iwasawa-theoretic and Bloch–Kato generalisations.

Formalizing it. The finiteness theorem is classical (see e.g. Silverman, Ch. X). A complete development produces continuous Galois cohomology of elliptic curves over number fields, the Kummer sequence, local conditions at all places, and a formal weak Mordell–Weil theorem for arbitrary number fields and arbitrary $n$.

Difficulty

The group $H^1(G_K,E[n])$ itself is infinite, so finiteness can only come from the local conditions, and conditions at all places must be used. The essential input is global arithmetic: the finiteness of the class group and the finite generation of the unit group of a ring of $S$-integers of a finite extension of $K$. The local analysis (behaviour of the Kummer image at places of good reduction not dividing $n$) and the profinite cohomology must both be built for elliptic curves before that input can be applied.

Formalization scope

• $E$ is a WeierstrassCurve K with [E.IsElliptic]; $K$ is a NumberField. The source treats an isogeny $f:A\to B$ of abelian varieties; this mission specialises to elliptic curves and to the isogeny $f=[n]$, $n\ge1$.
• $G_L$ is Field.absoluteGaloisGroup L with its Krull topology. $H^1$ is defined from scratch as locally constant 1-cocycles modulo coboundaries (discrete coefficients).
• Places: finite places are the height-one primes $v$ of $\mathcal O_K$ with completion v.adicCompletion K; infinite places are InfinitePlace K with completion w.Completion. Restriction uses a fixed embedding $\bar K\to\bar K_v$ chosen by IsAlgClosed.lift.
• $\mathrm{Sel}^{(n)}(E/K)$ and $\text{Ш}(E/K)$ are subsets of the cohomology groups. The local condition at $v$ asks that some representative cocycle restrict exactly to $\sigma\mapsto\sigma Q-Q$ with $nQ\in E(K_v)$; this is equivalent to the source's condition because $Q$ may be shifted by an $n$-torsion point.
• The source's exact sequence prints $\mathrm{Sel}^{(2)}$ and $\text{Ш}(A/K)$; the formal statement uses the standard form with $\mathrm{Sel}^{(n)}$ and $\text{Ш}(E/K)[n]$.
• The finiteness of all of $\text{Ш}(E/K)$ (conjectural) and effective computability are not part of the mission.
• Contributions welcome: Galois descent for points, the Kummer sequence, unramified cohomology classes, finiteness of $S$-unit and class-group quotients.

Selected references

• E. S. Selmer, The Diophantine equation $ax^3+by^3+cz^3=0$, Acta Math. 85 (1951), 203–362. https://doi.org/10.1007/BF02395746
• E. S. Selmer, A conjecture concerning rational points on cubic curves, Math. Scand. 2 (1954), 49–54. https://doi.org/10.7146/math.scand.a-10394
• J. W. S. Cassels, Arithmetic on curves of genus 1. III. The Tate–Šafarevič and Selmer groups, Proc. London Math. Soc. (3) 12 (1962), 259–296. https://doi.org/10.1112/plms/s3-12.1.259
• J. H. Silverman, The Arithmetic of Elliptic Curves, 2nd ed., GTM 106, Springer, 2009, Chapter X. https://doi.org/10.1007/978-0-387-09494-6
• Wikipedia, Selmer group (revision 1370673670). https://en.wikipedia.org/w/index.php?title=Selmer_group&oldid=1370673670

Motivation

The nontrivial zeros of the Riemann zeta function $\zeta(s)$ control the distribution of the prime numbers: the explicit formula expresses the error in the prime number theorem as a sum over these zeros. Almost every quantitative argument about primes therefore needs to know how many zeros there are up to a given height. The Riemann–von Mangoldt formula answers this question, and it is used throughout analytic number theory: in explicit prime-counting estimates, in zero-density arguments, in numerical verifications of the Riemann hypothesis, and in the study of the spacing of zeros.

Timeline.

• 1859: Riemann states, without proof, that the number of zeros up to height $T$ is about $\frac{T}{2\pi}\log\frac{T}{2\pi}-\frac{T}{2\pi}$, with a relative error of order $1/T$ ("On the Number of Primes Less Than a Given Magnitude").
• 1905: von Mangoldt proves the formula with error $O(\log T)$.
• 1918: Backlund makes the error explicit for $T>2$, with constants $0.137$, $0.443$, $4.350$ (Acta Math. 41).
• Conditional refinements: under the Lindelöf hypothesis the error is $o(\log T)$, and under the Riemann hypothesis it is $O(\log T/\log\log T)$ (Titchmarsh, Theorems 13.6(A) and 14.13).
• 2022: Hasanalizade, Shen and Wong improve the explicit constants to $0.1038$, $0.2573$, $9.3675$ for $T\ge e$ (J. Number Theory 235, Corollary 1.2).
• The analogous formula $N(T,\chi)=\frac{T}{\pi}\log\frac{qT}{2\pi e}+O(\log qT)$ holds for Dirichlet $L$-functions of primitive characters (Davenport, Multiplicative Number Theory, Ch. 16).

Setting

The Riemann zeta function $\zeta(s)=\sum_{n\ge1}n^{-s}$, defined for $\operatorname{Re}s>1$, extends to a meromorphic function on $\mathbb C$ with a single pole at $s=1$. Its zeros with positive imaginary part all lie in the critical strip $0<\operatorname{Re}s<1$. For real $T$, the zero-counting function is

$$N(T)=\#\{\rho:\ \zeta(\rho)=0,\ 0<\operatorname{Re}\rho<1,\ 0<\operatorname{Im}\rho\le T\},$$

where each zero is counted with its multiplicity. The main term is

$$M(T)=\frac{T}{2\pi}\log\frac{T}{2\pi}-\frac{T}{2\pi}=\frac{T}{2\pi}\log\frac{T}{2\pi e}.$$

For a positive integer $q$ and a Dirichlet character $\chi$ modulo $q$, $L(s,\chi)$ is the analytic continuation of $\sum_{n\ge1}\chi(n)n^{-s}$, and $N(T,\chi)$ counts, with multiplicity, its zeros $\rho$ with $0<\operatorname{Re}\rho<1$ and $-T\le\operatorname{Im}\rho\le T$. The Lindelöf hypothesis asserts $\zeta(\tfrac12+it)=O(t^{\varepsilon})$ for every $\varepsilon>0$, and the Riemann hypothesis asserts that every nontrivial zero has real part $\tfrac12$.

Formalization targets

Goal: the Riemann–von Mangoldt formula

$$N(T)=\frac{T}{2\pi}\log\frac{T}{2\pi}-\frac{T}{2\pi}+O(\log T)\qquad(T\to\infty).$$

This asserts only the shape of the asymptotics, with no numerical constants, so it remains valid however the explicit constants are later improved.

Explicit forms (each implies the goal)

• Backlund: for $T>2$, $\left|N(T)-M(T)-\frac78\right|<0.137\log T+0.443\log\log T+4.350$.
• Hasanalizade–Shen–Wong: for $T\ge e$, $\left|N(T)-M(T)\right|\le0.1038\log T+0.2573\log\log T+9.3675$.

Conditional refinements

• Under the Lindelöf hypothesis: $N(T)=M(T)+o(\log T)$.
• Under the Riemann hypothesis: $N(T)=M(T)+O\!\left(\frac{\log T}{\log\log T}\right)$.

Dirichlet $L$-functions

For every primitive character $\chi$ modulo $q$ and $T\ge2$, uniformly in $q$ and $\chi$:

$$N(T,\chi)=\frac{T}{\pi}\log\frac{qT}{2\pi e}+O(\log qT).$$

Significance

The result itself. The formula shows that the zeros up to height $T$ number about $\frac{T}{2\pi}\log T$, and that their mean spacing at height $T$ is $2\pi/\log T$. It is the normalisation behind pair-correlation statistics, the input that turns zero-free regions into error terms for the prime number theorem, and the bound that makes sums over zeros in the explicit formula converge. Explicit forms such as Backlund's and Hasanalizade–Shen–Wong's are what numerical work uses: they convert a verified count of zeros up to a height into rigorous statements about primes.

Formalizing it. All the targets are classical, proved theorems; none of them is open. What remains is a machine-checked development: the zero-counting function for Mathlib's riemannZeta, the asymptotic formula, its explicit and conditional forms, and the Dirichlet $L$-function analogue. The platform already contains a related dyadic-window statement for $N(T,2T)$ that is conditional on Stirling-type hypotheses. This mission targets the unconditional cumulative count $N(T)$ in its standard form.

Difficulty

The obvious approach counts zeros with the argument principle around the rectangle with vertices $-1$, $2$, $2+iT$, $-1+iT$, using the completed function $\xi(s)$. The contributions of the Gamma factor and of the right-hand edge are routine. The step that does not go through directly is the top edge: one must show that the change in $\arg\zeta(\sigma+iT)$ along $\tfrac12\le\sigma\le2$ is $O(\log T)$. A naive bound on $|\zeta|$ gives no control of the argument. The classical arguments bound the number of sign changes of $\operatorname{Re}\zeta$ on the segment (Backlund's trick via Jensen's formula), or use the Hadamard product with a local zero count. Both need growth estimates for $\zeta$ in the strip, Stirling's formula for complex $\Gamma$, and a careful treatment of $T$ that is the ordinate of a zero. For the explicit bounds, every one of these steps must be carried out with numerical constants. The conditional refinements need the Selberg-type analysis of $S(T)=\frac1\pi\arg\zeta(\tfrac12+iT)$.

Formalization scope

• $\zeta$ is Mathlib's riemannZeta, $L(s,\chi)$ is DirichletCharacter.LFunction, primitivity is DirichletCharacter.IsPrimitive, and the Riemann hypothesis is Mathlib's RiemannHypothesis.
• $N(T)$ (zetaZeroCount) and $N(T,\chi)$ (dirichletZeroCount) are finite sums of multiplicities (analyticOrderNatAt) over the zeros in the open critical strip, with imaginary part in $(0,T]$ and $[-T,T]$ respectively. Zeros on the line $\operatorname{Im}s=T$ are counted.
• The finiteness of each zero set is not assumed. A finsum over an infinite set would be $0$, so a solver must prove finiteness.
• Asymptotic statements use Asymptotics.IsBigO / IsLittleO along Filter.atTop. The Lindelöf hypothesis is the one-sided form $\zeta(\tfrac12+it)=O(t^\varepsilon)$ as $t\to+\infty$, which is equivalent to the two-sided form by conjugate symmetry.
• Decimal constants are exact rationals. Backlund's bound uses $+\tfrac78$, as in Backlund's paper. The source article prints $-\tfrac78$, which appears to be a typo.
• Reusable infrastructure includes: the argument principle on rectangles, Jensen-type zero counts in discs, Stirling's formula for $\log\Gamma$ in vertical strips, convexity bounds for $\zeta$ in the critical strip, and local zero-count lemmas. Contributions of any of these as separate lemmas are welcome.

Selected references

• B. Riemann, Ueber die Anzahl der Primzahlen unter einer gegebenen Grösse, Monatsberichte der Berliner Akademie, 1859.
• H. von Mangoldt, Zur Verteilung der Nullstellen der Riemannschen Funktion ξ(t), Math. Ann. 60 (1905) 1–19.
• R. J. Backlund, Über die Nullstellen der Riemannschen Zetafunktion, Acta Math. 41 (1918) 345–375.
• E. C. Titchmarsh, The Theory of the Riemann Zeta-Function, 2nd ed. (rev. D. R. Heath-Brown), Oxford, 1986. Theorems 9.4, 13.6(A), 14.13.
• H. Davenport, Multiplicative Number Theory, 3rd ed., GTM 74, Springer, 2000. Chapter 16.
• E. Hasanalizade, Q. Shen, P.-J. Wong, Counting zeros of the Riemann zeta function, J. Number Theory 235 (2022) 219–241. https://doi.org/10.1016/j.jnt.2021.06.032
• Wikipedia, Riemann–von Mangoldt formula, revision 1362774495. https://en.wikipedia.org/w/index.php?title=Riemann–von_Mangoldt_formula&oldid=1362774495

Motivation

Multivariate multipoint evaluation asks for the values $f(\alpha_0),\dots,f(\alpha_{N-1})$ of a polynomial $f(X_0,\dots,X_{m-1})$ over a ring $R$, with individual degrees at most $d-1$, at $N$ given points of $R^m$. Kedlaya and Umans showed that, over finite fields and rings $(\mathbb Z/r\mathbb Z)[Z]/(E(Z))$, this problem can be solved in time nearly linear in the input size $d^m + mN$, for $m \le d^{o(1)}$ (Kedlaya–Umans 2008, §4). Through their reduction of modular composition, the computation of $f(g(X)) \bmod h(X)$, to multipoint evaluation (§3 of the same paper), this gives the first nearly-linear-time algorithm for modular composition over finite fields. That in turn gives the fastest known algorithms for factoring univariate polynomials over $\mathbb F_q$, with $O(n^{1.5+o(1)}\log^{1+o(1)} q + n^{1+o(1)}\log^{2+o(1)} q)$ bit operations for a randomized algorithm on degree-$n$ polynomials (abstract and §8).

Timeline. Brent and Kung (1978) gave the $O(n^{(\omega+1)/2})$ baby-step/giant-step algorithm for modular composition (J. ACM 25). Huang and Pan (1997) improved the exponent using fast rectangular matrix multiplication. Kaltofen and Shoup (1998) introduced the factoring framework that the factoring application builds on (Math. Comp. 67). Kedlaya and Umans (2008, SIAM J. Comput. 2011) gave the multimodular algorithm formalized here, together with an algebraic algorithm for small characteristic.

Setting

Let $r \ge 1$ and write $\mathbb Z/r\mathbb Z$ for the integers modulo $r$. Every element of $\mathbb Z/r\mathbb Z$ has a lift, its representative in $\{0,\dots,r-1\}$. For $f \in (\mathbb Z/r\mathbb Z)[X_0,\dots,X_{m-1}]$, $\tilde f \in \mathbb Z[X_0,\dots,X_{m-1}]$ replaces each coefficient by its lift; $\tilde\alpha \in \mathbb Z^m$ lifts a point coordinatewise.

Algorithm MULTIMODULAR with degree parameter $d$ and $t \ge 1$ rounds takes $f$ (degree at most $d-1$ in each variable) and a point $\alpha$. It lists the primes $p_1,\dots,p_k$ at most $\ell = 16\log(d^m(r-1)^{md})$, reduces $\tilde f$ and $\tilde\alpha$ modulo each $p_h$, and evaluates the reductions $f_h(\alpha_h) \in \mathbb F_{p_h}$. It does this directly when $t = 1$, and by recursion with $t-1$ rounds otherwise. It then returns, reduced modulo $r$, the unique integer in $\{0,\dots,p_1\cdots p_k - 1\}$ congruent to $f_h(\alpha_h)$ modulo every $p_h$.

Let $E(Z) \in (\mathbb Z/r\mathbb Z)[Z]$ be monic of degree $e$ and $R = (\mathbb Z/r\mathbb Z)[Z]/(E(Z))$. The lift of $x \in R$ is its representative of degree at most $e-1$, with coefficients lifted to $\{0,\dots,r-1\}$, an element of $\mathbb Z[Z]$. Put

$$M = d^m\bigl(e(r-1)\bigr)^{(d-1)m+1} + 1,\qquad r' = M^{(e-1)dm+1}.$$

Algorithm MULTIMODULAR-FOR-EXTENSION-RING runs in four steps.

1. Lift $f \in R[X_0,\dots,X_{m-1}]$ and $\alpha \in R^m$ to $\mathbb Z[Z]$.
2. Substitute $Z = M$ and reduce modulo $r'$.
3. Run MULTIMODULAR over $\mathbb Z/r'\mathbb Z$, obtaining $\beta$.
4. Form the polynomial $Q(Z)$ whose coefficients are the base-$M$ digits of $\beta$, and return $Q$ reduced modulo $r$ and $E(Z)$.

Formalization targets

Goal: Theorem 4.4 (correctness)

For $E$ monic of degree $e \ge 1$, $m \ge 1$, $d \ge 2$, $t \ge 1$, every $f \in R[X_0,\dots,X_{m-1}]$ of degree at most $d-1$ in each variable, and every $\alpha \in R^m$:

$$\mathrm{MULTIMODULAR\text{-}FOR\text{-}EXTENSION\text{-}RING}_d(f,\alpha,t) = f(\alpha).$$

Milestones

In the order the paper's proofs use them:

1. Lemma 2.4. For every integer $N \ge 2$, $\displaystyle\prod_{p \le 16\log N} p > N$.
2. Magnitude bound (proof of Theorem 4.2). $0 \le \tilde f(\tilde\alpha) \le d^m(r-1)^{md} < p_1\cdots p_k$.
3. Theorem 4.2 (correctness). $\mathrm{MULTIMODULAR}_d(f,\alpha,r,t) = f(\alpha)$ over $\mathbb Z/r\mathbb Z$.
4. Coefficient bound (proof of Theorem 4.4). $\tilde f(\tilde\alpha) \in \mathbb Z[Z]$ has degree at most $(e-1)dm$ and coefficients in $\{0,\dots,M-1\}$.
5. Coincidence (proof of Theorem 4.4). The digit polynomial $Q$ of $\bar f(\bar\alpha)$ equals $\tilde f(\tilde\alpha)$, and the reduction of $\tilde f(\tilde\alpha)$ modulo $r$ and $E(Z)$ is $f(\alpha)$.

Significance

The result makes multivariate multipoint evaluation exact and fast over every finite ring of the form $(\mathbb Z/r\mathbb Z)[Z]/(E(Z))$, which includes every finite field $\mathbb F_q$. Combined with the paper's reduction from modular composition (Theorem 3.1) it yields modular composition of degree-$n$ polynomials over $\mathbb F_q$ in $n^{1+o(1)}\log^{1+o(1)} q$ bit operations (§7). That is the step on which the paper's improvements to univariate polynomial factorization, irreducibility testing and minimal-polynomial computation rest (§§7–8). The same algorithm gives a data structure answering polynomial-evaluation queries in time polylogarithmic in the degree (§5).

The theorem is proved in the paper; nothing in it is open. As far as is known, no part of it has been machine-checked. This mission formalizes the correctness of both algorithms exactly as the paper defines them, step for step, including the Chinese-remainder recombination, the explicit prime threshold $16\log N$, and the base-$M$ digit recovery. Lemma 2.4 is an explicit Chebyshev-type lower bound on the primorial, valid for all $N \ge 2$, and is reusable independently of this mission.

Difficulty

The recursion itself is routine. Two points carry the content. The first is the explicit prime threshold: the algorithm uses only primes up to $16\log N$, so its correctness depends on the explicit inequality of Lemma 2.4 for every $N \ge 2$, not on an asymptotic prime-number estimate. The small cases are part of the claim. The second is the extension-ring step: the integer $\beta$ produced over $\mathbb Z/r'\mathbb Z$ must determine the polynomial $\tilde f(\tilde\alpha) \in \mathbb Z[Z]$ exactly. That needs simultaneous control of its degree and of every coefficient, against the specific constants $M$ and $r'$. A bound on $\tilde f(\tilde\alpha)$ evaluated at a point does not by itself suffice.

Formalization scope

Lean represents $\mathbb Z/r\mathbb Z$ as ZMod r with $r \ge 1$ (NeZero r, excluding ZMod 0 = ℤ), polynomials as MvPolynomial (Fin m) _ with variables indexed $0,\dots,m-1$, and $R$ as AdjoinRoot E for a monic E with $1 \le$ E.natDegree. "Degree at most $d-1$ in each variable" is ∀ i, f.degreeOf i ≤ d - 1. $\log$ is the natural logarithm; the paper does not fix a base, and the natural log is the strongest reading of Lemma 2.4. The primes $p \le x$ for real $x$ are the primes $p \le \lfloor x\rfloor$. Each algorithm is defined for a single evaluation point, since the paper processes the $N$ points independently. The leaf $t = 1$ evaluates $f_h$ at $\alpha_h$ directly; that value is what Theorem 4.1's FFT algorithm outputs. $r'$ is $M^{(e-1)dm+1}$ as printed on p. 15; p. 16 prints $M^{(e-1)(d-1)m+1}$.

The hypotheses $d \ge 2$ and $m \ge 1$ are not written in the paper but are needed. For $r = 2$, $d = 1$, $f = 1$ the threshold $\ell$ is $0$, no prime is used, and MULTIMODULAR returns $0$. For $m = 0$ the inequality $d^m(r-1)^{(d-1)m+1} \le d^m(r-1)^{md}$ and the degree bound $(e-1)dm$ both fail.

Only correctness is formalized. Every running-time bound in Theorems 4.1, 4.2, 4.4 and Corollaries 4.3, 4.5 is out of scope. The Chinese-remainder step and the digit step are defined from the residues and from $\beta$ alone: an algorithm that evaluates $\tilde f(\tilde\alpha)$ in $\mathbb Z$ and reduces it, or that computes $f(\alpha)$ in $R$ directly, would make the theorems trivial and is not the algorithm stated here.

Needed infrastructure: explicit primorial lower bounds (Mathlib has primorial and Chebyshev's $\theta$), the Chinese remainder theorem for several moduli (ZMod.prodEquivPi), bounds on evaluations of polynomials with nonnegative coefficients, and uniqueness of base-$M$ representations of polynomials. Lemma 2.4 and the base-$M$ uniqueness are reusable beyond this mission. Proofs of any milestone are welcome, as are alternative proofs of Lemma 2.4.

Selected references

• K. S. Kedlaya, C. Umans, Fast polynomial factorization and modular composition, Dagstuhl Seminar Proceedings 08381 (version of Aug. 31, 2008). http://drops.dagstuhl.de/opus/volltexte/2008/1777 — published in SIAM J. Comput. 40(6), 2011, https://doi.org/10.1137/08073408X.
• R. P. Brent, H. T. Kung, Fast algorithms for manipulating formal power series, J. ACM 25(4), 1978. https://doi.org/10.1145/322092.322099
• E. Kaltofen, V. Shoup, Subquadratic-time factoring of polynomials over finite fields, Math. Comp. 67, 1998. https://doi.org/10.1090/S0025-5718-98-00944-2
• J. von zur Gathen, J. Gerhard, Modern Computer Algebra, Cambridge University Press, 1999. https://doi.org/10.1017/CBO9781139856065

Motivation

A real number is normal in base $b$ when every block of $k$ base-$b$ digits occurs in its expansion with limiting frequency $b^{-k}$, exactly as it would in a sequence of independent uniformly random digits. It is normal (absolutely normal) when it is normal in every base $b\ge 2$. Whether the classical constants of analysis, above all $\pi$, are normal is one of the oldest open questions linking number theory and probability: it asks whether a number defined by geometry has digits that are statistically indistinguishable from random ones.

Timeline.

• 1909. Borel introduces normality and proves that Lebesgue-almost every real number is normal in every base (Borel 1909). The proof is non-constructive and gives no explicit example.
• 1933. Champernowne gives the first explicit normal numbers. The best known is $0.123456789101112\ldots$, the positive integers written one after another, which is normal in base ten (Champernowne 1933, Theorems I–IV). He conjectures that $0.235711131719\ldots$, built from the primes, is also normal.
• 1946. Copeland and Erdős prove that $0.a_1a_2a_3\ldots$ is normal in base $b$ for every increasing sequence of positive integers $a_n$ that contains more than $N^\theta$ terms up to $N$ for every $\theta<1$ and all large $N$. This settles Champernowne's conjecture for the primes (Copeland–Erdős 1946).
• 1997–2001. The Bailey–Borwein–Plouffe formula computes binary digits of $\pi$ without the earlier ones (BBP 1997). Bailey and Crandall reduce the base-2 normality of $\pi$ to a conjecture on a specific discrete dynamical system (Bailey–Crandall 2001). The conjecture remains open.
• 2002. Becher and Figueira give a computable absolutely normal number (Becher–Figueira 2002).

Large-scale digit computations of $\pi$ are statistically consistent with normality. No base is known in which $\pi$ is normal, and it is not even known that any particular digit occurs infinitely often in its decimal expansion.

Setting

A digit sequence is a function $s:\mathbb N\to\mathbb N$; $s_0$ is the first digit after the point. A word is a finite list $w=(w_0,\dots,w_{k-1})$ of naturals. For $N\in\mathbb N$, the occurrence count $\mathrm{count}(s,w,N)$ is the number of positions $i<N$ with $s_{i+j}=w_j$ for every $j<k$. Overlapping occurrences each count.

The sequence $s$ is normal in base $b$ (IsNormalSeq b s) if, for every word $w$ with all entries $<b$,

$$\lim_{N\to\infty}\frac{\mathrm{count}(s,w,N)}{N}=b^{-|w|}.$$

The $n$-th base-$b$ digit of a real $x$ after the point is

$$\mathrm{digit}_b(x,n)=\lfloor x\,b^{\,n+1}\rfloor \bmod b .$$

The real $x$ is normal in base $b$ (IsNormalReal b x) if $n\mapsto \mathrm{digit}_b(x,n)$ is normal in base $b$. Two remarks:

• The integer part of $x$ plays no role.
• For a rational number with two expansions, the floor selects the one not ending in repeated $(b-1)$'s.

Formalization targets

Goal: $\pi$ is normal

$$\forall\, b\in\mathbb N,\quad b\ge 2\ \Longrightarrow\ \pi \text{ is normal in base } b.$$

This is the conjecture in its standard form, normality in every base. The base-ten case is the special case $b=10$.

Milestones

None are listed. No decomposition of this problem into intermediate statements is known that would be a faithful attack path, and the mission does not invent one. Proposals for intermediate targets are welcome in the discussion; see the contributions listed under Formalization scope.

The known theorems of the subject (Champernowne's constructions, the Copeland–Erdős theorem, Borel's theorem) concern numbers built to be normal or almost every number; they are not steps toward $\pi$ and are kept in the separate mission Explicit normal numbers: Champernowne and Copeland–Erdős.

Significance

A proof that $\pi$ is normal in base $b$ would give every finite digit pattern a definite limiting frequency in its expansion. It would be the first normality result for a classical constant not built to be normal. Every known normal number is constructed digit by digit (Champernowne, Copeland–Erdős, Sierpiński, Becher–Figueira) or shown to exist by a measure argument (Borel). Even the base-2 case would settle the Bailey–Crandall programme for $\pi$.

Formalization status. The goal is open mathematics. The definitions it is stated with are published and are shared with the mission Explicit normal numbers: Champernowne and Copeland–Erdős, where Champernowne's theorems and the Copeland–Erdős theorem have machine-checked proofs.

Difficulty

The constructive results all prove normality from the digit-by-digit description of the number. In particular, the Copeland–Erdős block criterion needs the expansion to be an explicit concatenation of blocks. $\pi$ has no such description. Its known series (Machin-type formulas, BBP) give digits as values of exponential sums, and no known method controls the joint distribution of long digit blocks of such values.

Borel's theorem does not help: it only says that the exceptional set is null, and gives no criterion for deciding whether a given number lies in it. Neither high-precision digit statistics nor irrationality measures for $\pi$ imply normality.

Formalization scope

All declarations live in the namespace Normal and use the definition bundle Normal_Core:

• count, IsNormalSeq, digit, IsNormalReal;
• ofDigits b s $=\sum_n s_n b^{-(n+1)}$;
• the concatenation operators flatten, digitsBE, concatDigits;
• the Champernowne and Copeland–Erdős constants.

Committed conventions:

• Digits are read after the point, with the floor convention above.
• Frequencies are limits of real quotients.
• Words of every length $k\ge0$ are quantified, with entries $<b$.
• The goal ranges over all natural bases $b\ge2$. The degenerate bases $0$ and $1$ are excluded by hypothesis, not by convention.

The definitions agree with Borel's, and the mission does not admit a trivialising reading. A real number is not normal merely because it is irrational, and the empty word imposes only the trivial condition.

The bundle also contains a verbatim copy of the integer-arithmetic definition IsNormal from xiangyazi24/agafonov; its equivalence with IsNormalSeq is proved on the platform (Normal.isNormalSeq_iff_isNormal), so results stated in either form transfer.

Welcome contributions:

• Borel's theorem, via the strong law of large numbers or a Chernoff bound for digit blocks;
• equivalent characterisations of normality, such as Wall's criterion by uniform distribution of $b^n x \bmod 1$ and the reduction from all words to aligned blocks;
• conditional reductions, such as the Bailey–Crandall hypothesis implying base-2 normality of $\pi$.

Selected references

• É. Borel, Les probabilités dénombrables et leurs applications arithmétiques, Rend. Circ. Mat. Palermo 27 (1909), 247–271. https://doi.org/10.1007/BF03019651
• D. G. Champernowne, The construction of decimals normal in the scale of ten, J. London Math. Soc. 8 (1933), 254–260. https://doi.org/10.1112/jlms/s1-8.4.254
• A. H. Copeland and P. Erdős, Note on normal numbers, Bull. Amer. Math. Soc. 52 (1946), 857–860. https://doi.org/10.1090/S0002-9904-1946-08657-7
• D. Bailey, P. Borwein and S. Plouffe, On the rapid computation of various polylogarithmic constants, Math. Comp. 66 (1997), 903–913. https://doi.org/10.1090/S0025-5718-97-00856-9
• D. H. Bailey and R. E. Crandall, On the random character of fundamental constant expansions, Experiment. Math. 10 (2001), 175–190. https://doi.org/10.1080/10586458.2001.10504441
• V. Becher and S. Figueira, An example of a computable absolutely normal number, Theoret. Comput. Sci. 270 (2002), 947–958. https://doi.org/10.1016/S0304-3975(01)00170-0

Motivation

Quasi-Newton methods such as BFGS were designed for smooth objectives, yet in practice they are routinely run on nonsmooth functions and they often work well there: on many nonsmooth problems the iterates converge to a minimizer at a linear rate, measured against the total number of function evaluations. Lewis and Overton (Math. Program. 141 (2013) 135–163) set out to explain this behaviour. Almost nothing about it is proved, so they analyse the simplest cases in detail.

The very simplest case is the subject of this mission: minimizing the absolute value $f(x)=|x|$ on the real line. In dimension one the quasi-Newton update is completely determined by the secant equation, so the method is the classical secant method, combined with a bisection-type Armijo–Wolfe line search. Even here the behaviour is far from obvious. Steepest descent on $|x|$ needs about $(\log_2(1/\epsilon))^2/2$ function trials to reach accuracy $\epsilon$, because the closer the iterate is to zero, the more bisections its fixed-size step needs. The secant method needs only about $\log_2(1/\epsilon)$, the cost of bisection. Lewis and Overton show that the iterates of the secant method trace out an expansion of the starting point as an alternating sum of powers of two, which accounts exactly for the number of trials.

Setting

The objective is $f(x)=|x|$ on $\mathbb R$, with gradient $\operatorname{sgn}(x)$ at every $x\ne0$.

The line search (Algorithm 4.6, p. 147). Given two tests on steps $t>0$, an Armijo test $A$ and a Wolfe test $W$, the line search starts with $\alpha=0$, $\beta=+\infty$ and $t=1$. Each trial examines the current $t$. If $A(t)$ fails, it sets $\beta\leftarrow t$. Otherwise, if $W(t)$ fails, it sets $\alpha\leftarrow t$. Otherwise it stops and returns $t$. The next trial step is $(\alpha+\beta)/2$ when $\beta<+\infty$ and $2\alpha$ otherwise. So the line search doubles until the step is bracketed, then bisects.

The tests of §5.1. At an iterate $x_k$ with direction $p_k$ (where $p_kx_k<0$), take the line search objective $h(t)=|x_k+tp_k|-|x_k|$, the Armijo parameter $c_1=0$, and replace the differentiability check by a termination rule. The conditions become

$$A(t):\ t<-\frac{2x_k}{p_k},\qquad W(t):\ t\ge-\frac{x_k}{p_k}.$$

The secant method. Start at $x_0$ with $H_0=1$. At step $k$ set $p_k=-H_k\operatorname{sgn}(x_k)$, let $t_k$ be the step returned by the line search, and put $x_{k+1}=x_k+t_kp_k$. If $x_{k+1}=0$ the method terminates at the minimizer. Otherwise $H_{k+1}$ is the solution of the secant equation $H_{k+1}y_k=t_kp_k$ with $y_k=\operatorname{sgn}(x_{k+1})-\operatorname{sgn}(x_k)$. The $k$-th line search takes $N_k$ trials. The trial points $z_0,z_1,\dots$ of all line searches, listed in order, give the function trial values $|z_j|$.

Alternating binary expansions. For $x>0$, an alternating binary expansion is a length $m\in\{0,1,2,\dots\}\cup\{\infty\}$ and integers $a_0<a_1<\cdots$ (with $m+1$ terms when $m<\infty$) such that

$$x=\sum_{j=0}^{m}(-1)^j2^{-a_j}.$$

It is canonical if either $m\in\{0,\infty\}$ or its last gap satisfies $a_m\ge a_{m-1}+2$.

Rates (p. 141). A sequence $\tau_k\to\mu$ is Q-linear with rate $r$ if $|\tau_{k+1}-\mu|/|\tau_k-\mu|\to r$. A sequence $\upsilon_k$ is R-linear with rate $r$ if $|\upsilon_k-\mu|\le|\tau_k-\mu|$ for all $k$, for some $\tau$ converging to $\mu$ Q-linearly with rate $r$.

Formalization targets

Goal: Theorem 5.2, secant part (pp. 152–153)

Let $x_0>0$ have the canonical expansion $x_0=\sum_{j=0}^m(-1)^j2^{-a_j}$. Then the secant method from $x_0$ with $H_0=1$ satisfies

$$x_k=\sum_{j=k}^{m}(-1)^j2^{-a_j}\quad(0\le k\le m),\qquad N_0=1+|a_0|,\qquad N_k=a_k-a_{k-1}\ (1\le k<m).$$

If $m<\infty$, the method terminates at zero after finitely many trials. If $m=\infty$, the function trial values $|z_j|$ converge to $0$ R-linearly with rate $\tfrac12$. All four conclusions are exact: the iterates are equal to the tails of the expansion, and the trial counts are equalities.

Milestones

1. §5.1, pp. 151–152. The tests $A$ and $W$ give $|x_{k+1}|<|x_k|$ and $x_kx_{k+1}<0$ whenever $x_k\ne0\ne x_{k+1}$.
2. §5.1, p. 152. For any $H_0>0$: $H_{k+1}=|x_{k+1}-x_k|/2$ and $p_{k+1}=-\tfrac{|x_{k+1}-x_k|}{2}\operatorname{sgn}(x_{k+1})$, and the iterates alternate in sign.
3. Theorem 5.2, first sentence. Every $x>0$ has a canonical alternating binary expansion, and it is unique.
4. §5.1, p. 153. The worked example $x_0=4/7$: $x_{2j}=4/(7\cdot8^j)$, $x_{2j+1}=-3/(7\cdot8^j)$, with trial counts $1,1,2,1,2,\dots$.

Significance

The theorem gives a complete description of a quasi-Newton method on a nonsmooth function, in the one setting where the description is exact. It identifies each iterate, counts every function evaluation, and decides termination. Two things follow. After $a_k$ trials the error is below $2^{-a_k}$, so accuracy $\epsilon$ costs about $\log_2(1/\epsilon)$ trials, compared with the quadratic count for steepest descent. The analysis also shows that choosing the Armijo parameter $c_1=0$ is harmless for $|x|$, which the paper contrasts with the tilted function $\max\{x,-ux\}$. The R-linear rate $\tfrac12$ of all trial values is the one-dimensional instance of the rates the paper observes numerically for BFGS on the Euclidean norm in higher dimensions (§5.2). Those rates remain unexplained.

The result is proved on paper: in Lewis–Overton, with the detailed analysis attributed to the companion report [31]. To our knowledge none of it has been formalized. This mission produces a machine-checked account of an algorithm as executed: a bisection line search counted trial by trial, a secant update, and the number-theoretic fact that this process computes an alternating binary expansion. It also states and fixes the two places where the printed text is inaccurate (see Formalization scope).

Difficulty

The first line search is easy to analyse directly: with $p_0=-1$ it returns the unique power of two in $[x_0,2x_0)$. The difficulty starts with the second. The step returned by Algorithm 4.6 depends on the whole bisection history, and the new direction depends on the previous step through the secant update. The statement therefore has to be proved by an induction that carries an exact invariant. That invariant ties $x_k$, $p_k$ and the line-search bracket to the tail of the expansion, and the trial count to the gap $a_k-a_{k-1}$.

A natural first attempt is to describe each line search as "returns the power of two in the Armijo–Wolfe interval". That does not determine the trial count: the count depends on where the bisection starts and in which order it halves, and it uses the specific directions $p_k$. The R-linear statement adds a further layer. Trial values inside one line search are not monotone, so the dominating Q-linear sequence has to be built over the global trial index, across line searches of different lengths.

The uniqueness half is elementary but needs care. Without canonicity it is false, and a finite expansion has to be told apart from an infinite one.

Formalization scope

• Line search as executed. Algorithm 4.6 is the iteration itself, on states $(\alpha,\beta,t)$ with $\beta\in$ WithTop ℝ. A trial count is the index of the first trial passing both tests, plus one. Every statement about trial counts also asserts that the line search terminates, so the junk value of an empty stopping set cannot be used. The step $t_k$ is not defined as a closed form: that is what the theorem proves.
• The run. The secant run is a recursion on $(x_k,H_k)$, frozen once $x_k=0$. The division defining $H_{k+1}$ is meaningful only when $\operatorname{sgn}x_{k+1}\ne\operatorname{sgn}x_k$, which milestone 1 guarantees. The function trial values are $|z_j|$ for the trial points of all line searches in order, without $|x_0|$; adding it does not affect R-linear convergence.
• Expansions. The length is $m\in$ ℕ∞, the exponents are a : ℕ → ℤ (negative when $x_0>1$), and the powers $2^{-a_j}$ are integer powers. The series is a HasSum whose terms beyond $m$ vanish. Indices start at $0$, as printed.
• Rates. Q-linear convergence requires the ratio to be defined ($\tau_k\ne\mu$ for all $k$). R-linear convergence is exactly the p. 141 definition, domination by a Q-linear sequence, not a bound $C2^{-j}$.
• Corrections to the printed text. (i) Uniqueness of the expansion is false as printed: $1=2^0=2^1-2^0$. Every statement uses canonical expansions, which are unique and are the ones the method follows. (ii) "Arbitrary $x_0$" becomes $x_0>0$, since the expansion is defined only for positive numbers; $x_0<0$ is the mirror image. (iii) "For all $k<m$" in the trial count is read as $1\le k<m$, because $k=0$ is the separate clause $1+|a_0|$. (iv) In the $4/7$ example the printed pattern swaps the one-trial and two-trial line searches, contradicting the preceding sentence and Theorem 5.2; the milestone states the corrected counts $N_{2j}=2$, $N_{2j+1}=1$ ($j\ge1$).
• No trivial reading. The hypotheses are satisfiable for every $x_0>0$ (milestone 3), and the conclusions are equalities about the algorithm's own iterates and trial counts. A formalization in which the line search returns its own answer by definition, or in which the iterates are only bounded, would not prove the theorem.

The development needs only Mathlib's real analysis, tsum/HasSum and filters. The expansion definitions and the R-linear predicate can be reused for other rate statements. Contributions are welcome on the line-search invariant, the trial-count lemmas, and the existence and uniqueness of the canonical expansion.

Selected references

• A. S. Lewis, M. L. Overton, Nonsmooth optimization via quasi-Newton methods, Mathematical Programming Ser. A 141 (2013) 135–163. https://doi.org/10.1007/s10107-012-0514-2
• A. S. Lewis, M. L. Overton, Nonsmooth optimization via BFGS, technical report (reference [31] of the paper, the detailed analysis of the secant method on $|x|$), 2008. http://www.cs.nyu.edu/overton/papers/pdffiles/bfgs_inexactLS.pdf (URL as printed in the paper)
• J. Nocedal, S. J. Wright, Numerical Optimization, 2nd ed., Springer, 2006 (secant equation, Armijo–Wolfe conditions). https://doi.org/10.1007/978-0-387-40065-5