$\chi^2(x) = \chi^2(\hat x) + (x-\hat x)^{\mathsf T}A^{\mathsf T}WA(x-\hat x)$

Proved

CODATA2022.chiSquare_decomposition

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

analysismathematical-physicsmetrology

The algebraic identity underlying the whole adjustment. If $\hat x$ solves the normal equations $A^{\mathsf T}WA\hat x = A^{\mathsf T}Wz$ and the weight matrix $W$ is symmetric, then for every parameter vector $x$

\chi^2(x) \;=\; \chi^2(\hat x) \;+\; (x-\hat x)^{\mathsf T}A^{\mathsf T}WA\,(x-\hat x).

The cross terms cancel precisely because of the normal equations, which is why $\chi^2$ at the fitted values is the residual chi-square reported by the adjustment and why any departure from $\hat x$ can only increase it when $A^{\mathsf T}WA$ is positive semidefinite.

Preamble

import Mathlib
import Definitions.Def_CODATA2022_least_squares
open Matrix

Formal statement

namespace CODATA2022
theorem chiSquare_decomposition {N M : ℕ} (A : Matrix (Fin N) (Fin M) ℝ)
    (W : Matrix (Fin N) (Fin N) ℝ) (hW : W.IsHermitian) (z : Fin N → ℝ) (xhat x : Fin M → ℝ)
    (hnormal : (Aᵀ * W * A).mulVec xhat = (Aᵀ * W).mulVec z) :
    chiSquare A W z x
      = chiSquare A W z xhat + (x - xhat) ⬝ᵥ (Aᵀ * W * A).mulVec (x - xhat) := 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 (least-squares adjustment;

\chi^2

of the 2022 adjustment) and Nomenclature entry for

\chi^2

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.

Fix natural numbers $N$ and $M$ (implicit arguments), a real matrix $A$ with $N$ rows and $M$ columns, a real $N\times N$ matrix $W$ , a vector $z \in \mathbb{R}^N$ , and two vectors $\hat x, x \in \mathbb{R}^M$ . Write $\chi^2(y) = (z - Ay)\cdot W(z - Ay)$ for the quantity defined in the definition file.

Two hypotheses are assumed. First, $W$ is Hermitian; over the reals this says exactly $W^{\mathsf T} = W$ . Second, the normal equations hold in the form

\bigl(A^{\mathsf T}WA\bigr)\hat x \;=\; \bigl(A^{\mathsf T}W\bigr)z,

an equality of vectors in $\mathbb{R}^M$ .

The conclusion is the identity of real numbers

\chi^2(x) \;=\; \chi^2(\hat x) \;+\; (x - \hat x)\cdot\Bigl(\bigl(A^{\mathsf T}WA\bigr)(x-\hat x)\Bigr).

No positivity, invertibility or rank condition is imposed on $W$ or $A$ , and $\hat x$ is not asserted to exist or to be unique - it is a given vector assumed to satisfy the displayed equation. The case $N = 0$ or $M = 0$ is included, where all the terms are $0$ .

View graph

χ2(x)=χ2(x^)+(x−x^)TATWA(x−x^)\chi^2(x) = \chi^2(\hat x) + (x-\hat x)^{\mathsf T}A^{\mathsf T}WA(x-\hat x)χ2(x)=χ2(x^)+(x−x^)TATWA(x−x^)

$\chi^2(x) = \chi^2(\hat x) + (x-\hat x)^{\mathsf T}A^{\mathsf T}WA(x-\hat x)$