Normalized residuals under an expansion factor: $r_i \mapsto r_i/f$

Proved

CODATA2022.normalizedResidual_expansion_factor

by Lucas · Sep 20, 2026 · Mathlib 0df444a (Lean v4.33.1)

analysismathematical-physicsmetrology

The normalized residual of an input datum is $r = (X - \langle X\rangle)/u(X)$ . Multiplying its standard uncertainty by an expansion factor $f>0$ divides the residual by $f$ :

r \;\longmapsto\; \frac{r}{f}.

This is the criterion the task group applies when choosing expansion factors - in 2022, factors $1.7$ , $2.5$ and $3.9$ were chosen to bring all normalized residuals of the affected groups to $2$ or less.

Preamble

import Mathlib
import Definitions.Def_CODATA2022_least_squares
open Matrix

Formal statement

namespace CODATA2022
theorem normalizedResidual_expansion_factor (X Xadj u f : ℝ) (hf : 0 < f) :
    normalizedResidual X Xadj (f * u) = normalizedResidual X Xadj u / f := by sorry
end CODATA2022

Source

Mohr, Newell, Taylor, Tiesinga, CODATA recommended values of the fundamental physical constants: 2022, Rev. Mod. Phys. 97, 025002 (2025), https://doi.org/10.1103/RevModPhys.97.025002, Sec. XIV.A: expansion factors chosen to reduce the normalized residuals to 2 or less; Nomenclature entry

r_i = (X_i - \langle X_i\rangle)/u(X_i)

Read-back

What the Lean code literally says, in plain math · Aristotle by Harmonic (same agent as the drafter; non-blind)

Disclosure - non-blind read-back. This read-back was written by the same agent that drafted the Lean statement it describes, not by an independent auditor with a fresh context. It is therefore not independent testimony: the writer already knew what the code was intended to say, which is exactly the bias that blind read-backs exist to remove. A reviewer should treat it as the drafter's own restatement of the code and, where independence matters, obtain a genuinely blind read-back before relying on it.

The statement quantifies over four real numbers $X$ , $X_{\mathrm{adj}}$ , $u$ and $f$ and assumes only $f > 0$ . With $r(X,X_{\mathrm{adj}},u) = (X - X_{\mathrm{adj}})/u$ , it asserts

\frac{X - X_{\mathrm{adj}}}{f\,u} \;=\; \frac{1}{f}\cdot\frac{X - X_{\mathrm{adj}}}{u}.

The uncertainty $u$ is unconstrained: it may be zero or negative. When $u = 0$ both sides are $0$ , since division by zero returns $0$ , so the equation still holds. Nothing is assumed relating $X$ and $X_{\mathrm{adj}}$ , and the adjusted value $X_{\mathrm{adj}}$ is an arbitrary real number, not the output of any fit.

View graph

Normalized residuals under an expansion factor: ri↦ri/fr_i \mapsto r_i/fri​↦ri​/f

Normalized residuals under an expansion factor: $r_i \mapsto r_i/f$