Analysis

Motivation

Since the 2019 revision of the SI, seven constants of nature have fixed, exact numerical values: the caesium hyperfine frequency $\Delta\nu_{\mathrm{Cs}}$, the speed of light $c$, the Planck constant $h$, the elementary charge $e$, the Boltzmann constant $k$, the Avogadro constant $N_A$ and the luminous efficacy $K_{\mathrm{cd}}$. Every other constant is either measured, and then carries an uncertainty, or is a closed-form expression in the seven, and is then known exactly. The CODATA 2022 adjustment (Mohr, Newell, Taylor and Tiesinga, Rev. Mod. Phys. 97, 025002, 2025) is the authoritative statement of which constants fall on which side of that line, and of the statistical procedure that produces the recommended values of the measured ones.

The exactly known side of the line is pure mathematics: the tabulated value of the Stefan-Boltzmann constant, of the radiation constants, of the molar gas constant and of the Faraday constant are theorems about $\pi$, an integral, and rational arithmetic - not measurements. The measured side rests on one statistical object, the weighted linear least-squares fit of $N=133$ input data to $M=79$ adjusted constants, together with the diagnostics ($\chi^2$, the Birge ratio, normalized residuals, expansion factors) the task group uses to decide that the fit is acceptable. This mission formalizes both.

Setting

Write $h$, $c$, $k$, $e$, $N_A$ for the numerical values of the defining constants in coherent SI units, and $\hbar = h/2\pi$. The spectral radiance of a blackbody at thermodynamic temperature $T$, per unit frequency, is Planck's function

$$B_\nu(T,\nu) \;=\; \frac{2h\nu^3}{c^2}\,\frac{1}{e^{h\nu/kT}-1},$$

and per unit wavelength

$$B_\lambda(T,\lambda) \;=\; \frac{2hc^2}{\lambda^5}\,\frac{1}{e^{hc/(\lambda k T)}-1}.$$

The derived constants named in Tables XXXII and XXXIII of the paper are $\sigma = (\pi^2/60)k^4/\hbar^3c^2$ (Stefan-Boltzmann), $c_1 = 2\pi hc^2$ and $c_2 = hc/k$ (radiation constants), $R = N_Ak$ (molar gas), $F = N_Ae$ (Faraday), $K_J = 2e/h$ (Josephson) and $R_K = h/e^2$ (von Klitzing).

For the adjustment, let $A \in \mathbb{R}^{N\times M}$ be the design matrix of the linearized observational equations, $z \in \mathbb{R}^N$ the input data and $W \in \mathbb{R}^{N\times N}$ the weight matrix - the inverse of the covariance matrix of the data, symmetric and positive definite. The fit minimizes

$$\chi^2(x) \;=\; (z - Ax)^{\mathsf T} W (z - Ax), \qquad x \in \mathbb{R}^M,$$

with $\nu = N - M$ degrees of freedom, Birge ratio $R_B = (\chi^2/\nu)^{1/2}$ and normalized residuals $r_i = (X_i - \langle X_i\rangle)/u(X_i)$.

Formalization targets

Goal

$$\int_0^{\infty} \pi\,B_\nu(T,\nu)\,\mathrm{d}\nu \;=\; \sigma T^4 \qquad (T>0), \qquad \sigma = \frac{\pi^2}{60}\frac{k^4}{\hbar^3c^2}.$$

The goal fixes no digits: it asserts that the constant appearing in the tabulated closed form is exactly the one produced by integrating Planck's law over the spectrum and over a Lambertian hemisphere. The numerical enclosure of $\sigma$ is a separate, weaker milestone, so that the goal survives any change of tabulated digits.

Supporting targets

$$\int_0^\infty \frac{x^3}{e^x-1}\,\mathrm{d}x = \frac{\pi^4}{15}, \qquad \sigma = \frac{2\pi^5k^4}{15h^3c^2}, \qquad R = N_Ak, \qquad F = N_Ae,$$

together with the numerical enclosures of $\sigma$, of Wien's displacement constants $b = c_2/x_5$ and $b' = x_3k/h$ (where $x_5$, $x_3$ solve $x = 5(1-e^{-x})$ and $x = 3(1-e^{-x})$), and the identity $K_J^2R_K = 4/h$.

On the statistical side:

$$\chi^2(x) \;=\; \chi^2(\hat x) + (x-\hat x)^{\mathsf T}A^{\mathsf T}WA\,(x-\hat x) \quad\text{whenever}\quad A^{\mathsf T}WA\,\hat x = A^{\mathsf T}Wz,$$

the equivalence of minimality with the normal equations, the closed form $\hat x = (A^{\mathsf T}WA)^{-1}A^{\mathsf T}Wz$ when $A^{\mathsf T}WA$ is invertible, and the behaviour of $\chi^2$, $R_B$ and $r_i$ under an expansion factor $f$ applied to the uncertainties.

Significance

The exact-constant statements are what makes the tabulated values checkable rather than authoritative: a reader who accepts the SI definitions can, in principle, re-derive $R = 8.314\,462\,618\,153\,24\ \mathrm{J\,mol^{-1}K^{-1}}$ and $F = 96\,485.332\,123\,310\,0184\ \mathrm{C\,mol^{-1}}$ by arithmetic, and $\sigma = 5.670\,374\,419\ldots\times10^{-8}\ \mathrm{W\,m^{-2}K^{-4}}$ from Planck's law and $\zeta(4)$. Formalizing them turns "in principle" into a machine-checked derivation from the seven fixed numbers.

The least-squares statements make precise what the adjustment is, independently of the 133 data of this particular round: that the recommended values are the unique minimizer of a quadratic form, that the normal equations characterize it, and that multiplying a group of uncertainties by an expansion factor $f$ - the device used in 2022 with $f = 1.7$, $2.5$ and $3.9$ - rescales $\chi^2$ by $f^{-2}$, the Birge ratio by $f^{-1}$ and the residuals by $f^{-1}$, without moving the fitted values. None of these statements is new mathematics; none of them, as far as the catalog shows, is currently available as a machine-checked statement about the CODATA quantities.

Difficulty

Two hard points. First, $\int_0^\infty x^3/(e^x-1)\,\mathrm{d}x = \pi^4/15$: the obvious route expands $1/(e^x-1)$ as a geometric series and integrates term by term, which needs a dominated convergence or monotone convergence argument plus the value $\zeta(4)=\pi^4/90$; interchanging the sum and the integral is the step that must be justified, not assumed. The goal then needs this together with a change of variables $x = h\nu/kT$ on $(0,\infty)$ and an integrability argument for the original integrand.

Second, the numerical enclosures. $5.670\,374\,419\times10^{-8} < \sigma$ requires certified rational bounds on $\pi^5$; the Wien constants require certified bounds on a transcendental root, obtained from interval evaluation of $e^{-x}$ at rational points plus monotonicity of $x - n(1-e^{-x})$. Floating-point evaluation proves nothing here.

The least-squares milestones are routine linear algebra, with one subtlety: the decomposition identity needs symmetry of $W$, and the characterization of minimizers needs positive definiteness, so both hypotheses are carried explicitly.

Formalization scope

All physical quantities are plain real numbers: each constant is the numerical value of the quantity in the coherent SI unit named in its docstring, and the code carries no units. The defining constants are given by the exact decimal literals of Table XXXII, so they are exact rationals; $\hbar$ is defined as $h/2\pi$ and is therefore irrational.

Planck's function is a total function of two real arguments. Outside the physical regime it returns junk rather than failing - at $T = 0$ the exponent is $0$, the denominator $e^0 - 1 = 0$, and Lean's division returns $0$ - so every statement about it carries $0 < T$ and a positivity hypothesis on the spectral variable. The goal's integral is the Bochner integral over $(0,\infty)$ with respect to Lebesgue measure; it is not trivially true by non-integrability, since the integrand is integrable for $T>0$.

The adjustment is formalized over $\mathrm{Fin}\,N$ and $\mathrm{Fin}\,M$ with an arbitrary design matrix $A$ and an arbitrary weight matrix $W$, hypotheses on $W$ (Hermitian, positive definite) stated where they are used rather than baked into the definition; $\nu = N-M$ is an integer, not a truncated natural number.

Contributions welcome: the $\zeta(4)$ integral and the interval-arithmetic enclosures are reusable well beyond this mission, as are the least-squares statements.

Selected references

• P. J. Mohr, D. B. Newell, B. N. Taylor, E. Tiesinga, CODATA recommended values of the fundamental physical constants: 2022, Rev. Mod. Phys. 97, 025002 (2025). https://doi.org/10.1103/RevModPhys.97.025002
• Bureau International des Poids et Mesures, The International System of Units (SI), 9th edition (2019). https://www.bipm.org/en/publications/si-brochure

Motivation

Most equations that arise in applications cannot be solved in closed form: the age of the Moon from a radioactive-decay balance, the deflection of a clamped beam, the equilibrium of a catenary, all reduce to solving $f(x) = 0$ for a function $f$ with no algebraic inverse. A first course in numerical methods therefore opens with root finding: constructive procedures that produce a sequence of approximations $x_0, x_1, x_2, \\dots$ together with a theorem saying that the sequence converges to a root and how fast.

This mission is the first in a series formalizing the lecture notes Métodos Numéricos by Sergio Roberto de Freitas (Departamento de Computação e Estatística, UFMS, 2000). It covers Chapter 3, Zeros de Funções, whose capstone is the local convergence of Newton's method.

Setting

Let $f : \\mathbb{R} \\to \\mathbb{R}$ and let $\\bar{x}$ be a zero of $f$, i.e. $f(\\bar{x}) = 0$. The chapter studies three constructions.

Bisection. Starting from an interval $(a_0, b_0)$ with $f(a_0) < 0 < f(b_0)$, put $x_{k+1} = (a_k + b_k)/2$ and keep the half of $(a_k, b_k)$ on whose endpoints $f$ still changes sign. The width of the bracketing interval is halved at every step.

Linear iteration (MIL). Rewrite $f(x) = 0$ as a fixed-point equation $x = g(x)$ and iterate $x_{n+1} = g(x_n)$ from an arbitrary $x_0$.

Newton's method. Take the particular iteration function

$$g(x) = x - \\frac{f(x)}{f'(x)}, \\qquad x_{n+1} = x_n - \\frac{f(x_n)}{f'(x_n)},$$

obtained by truncating the Taylor expansion of $f$ at $x_n$ after the linear term.

A sequence $x_n \\to \\alpha$ has order of convergence $p$ when $|e_{n+1}| / |e_n|^p$ tends to a finite constant, where $e_n = x_n - \\alpha$; $p = 1$ is linear and $p = 2$ quadratic convergence.

Target

The goal theorem is the local convergence of Newton's method at a simple zero. If $f$ is twice differentiable on an open interval $(a, b)$ containing $\\bar{x}$, its second derivative is continuous there, and $f'$ never vanishes on $(a, b)$, then there is $h > 0$ such that

$$x_0 \\in [\\bar{x} - h, \\bar{x} + h] \\implies x_n \\to \\bar{x},$$

where $x_n$ is the Newton sequence started at $x_0$. This is the formal content of the chapter's statement that Newton's method converges provided the initial guess is chosen close enough to the root.

The milestones are the supporting results of the chapter: the error bound and convergence of bisection, the convergence of the linear iterative method under a derivative bound $|g'| \\le L < 1$, the a posteriori estimate $|\\bar{x} - x_n| \\le \\frac{L}{1-L}|x_n - x_{n-1}|$, and the quadratic order of Newton's method at a simple zero.

Significance

Bisection, fixed-point iteration and Newton's method are the three root finders every numerical-analysis course starts with, and the three convergence theorems above are what justifies using them. The a posteriori estimate is what turns the iteration into an algorithm with a stopping criterion: it bounds the distance to the root by a quantity the program can measure. The quadratic order statement explains the observed doubling of correct digits per step at a simple zero and its loss at a multiple zero.

On the formalization side, Mathlib already has a fixed-point theorem for contractions on complete spaces and the mean value theorem, but not the statements in the form used in numerical analysis: bisection with its explicit $2^{-n}$ bracket, the $\\frac{L}{1-L}$ a posteriori bound, or Newton's local convergence and quadratic rate stated for the concrete iteration sequence. This mission asks for those.

Difficulty

The delicate point in all three theorems is that the iterates must be known to stay in the region where the hypotheses hold; the informal proofs assume this silently. For the linear iterative method the mission therefore states the invariance hypothesis explicitly ($g$ maps the closed interval into itself). For Newton's method, no such hypothesis is given: the existence of a neighbourhood of $\\bar{x}$ that the iteration preserves is part of what must be proved, and it comes from the continuity of $g'$ together with $g'(\\bar{x}) = 0$. The quadratic-order milestone also has to handle the degenerate possibility $x_n = \\bar{x}$, which would put a zero in the denominator; it is excluded by hypothesis.

Formalization scope

Everything is over the real numbers. The iterations are given as explicit recursive sequences: the bisection construction returns the bracketing pair $(a_n, b_n)$ and its midpoint, and there are separate sequences for the fixed-point and Newton iterations. Newton's method takes the derivative as a separate function argument $f'$, tied to $f$ by a hypothesis of the form "$f$ has derivative $f'(x)$ at every $x$ of the interval"; this avoids relying on any junk value of a derivative operator where $f$ fails to be differentiable. Division is total, so a step at a point where $f'$ vanishes would leave the iterate unchanged; the hypotheses exclude this inside the interval.

Two deliberate deviations from the source are worth flagging for the auditor. First, Proposição 3.5.1 assumes $f'(x) \\neq 0$ only for $x \\neq \\bar{x}$, but its proof divides by $f'(\\bar{x})^2$; the formal statement assumes $f' \\neq 0$ on the whole interval, so $\\bar{x}$ is a simple zero. Second, the convergence statement for the linear iterative method adds the hypothesis that $g$ maps the closed interval into itself, without which the iterates may leave the region where the derivative bound is assumed.

Selected references

• S. R. Freitas, Métodos Numéricos, Departamento de Computação e Estatística, Centro de Ciências Exatas e Tecnologia, Universidade Federal de Mato Grosso do Sul, 2000. Chapter 3, Zeros de Funções, pp. 33–70. (Course notes supplied with this mission.)

Motivation

A table of values is all one has of many functions: measurements, tabulated physical constants, the output of an expensive simulation. Interpolation reconstructs a function between tabulated points by passing a polynomial through them, and it underlies much of the rest of numerical analysis — quadrature rules, finite-difference formulas and predictor-corrector schemes for differential equations are all obtained by integrating or differentiating an interpolating polynomial. What makes the reconstruction trustworthy is a formula for the error committed away from the nodes.

This mission is the fifth in a series formalizing the lecture notes Métodos Numéricos by Sergio Roberto de Freitas (UFMS, 2000). It covers Chapter 7, Interpolação.

Setting

Let $x_0 < x_1 < \\dots < x_n$ be distinct nodes and $f_i = f(x_i)$ the tabulated values of a function $f$. The Lagrange form of the interpolating polynomial is

$$P_n(t) = \\sum_{i=0}^{n} f_i L_i(t), \\qquad L_i(t) = \\prod_{j \\neq i}\\frac{t - x_j}{x_i - x_j},$$

so that $P_n(x_i) = f_i$ for every $i$, and $P_n$ is the unique polynomial of degree at most $n$ with this property.

The interpolation error at a point $x$ that is not a node is the difference $f(x) - P_n(x)$.

Target

The goal theorem is Proposição 7.3.1: if $f$ is $n+1$ times differentiable on $(a,b)$ and all nodes lie in $(a,b)$, then for every $x \\in (a,b)$ different from all nodes there exists $\\xi \\in (a,b)$ with

$$f(x) = P_n(x) + \\left(\\prod_{k=0}^{n}(x - x_k)\\right)\\frac{f^{(n+1)}(\\xi)}{(n+1)!}.$$

The milestones are the other results of the chapter needed to make sense of it: the existence and uniqueness of the interpolating polynomial of degree at most $n$ through $n+1$ points with distinct abscissas (Proposição 7.2.1), the fact that the Lagrange formula does interpolate the data, and the practical error bound of Proposição 7.3.2, $|f(x) - P_n(x)| \\le \\frac{M}{(n+1)!}\\prod_k |x - x_k|$ when $|f^{(n+1)}| \\le M$.

Significance

The error formula is the reason interpolation is a numerical method and not just a curve-drawing device: it shows that the error is governed by two independent factors, the smoothness of $f$ through $f^{(n+1)}$ and the geometry of the nodes through the product $\\prod_k(x - x_k)$. Everything downstream follows from it — the $h^2$ and $h^4$ error terms of the trapezoidal and Simpson rules in the next mission are obtained by integrating exactly this expression, and the choice of Chebyshev nodes is the attempt to make the product factor small.

Difficulty

The standard proof introduces the auxiliary function $F(t) = f(t) - P_n(t) - K\\prod_k(t - x_k)$ with $K$ chosen so that $F(x) = 0$, and then applies Rolle's theorem $n+1$ times to conclude that $F^{(n+1)}$ vanishes somewhere. Formalizing the repeated application of Rolle's theorem, keeping track of the $n+2$ distinct zeros and the nested intervals they generate, is the substance of the work; it is an induction that has to be organized carefully rather than a computation.

Formalization scope

The nodes are given as a strictly increasing family $x_0 < \\dots < x_n$ of $n+1$ reals lying in the open interval $(a,b)$, and the interpolating polynomial is the explicit Lagrange sum rather than an abstract polynomial: at a node it is defined by the same formula, whose factors then include $0/0$ contributions unless the nodes are distinct, which is why the distinctness hypothesis appears in the interpolation milestone. Smoothness is expressed as continuous differentiability of order $n+1$ on the open interval $(a,b)$, and the derivative appearing in the error term is the iterated derivative computed within that set; since the set is open this agrees with the ordinary $(n+1)$-st derivative. The evaluation point $x$ is assumed to lie in $(a,b)$ and to differ from every node; the point $\\xi$ is asserted to exist in $(a,b)$, with no claim of uniqueness or of any relation to $x$ beyond membership in the interval. The uniqueness milestone is stated with Mathlib's polynomial type and the degree bound $\\deg \\le n$, which includes the zero polynomial.

Selected references

• S. R. Freitas, Métodos Numéricos, Departamento de Computação e Estatística, Universidade Federal de Mato Grosso do Sul, 2000. Chapter 7, Interpolação, pp. 133–161. (Course notes supplied with this mission.)

Motivation

In the Standard Model the scalar sector consists of a single complex $SU(2)_L$ doublet. The general Two-Higgs-Doublet Model (THDM) replaces it by two complex doublets $\varphi_1,\varphi_2$ of the same weak hypercharge $y=1/2$. This is the minimal extension of the scalar sector that is still renormalisable and gauge invariant, and it is forced on any supersymmetric completion: the Minimal Supersymmetric Standard Model has exactly two Higgs doublets. Before any phenomenology can be done with such a model, two questions have to be answered for the given parameter point: is the scalar potential stable, i.e. bounded from below, and does its global minimum break $SU(2)_L\times U(1)_Y$ down to the electromagnetic $U(1)_{\text{em}}$?

The general THDM potential has $14$ real parameters, and answering these questions directly in field space — eight real scalar degrees of freedom, of which three are gauge — is unwieldy. Maniatis, von Manteuffel, Nachtmann and Nagel (2006) proposed a reformulation in terms of gauge-invariant bilinears, in which the gauge orbits of the Higgs fields are parametrised by a Minkowski-type four-vector confined to the closed forward light cone, and the potential becomes a quadratic polynomial on that cone. In these variables the stability question reduces to a one-variable problem: the sign of an explicit rational function $f(u)$ on a finite set $I$ of at most ten real numbers. This mission formalizes that analysis: the gauge-orbit parametrisation (their Theorem 4), the classification of the stationary points of the potential (their Theorem 2), and the stability criterion itself (their Theorem 1).

Setting

Write the two doublets as rows of a $2\times 2$ complex matrix,

$$\phi=\begin{pmatrix}\varphi_1^+&\varphi_1^0\\ \varphi_2^+&\varphi_2^0\end{pmatrix},$$

and form the hermitian matrix of gauge-invariant scalar products $K^{ij}=\varphi_j^\dagger\varphi_i$, i.e. $K=\phi\,\phi^\dagger$. Decomposing $K$ in the Pauli basis gives four real functions

$$K_0=\operatorname{tr}K,\qquad K_a=\operatorname{tr}\!\left(K\sigma^a\right),\quad a=1,2,3 .$$

Positive semi-definiteness of $K$ is equivalent to $K_0\ge 0$ and $K_0^2-|K|^2\ge 0$: the four-vector $(K_0,K)$ lies on or inside the forward light cone. A gauge transformation acts as $\phi\mapsto \phi\,U^{\mathsf T}$ with $U\in U(2)$, and leaves $K$ invariant.

The most general gauge-invariant renormalisable potential is

$$V=\underbrace{\xi_0K_0+\xi^{\mathsf T}K}_{V_2}+\underbrace{\eta_{00}K_0^2+2K_0\,\eta^{\mathsf T}K+K^{\mathsf T}EK}_{V_4},$$

with real parameters $\xi_0,\eta_{00}\in\mathbb R$, $\xi,\eta\in\mathbb R^3$ and a real symmetric $3\times3$ matrix $E$. For $K_0>0$ one sets $k=K/K_0$, so that $|k|\le 1$, and

$$J_2(k)=\xi_0+\xi^{\mathsf T}k,\qquad J_4(k)=\eta_{00}+2\eta^{\mathsf T}k+k^{\mathsf T}Ek,\qquad V=K_0J_2(k)+K_0^2J_4(k).$$

Stationary points of $J_4$ on the ball $|k|\le1$ are governed by the functions

$$f(u)=u+\eta_{00}-\eta^{\mathsf T}(E-u)^{-1}\eta,\qquad f'(u)=1-\eta^{\mathsf T}(E-u)^{-2}\eta,\qquad g(u)=\xi_0-\xi^{\mathsf T}(E-u)^{-1}\eta,$$

where $u$ is a Lagrange multiplier for the constraint $|k|=1$. The finite set $I$ collects: every regular $u$ with $f'(u)=0$; the point $u=0$ when $f'(0)>0$; and every eigenvalue $\mu$ of $E$ at which $f$ stays finite and $f'(\mu)\ge0$. It has at most ten elements, and $\{f(u):u\in I\}$ is exactly the set of stationary values of $J_4$.

For the stationary points of the full potential one uses four-vector notation $\tilde K=(K_0,K)$, $\tilde\xi=(\xi_0,\xi)$, $\tilde E=\begin{pmatrix}\eta_{00}&\eta^{\mathsf T}\\ \eta&E\end{pmatrix}$ and the metric $\tilde g=\mathrm{diag}(1,-1,-1,-1)$, so that $V=\tilde K^{\mathsf T}\tilde\xi+\tilde K^{\mathsf T}\tilde E\tilde K$ on the domain $\tilde K^{\mathsf T}\tilde g\tilde K\ge0$, $K_0\ge0$, with $\tilde f(u)=-\tfrac14\tilde\xi^{\mathsf T}(\tilde E-u\tilde g)^{-1}\tilde\xi$.

Formalization targets

Goal — Theorem 1 (stability criterion)

For $V_4\equiv0$ the potential is stable for $\xi_0>|\xi|$, marginal for $\xi_0=|\xi|$ and unstable for $\xi_0<|\xi|$. For $V_4\not\equiv0$,

$$f(u_i)>0\ \ \forall u_i\in I\ \Longrightarrow\ J_4>0 \text{ on } |k|\le1 \quad\text{(stability in the strong sense)},$$ $$\exists u_i\in I:\ f(u_i)<0\ \Longrightarrow\ V \text{ unbounded below},$$

and if $f\ge0$ on $I$ with equality somewhere, the sign of $g(u_i)$ — replaced by $g(u_i)-|\xi_\perp(u_i)|\sqrt{f'(u_i)}$ when $u_i$ is an eigenvalue of $E$ — decides between stability in the weak sense and instability.

Milestones

Theorem 4 (gauge orbits); the four stability cases (a), (b.2), (b.3), (b.4) of Section 4 including the criterion $J_2^2\le CJ_4$ for the marginal case; equation (4.39) identifying the stationary values of $J_4$ with $\{f(u):u\in I\}$; equations (4.42)–(4.44) giving $J_2$ at those stationary points; and Theorem 2, the classification of the stationary points of $V$.

Significance

The criterion is a decision procedure: given the $14$ parameters of a THDM, stability is settled by evaluating one rational function at the roots of another, without any search in field space. The authors use it to re-derive the known stability conditions for the MSSM potential and to settle the stability and symmetry-breaking properties of the THDM potential of Gunion et al., for which $\lambda_1+\lambda_3>0$, $\lambda_2+\lambda_3>0$ and $\lambda_4,\kappa>-2\lambda_3-2\sqrt{(\lambda_1+\lambda_3)(\lambda_2+\lambda_3)}$ come out as the strong-stability conditions. Theorem 4 is what makes the whole approach legitimate: it says that nothing is lost in passing from fields to the invariants $(K_0,K)$, because the fibres of that map are exactly the gauge orbits.

The results are established in the published literature; what this mission adds is machine-checked proofs. The statements are not present in Mathlib in any form, and the note added in version 3 of the paper — a condition for the marginal case that was missing in the original version — is a concrete reminder that the case analysis here is easy to get subtly wrong.

Difficulty

The obvious route to stability is to minimise $V$ directly; it fails because the domain is a cone with a boundary, and the minimisation over the boundary $|k|=1$ introduces a Lagrange multiplier whose admissible values are the roots of $f'$, including the degenerate "exceptional" solutions where $E-u$ is singular. Those exceptional solutions are not a technicality: they are where the eigenvalue clauses of $I$, the $\xi_\perp$ correction in (4.43), and the junk-value behaviour of matrix inverses all live. The marginal case ($J_4$ and $J_2$ vanishing simultaneously somewhere) is not decided by the signs alone and needs the quantitative bound $J_2^2\le CJ_4$.

Formalization scope

Vectors in $\mathbb R^3$ are plain functions Fin 3 → ℝ with an explicitly defined dot product; $E$ is a Matrix (Fin 3) (Fin 3) ℝ and its symmetry is carried as a hypothesis. Four-vectors are indexed by Unit ⊕ Fin 3 so that $\tilde E$ and $\tilde g$ are block matrices, with the first component being $K_0$. Higgs configurations are $2\times2$ complex matrices and $K=\phi\phi^\dagger$; a gauge transformation is $\phi\mapsto\phi U^{\mathsf T}$ with $U^\dagger U=1$.

Stability is formalized as the honest statement that $V(K_0,k)$ is bounded from below on the physical domain $K_0\ge0$, $|k|\le1$ — not as any of the sign conditions that the theorem derives — so none of the implications is true by definition. Matrix inversion in Lean returns the zero matrix at a singular argument; every occurrence of $(E-u)^{-1}$ is therefore guarded by a regularity hypothesis, and the values of $f,f',g$ at an eigenvalue of $E$ are defined as limits, with the existence of those limits part of the membership condition for $I$. The projection $\xi_\perp(\mu)$ is characterised by its defining property (it lies in the eigenspace and $\xi-\xi_\perp$ is orthogonal to it) rather than by a choice of eigenbasis.

A complete development needs linear algebra over $\mathbb R$ (resolvents, symmetric matrices, eigenspaces), $U(2)$ and the spectral decomposition of positive semi-definite $2\times2$ complex matrices for Theorem 4, and elementary real analysis (compactness of the ball, limits of rational functions) for Section 4. The gauge-orbit statement and the light-cone parametrisation are reusable for any multi-doublet scalar sector; contributions of the $n$-doublet generalisation (Appendix B, Theorem 5) are welcome as follow-ups.

Selected references

• M. Maniatis, A. von Manteuffel, O. Nachtmann, F. Nagel, Stability and symmetry breaking in the general two-Higgs-doublet model, Eur. Phys. J. C 48 (2006) 805–823. https://arxiv.org/abs/hep-ph/0605184
• J. F. Gunion, H. E. Haber, G. L. Kane, S. Dawson, The Higgs Hunter's Guide, Addison-Wesley, 1990.

Motivation

Given independent random variables $X_1,X_2,\dots$, when does $\sum_n X_n$ converge? Not absolutely — that question is settled by $\sum_n\mathbb{E}|X_n|<\infty$ and is usually too strong. The interesting question is when the partial sums converge for almost every outcome, and here independence buys something that holds for no general sequence: convergence is not a delicate matter of cancellation but is decided, once and for all, by three numerical series.

Chapter 2 of Rick Durrett's Probability: Theory and Examples (Version 5, 2019) reaches this in section 2.5. Kolmogorov's three-series theorem fixes a truncation level $A>0$, replaces each $X_n$ by $Y_n=X_n\mathbb{1}(|X_n|\le A)$, and asserts that $\sum_n X_n$ converges almost surely if and only if

$$\sum_n\mathbb{P}(|X_n|>A)<\infty,\qquad \sum_n\mathbb{E}Y_n \text{ converges},\qquad \sum_n\operatorname{var}(Y_n)<\infty .$$

Three deterministic conditions on the distributions decide an almost-sure question about paths, and the answer does not depend on which $A$ is chosen. Through Kronecker's lemma this is also the route to the strong law of large numbers, which is how the chapter uses it.

Setting

Let $X_1,X_2,\dots$ be independent real random variables on a probability space, with partial sums $S_N=\sum_{n<N}X_n$. Say that $\sum_n X_n$ converges almost surely when for almost every $\omega$ the sequence $S_N(\omega)$ has a real limit; following Durrett, "$\sum a_n$ converges" means $\lim_N\sum_{n\le N}a_n$ exists, not that it converges absolutely.

Three tools from the same section support the theorem. Kolmogorov's maximal inequality strengthens Chebyshev from $\mathbb{P}(|S_n|\ge x)$ to the maximum of the whole path,

$$\mathbb{P}\Bigl(\max_{1\le k\le n}|S_k|\ge x\Bigr)\le x^{-2}\operatorname{var}(S_n),$$

for independent, centred, square-integrable summands. From it comes the convergence criterion: if $\mathbb{E}X_n=0$ and $\sum_n\operatorname{var}(X_n)<\infty$ then $\sum_n X_n$ converges almost surely. Kronecker's lemma is the deterministic bridge to averages: if $a_n\uparrow\infty$ and $\sum_n x_n/a_n$ converges then $a_n^{-1}\sum_{m\le n}x_m\to0$. And the Hewitt–Savage 0-1 law says that for an i.i.d. sequence every permutable event — one unchanged by rearranging finitely many coordinates — has probability $0$ or $1$.

Formalization targets

Goal — Theorem 2.5.8, Kolmogorov's three-series theorem

$$\sum_n X_n \text{ converges a.s.} \iff \begin{cases} \sum_n\mathbb{P}(|X_n|>A)<\infty,\\ \sum_n\mathbb{E}\bigl[X_n\mathbb{1}(|X_n|\le A)\bigr]\ \text{converges},\\ \sum_n\operatorname{var}\bigl(X_n\mathbb{1}(|X_n|\le A)\bigr)<\infty . \end{cases}$$

Both directions are asserted, as Durrett states the theorem. The truncation level $A>0$ is arbitrary and fixed in the statement; that the three conditions hold for one $A$ exactly when they hold for every $A$ is a consequence, not an assumption.

Supporting levels

Kolmogorov's maximal inequality (2.5.5); the convergence criterion under summable variances (2.5.6); Kronecker's lemma (2.5.9); and the Hewitt–Savage 0-1 law (2.5.4).

Significance

The result itself. The three-series theorem is the complete answer to a question that has no complete answer without independence, and the shape of the answer is the interesting part: a pathwise, almost-sure property is equivalent to three conditions each computable from the marginal distributions alone. Each of the three does a separate job — the first says $X_n$ and its truncation differ only finitely often, so Borel–Cantelli lets them be exchanged; the second controls the drift of the truncated sums; the third controls their fluctuation. The theorem is also the standard route to the strong law: applying it to $X_n/n$ and then Kronecker's lemma gives $S_n/n\to\mu$, which is why section 2.5 sits where it does.

Formalizing it. Mathlib has the strong law of large numbers (strong_law_ae), both Borel–Cantelli lemmas, and Kolmogorov's 0-1 law for the tail σ-field. It has none of the following: Kolmogorov's maximal inequality, the almost-sure convergence criterion for random series with summable variances, Kronecker's lemma, the Hewitt–Savage 0-1 law, or the three-series theorem. The mission therefore contributes the whole of section 2.5, and the pieces are reusable well beyond it — the maximal inequality and Kronecker's lemma in particular are standard tools with no probabilistic content in the second case at all.

Difficulty

The maximal inequality is the step where the argument stops being routine. Chebyshev bounds $\mathbb{P}(|S_n|\ge x)$ and no more; controlling the maximum over the whole path needs the first passage decomposition $A_k=\{|S_k|\ge x,\ |S_j|<x \text{ for } j<k\}$ and the observation that $S_k\mathbb{1}_{A_k}$ is measurable with respect to the first $k$ variables while $S_n-S_k$ is independent of them, so the cross terms vanish. That is a stopping-time argument in disguise, and it is what makes the whole section work.

The sufficiency half of the goal is then assembly: the third series and the convergence criterion give $\sum(Y_n-\mathbb{E}Y_n)$ convergent, the second adds the means back, and the first plus Borel–Cantelli replaces $Y_n$ by $X_n$. Necessity is the harder direction, and Durrett does not prove it in Chapter 2 at all — he defers it to Example 3.4.12, where it follows from the Lindeberg–Feller central limit theorem. A solver attacking the goal should expect the reverse implication to need machinery from outside this section.

The Hewitt–Savage law has a difficulty of its own kind: the natural statement is about a σ-field of events on a sequence space, and the proof approximates a permutable event by cylinder events and then applies the permutation that swaps the first $n$ coordinates with the next $n$.

Formalization scope

Random variables are measurable real-valued functions on a probability space and independence is Mathlib's iIndepFun. Variance is Mathlib's variance, and square-integrability is stated as membership in $L^2$ where the maximal inequality and the convergence criterion need it. The three-series theorem itself assumes no integrability: the truncated variables are bounded, so their means and variances exist automatically, which is exactly why the truncation is there.

"$\sum_n a_n$ converges" is formalized as convergence of the sequence of partial sums to a real limit, not as Summable, which in Mathlib means unconditional and hence absolute convergence for real series. This distinction is not pedantic here: condition (ii) of the theorem is convergence of $\sum\mathbb{E}Y_n$ in Durrett's sense and would be a strictly stronger condition if read as summability. Conditions (i) and (iii) are series of non-negative terms, where the two notions agree, and are stated as Summable.

Almost-sure convergence of $\sum_n X_n$ is "for almost every $\omega$ there exists a real $L$ with $S_N(\omega)\to L$" — the limit is not asserted to be measurable in $\omega$, and does not need to be for the statement to say what it should.

For the Hewitt–Savage law the sequence space is the countable product $\mathbb{N}\to S$ carrying the infinite product of copies of one law, which is Mathlib's Measure.infinitePi, and a permutable event is a measurable set invariant under every finitely supported permutation of the coordinates. That is Durrett's exchangeable σ-field stated directly rather than constructed as a σ-field object.

Contributions welcome beyond the listed items: the converse direction via Lindeberg–Feller (Example 3.4.12); the derivation of the strong law from the three-series theorem and Kronecker's lemma; the Marcinkiewicz–Zygmund law (2.5.12); and the rates of convergence of section 2.5.1.

Selected references

• Rick Durrett, Probability: Theory and Examples, Version 5 (January 11, 2019), section 2.5 (pp. 81–90); Theorems 2.5.4, 2.5.5, 2.5.6, 2.5.8, 2.5.9. Published as Cambridge Series in Statistical and Probabilistic Mathematics, 5th edition, 2019, DOI 10.1017/9781108591034
• A. N. Kolmogorov, Grundbegriffe der Wahrscheinlichkeitsrechnung, Springer, 1933.
• E. Hewitt and L. J. Savage, Symmetric measures on Cartesian products, Transactions of the American Mathematical Society 80 (1955), 470–501. DOI 10.1090/S0002-9947-1955-0076206-8
• P. Billingsley, Probability and Measure, 3rd ed., Wiley, 1995, section 22.

Motivation

The Riemann hypothesis asserts that all nontrivial zeros of the Riemann zeta function lie on the critical line. A classical way to measure how far the hypothesis is from failing runs through a one-parameter deformation of the Riemann $\xi$ function by the backward heat flow. De Bruijn (1950) introduced a family of entire functions $H_t$, $t \in \mathbb{R}$, with $H_0$ essentially the $\xi$ function, and showed that $H_t$ has only real zeros for $t \ge 1/2$. Newman (1976) proved that there is a finite constant $\Lambda$, now called the de Bruijn–Newman constant, such that $H_t$ has only real zeros precisely when $t \ge \Lambda$. The Riemann hypothesis is exactly the statement $\Lambda \le 0$, and Newman conjectured the complementary bound $\Lambda \ge 0$ — in his phrase, that if the Riemann hypothesis is true, then it is only barely so.

Timeline of lower bounds on $\Lambda$, all obtained before 2018 by exhibiting Lehmer pairs, that is, pairs of adjacent zeros of $\zeta$ that are unusually close together: $\Lambda > -\infty$ (Newman 1976), $\Lambda \ge -50$ (Csordas–Norfolk–Varga 1988), $\Lambda \ge -5$ (te Riele 1991), $\Lambda \ge -0.385$ (Norfolk–Ruttan–Varga 1992), $\Lambda \ge -0.0991$ (Csordas–Ruttan–Varga 1991), $\Lambda \ge -4.379 \times 10^{-6}$ (Csordas–Smith–Varga 1994), $\Lambda \ge -5.895 \times 10^{-9}$ (Csordas–Odlyzko–Smith–Varga 1993), $\Lambda \ge -2.63 \times 10^{-9}$ (Odlyzko 2000), $\Lambda \ge -1.15 \times 10^{-11}$ (Saouter–Gourdon–Demichel 2011). Rodgers and Tao closed the gap in 2020 by proving $\Lambda \ge 0$. In the other direction, de Bruijn's bound $\Lambda \le 1/2$ was sharpened to $\Lambda < 1/2$ by Ki–Kim–Lee (2009) and to $\Lambda \le 0.22$ by the Polymath 15 project (2019).

Setting

For a real number $u$ put

$$\Phi(u) := \sum_{n=1}^{\infty}\bigl(2\pi^2 n^4 e^{9u} - 3\pi n^2 e^{5u}\bigr)\exp\bigl(-\pi n^2 e^{4u}\bigr),$$

a function that decays super-exponentially as $|u| \to \infty$ and satisfies $\Phi(u) = \Phi(-u)$. For each $t \in \mathbb{R}$ define the entire function

$$H_t(z) := \int_0^{\infty} e^{t u^2}\,\Phi(u)\,\cos(z u)\,du .$$

Each $H_t$ is even and satisfies $H_t(\bar z) = \overline{H_t(z)}$; the function $H_0$ is $\tfrac18 \xi\bigl(\tfrac12 + \tfrac{iz}{2}\bigr)$, so the Riemann hypothesis says exactly that every zero of $H_0$ is real. Write

$$S := \{\, t \in \mathbb{R} : \text{every zero of } H_t \text{ is real} \,\},\qquad \Lambda := \inf S .$$

By Pólya and Newman, $S$ is the ray $[\Lambda, \infty)$ with $-\infty < \Lambda \le 1/2$.

When $\Lambda < t \le 0$ the zeros of $H_t$ are real, simple, symmetric about the origin and avoid the origin, so they can be listed as $(x_j(t))_{j \in \mathbb{Z}^*}$, indexed by the nonzero integers, with $0 < x_1(t) < x_2(t) < \cdots$ and $x_{-j}(t) = -x_j(t)$. The classical locations $\xi_j$ are defined for $j \ge 1$ by $\Psi(\xi_j) = j$ with

$$\Psi(T) := \frac{T}{4\pi}\log\frac{T}{4\pi} - \frac{T}{4\pi},$$

extended by $\xi_{-j} = -\xi_j$; they are the positions the zeros would occupy if the Riemann–von Mangoldt counting formula were exact. Throughout, $\log_+ x := \log(2 + |x|)$.

Formalization targets

Goal — Newman's conjecture

$$\Lambda \ge 0, \qquad\text{equivalently}\qquad \text{every } t \text{ with } H_t \text{ having only real zeros satisfies } t \ge 0 .$$

The goal is stated in both forms simultaneously, so that it does not depend on any convention for the infimum of a set that might be empty or unbounded below.

Milestones

The milestone list follows the architecture of Rodgers–Tao, which is a proof by contradiction: every milestone is stated under the standing hypothesis $\Lambda < 0$ of that paper, in the time ranges the paper uses ($\Lambda < t \le 0$, then $\Lambda/2 \le t \le 0$, then $\Lambda/4 \le t \le 0$). In order: an upper bound for $H_t$ near the real axis (Lemma 4); Riemann–von Mangoldt type counting formulae for the zeros of $H_t$ (Theorem 9); the resulting macroscopic description of the zeros (Corollary 10); the equations of motion $\partial_t x_k = 2\sum_{j \ne k} (x_k - x_j)^{-1}$ (Theorem 11); a quantitative lower bound on gaps between zeros (Proposition 13); a bound on the time-integrated renormalized energy (Theorem 17); and a bound on that energy at time $t = 0$ (Proposition 26). The last of these says that at time zero the zeros are, on average, locally in the equilibrium configuration of an arithmetic progression, which contradicts known results on the local distribution of zeros of $\zeta$.

Significance

$\Lambda \ge 0$ settles Newman's conjecture, and together with the Riemann hypothesis it would force $\Lambda = 0$. Unconditionally, it says that the zeros of $\xi$ are not in local equilibrium: infinitely often, gaps between consecutive zeros deviate from the mean spacing, which is what makes the pair correlation phenomenology of Montgomery and of Conrey–Ghosh–Goldston–Gonek–Heath-Brown incompatible with $\Lambda < 0$. Any proof of the Riemann hypothesis must therefore be compatible with the hypothesis being tight in this sense.

The theorem has a complete published proof (Rodgers–Tao, Forum of Mathematics, Pi, 2020); it is not an open problem. What is missing is a machine-checked proof. To the extent the material has been formalized at all, the underlying objects — the $\xi$ function, the heat flow $H_t$, the counting function for zeros, the zero dynamics, the renormalized energies — are not available in Mathlib, so the mission produces reusable analytic infrastructure: bounds for a Fourier–Laplace type integral by the saddle point method, a Riemann–von Mangoldt counting argument via the argument principle, and a gradient-flow monotonicity framework for an infinite particle system with logarithmic interaction.

Difficulty

The obvious route to $\Lambda \ge 0$ is the one used for every previous lower bound: exhibit Lehmer pairs of ever higher quality, since if $\Lambda$ were very negative the zeros of $H_0$ would repel each other and unusually close pairs of zeta zeros could not exist. Producing an infinite sequence of Lehmer pairs of arbitrarily high quality is possible under the GUE hypothesis, but the known unconditional upper bounds for small gaps between zeta zeros are too weak, even assuming the Riemann hypothesis. The proof instead upgrades repulsion to relaxation to local equilibrium: it must control the zeros of $H_t$ uniformly for $\Lambda < t \le 0$ at length scales as fine as $\log T$, with only the weaker counting formulae available for negative $t$ (an error term $O(\log_+^2 T)$ rather than $O(\log_+ T)$), and must make sense of a Hamiltonian and an energy that are given by divergent series, which requires truncation, renormalization, and careful control of all the resulting boundary terms.

Formalization scope

The Lean development commits to the following conventions. $\Phi$ is a tsum over the positive integers and $H_t(z)$ is the Bochner integral over $(0, \infty)$ of $e^{tu^2}\Phi(u)\cos(zu)$; no convergence or entireness statement is built into the definition. $\Lambda$ is sInf of the set of admissible times, and the goal theorem also states the quantifier form "every admissible $t$ is nonnegative", so it cannot be satisfied by a junk value of the infimum. The zero families $(x_j(t))$ and the classical locations $(\xi_j)$ are not defined by choice functions: they enter the milestones as universally quantified functions $\mathbb{Z} \to \mathbb{R}$ subject to explicit predicates saying exactly which sequences they are, so a milestone asserts something about every valid enumeration. Asymptotic notation is unfolded: $O(\cdot)$ becomes an explicit existential constant, $o_{T \to \infty}(\cdot)$ an explicit $\varepsilon$–$T_0$ statement, and a principal value sum a limit of symmetric partial sums. Where a statement asserts the value of a time integral, absolute integrability is part of the conclusion, so the statement cannot be satisfied by the convention that a non-integrable function has integral zero.

One degeneracy is inherent to the source and is stated here explicitly: since the paper argues by contradiction, each milestone carries the hypothesis $\Lambda < 0$ (directly, or through a time range such as $\Lambda < t \le 0$). Once the goal theorem is proved, those hypotheses are unsatisfiable and the milestones become vacuously true. They are the intended attack path on the goal, not independent targets, and a solver who derives one of them from the goal theorem contributes nothing.

Contributions welcome: the analytic estimates for $H_t$ (Lemma 4) and the counting formulae (Theorem 9) are independent of the dynamical part and are the natural entry points; Mathlib-level infrastructure on the argument principle, the saddle point method, and Stirling asymptotics for $\Gamma$ in vertical strips is reusable well beyond this mission.

Selected references

• B. Rodgers and T. Tao, The de Bruijn–Newman constant is non-negative, Forum of Mathematics, Pi 8 (2020), e6. https://doi.org/10.1017/fmp.2020.6
• N. G. de Bruijn, The roots of trigonometric integrals, Duke Math. J. 17 (1950), 197–226. https://doi.org/10.1215/S0012-7094-50-01720-0
• C. M. Newman, Fourier transforms with only real zeros, Proc. Amer. Math. Soc. 61 (1976), 246–251. https://doi.org/10.1090/S0002-9939-1976-0434982-5
• G. Csordas, W. Smith and R. S. Varga, Lehmer pairs of zeros, the de Bruijn–Newman constant $\Lambda$, and the Riemann hypothesis, Constr. Approx. 10 (1994), 107–129. https://doi.org/10.1007/BF01205170
• H. L. Montgomery, The pair correlation of zeros of the zeta function, Proc. Sympos. Pure Math. XXIV (1973), 181–193. https://doi.org/10.1090/pspum/024
• J. B. Conrey, A. Ghosh, D. Goldston, S. M. Gonek and D. R. Heath-Brown, On the distribution of gaps between zeros of the zeta-function, Q. J. Math. 36 (1985), 43–51. https://doi.org/10.1093/qmath/36.1.43
• D. H. J. Polymath, Effective approximation of heat flow evolution of the Riemann $\xi$ function, and a new upper bound for the de Bruijn–Newman constant, Res. Math. Sci. 6 (2019), 31. https://doi.org/10.1007/s40687-019-0193-1

Motivation

Chapter 6 of Walter Rudin's Principles of Mathematical Analysis (3rd edition, McGraw-Hill, 1976) constructs the Riemann–Stieltjes integral $\int_a^b f\,d\alpha$: the Riemann integral with the increments $\Delta x_i$ of the variable replaced by the increments $\Delta \alpha_i = \alpha(x_i) - \alpha(x_{i-1})$ of a monotonically increasing integrator $\alpha$. Taking $\alpha(x) = x$ recovers the ordinary Riemann integral; taking $\alpha$ a step function turns integrals into sums, so series and integrals become special cases of one construction. This is the reason Rudin develops the theory in this generality: it unifies Chapter 3's series with the integral, and it is the natural setting for the Fourier coefficients of Chapter 8.

The chapter's capstone is the fundamental theorem of calculus (Theorem 6.21): an integrable function which is the derivative of some $F$ integrates to $F(b) - F(a)$.

This mission is the sixth in a series formalizing Rudin Chapters 1–11; it uses the uniform continuity of Mission IV and the mean value theorem of Mission V.

Setting

A partition $P$ of $[a,b]$ is a finite set of points $a = x_0 \le x_1 \le \dots \le x_n = b$, with increments $\Delta \alpha_i = \alpha(x_i) - \alpha(x_{i-1})$ for a monotonically increasing $\alpha$. For a bounded real $f$ put $M_i = \sup_{[x_{i-1},x_i]} f$, $m_i = \inf_{[x_{i-1},x_i]} f$, and

$$U(P,f,\alpha) = \sum_{i=1}^n M_i\,\Delta\alpha_i, \qquad L(P,f,\alpha) = \sum_{i=1}^n m_i\,\Delta\alpha_i .$$

The upper and lower integrals are $\inf_P U(P,f,\alpha)$ and $\sup_P L(P,f,\alpha)$; $f$ is integrable with respect to $\alpha$, written $f \in \mathcal{R}(\alpha)$, when they agree, and the common value is $\int_a^b f\,d\alpha$. $P'$ refines $P$ when every division point of $P$ is one of $P'$. Writing $\mathcal{R}$ for $\mathcal{R}(\alpha)$ with $\alpha(x) = x$ gives the Riemann integral $\int_a^b f\,dx$.

Formalization targets

Goal — the fundamental theorem of calculus (Theorem 6.21)

$$f \in \mathcal{R} \text{ on } [a,b], \quad F' = f \text{ on } [a,b] \;\Longrightarrow\; \int_a^b f(x)\,dx = F(b) - F(a).$$

Milestones

$$P' \text{ refines } P \Rightarrow L(P,f,\alpha) \le L(P',f,\alpha),\ U(P',f,\alpha) \le U(P,f,\alpha) \qquad (6.4)$$ $$\underline{\int} f\,d\alpha \le \overline{\int} f\,d\alpha \qquad (6.5)$$ $$f \in \mathcal{R}(\alpha) \iff \forall \varepsilon>0\ \exists P,\ U(P,f,\alpha) - L(P,f,\alpha) < \varepsilon \qquad (6.6)$$ $$f \text{ continuous} \Rightarrow f \in \mathcal{R}(\alpha) \qquad (6.8)$$ $$f \text{ monotone},\ \alpha \text{ continuous} \Rightarrow f \in \mathcal{R}(\alpha) \qquad (6.9)$$ $$\text{linearity of the integral} \qquad (6.12\mathrm{a})$$ $$\text{monotonicity, additivity in the interval, and } \big|\!\int f\,d\alpha\big| \le M(\alpha(b)-\alpha(a)) \qquad (6.12\mathrm{b,c,d})$$ $$\alpha' \in \mathcal{R} \Rightarrow \big(f \in \mathcal{R}(\alpha) \iff f\alpha' \in \mathcal{R}\big),\ \int f\,d\alpha = \int f\alpha'\,dx \qquad (6.17)$$ $$\text{change of variable through a strictly increasing } \varphi \qquad (6.19)$$ $$F(x) = \int_a^x f\,dt \text{ is continuous, and } F'(x_0) = f(x_0) \text{ where } f \text{ is continuous} \qquad (6.20)$$ $$\text{integration by parts} \qquad (6.22)$$

Significance

The fundamental theorem is what makes the integral computable: it reduces integration to antidifferentiation and so links Chapters 5 and 6. Theorem 6.20 is its companion — it says the integral of a continuous function is an antiderivative — and together they show the two operations are mutually inverse to the extent that the hypotheses allow. Theorem 6.17 explains when a Stieltjes integral collapses to a Riemann integral with the density $\alpha'$, and it is the computational tool for integrators that are differentiable; the step-function case at the other extreme (Rudin's 6.15–6.16) is what turns sums into integrals.

Mathlib has no Riemann–Stieltjes integral: it has the Bochner integral, the interval integral, and a Lebesgue–Stieltjes measure, but the upper-and-lower-sum construction of Chapter 6 is absent. This mission therefore builds the object from Rudin's definitions and develops its basic theory; that development is reusable beyond this mission — Chapter 7's interchange theorem (7.16) and Chapter 8's Fourier coefficients are stated with respect to it.

Difficulty

Two obstacles are specific to formalizing this chapter. First, the upper and lower integrals are an infimum and a supremum over the set of all partitions, which is not a lattice-friendly index; every comparison between partitions goes through the common refinement, and Theorem 6.4 is the workhorse that makes such comparisons possible. Second, the fundamental theorem is proved by choosing a partition on which $U - L < \varepsilon$ and applying the mean value theorem on each subinterval, so the proof requires selecting an intermediate point per subinterval — a finite choice that is easy on paper and must be organized explicitly in Lean.

The integrator $\alpha$ is only assumed monotone, so it may be discontinuous, and the theory must not assume otherwise: Theorem 6.9 needs continuity of $\alpha$ precisely because it is not available in general.

Formalization scope

Conventions fixed by this mission:

• A partition of [a, b] is Rudin.Partition a b: the number n of subintervals together with a monotone placement function x with x 0 = a and x n = b. Rudin allows $x_{i-1} = x_i$, and so does this structure.
• Rudin.upperSum, Rudin.lowerSum, Rudin.upperIntegral, Rudin.lowerIntegral, Rudin.RSIntegrable, Rudin.RSIntegral follow Definitions 6.1–6.2 literally, with sSup and sInf over the images $f([x_{i-1},x_i])$.
• Since sSup/sInf on ℝ return 0 on unbounded sets, every statement carries Rudin's boundedness hypothesis for $f$ explicitly; likewise monotonicity of $\alpha$ is assumed as MonotoneOn α (Set.Icc a b) rather than built into a type.
• Rudin.RiemannIntegrable and Rudin.RiemannIntegral are the case $\alpha = \mathrm{id}$, in which the goal theorem and Theorems 6.20–6.22 are stated, matching Rudin.
• Derivatives are HasDerivAt, so F' = f is stated pointwise on [a, b] with the value f x supplied, as in Rudin's hypothesis.

The goal is not vacuous, and not a restatement of a library lemma: the integral in it is the one defined in this mission, so a solution must connect the upper/lower sum construction to differentiation rather than quoting Mathlib's interval integral.

Selected references

• Walter Rudin, Principles of Mathematical Analysis, 3rd edition, McGraw-Hill, 1976, Chapter 6 (pp. 120–142).