$\chi^2$ scales linearly in the weight matrix

Proved

CODATA2022.chiSquare_weight_smul

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

analysismathematical-physicsmetrology

Multiplying all uncertainties by an expansion factor $f$ multiplies the covariance matrix by $f^2$ and hence the weight matrix by $f^{-2}$ . The underlying elementary fact is that $\chi^2$ is linear in the weight matrix:

\chi^2_{cW}(x) \;=\; c\,\chi^2_W(x)\qquad\text{for every scalar }c.

In particular the set of minimizers is unchanged for $c>0$ : expansion factors rescale the reported $\chi^2$ and the Birge ratio without moving the recommended values.

Preamble

import Mathlib
import Definitions.Def_CODATA2022_least_squares
open Matrix

Formal statement

namespace CODATA2022
theorem chiSquare_weight_smul {N M : ℕ} (A : Matrix (Fin N) (Fin M) ℝ)
    (W : Matrix (Fin N) (Fin N) ℝ) (z : Fin N → ℝ) (x : Fin M → ℝ) (c : ℝ) :
    chiSquare A (c • W) z x = c * chiSquare A W z x := 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. I.B.12 and Sec. XIV.A: expansion factors 1.7, 2.5 and 3.9 applied to the uncertainties of groups of input data.

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$ , $M$ (implicit), a real $N\times M$ matrix $A$ , a real $N\times N$ matrix $W$ , vectors $z\in\mathbb{R}^N$ , $x\in\mathbb{R}^M$ , and a real scalar $c$ . With $\chi^2_W(x) = (z-Ax)\cdot W(z-Ax)$ , the statement asserts

\chi^2_{cW}(x) \;=\; c\cdot\chi^2_{W}(x),

where $cW$ is the entrywise scalar multiple of $W$ .

There are no hypotheses at all: $c$ may be zero or negative, $W$ need not be symmetric or positive, $A$ is arbitrary, and $N$ or $M$ may be $0$ . The claim is the bilinearity of the quadratic form in its middle argument and says nothing about minimizers.

View graph

χ2\chi^2χ2 scales linearly in the weight matrix

$\chi^2$ scales linearly in the weight matrix