The normal equations characterize the minimizers of the chi-square statistic
DisprovedCODATA.normal_equationsFor a weighted least-squares problem whose weight matrix is symmetric and strictly positive definite, a parameter vector minimizes the chi-square statistic of the weighted residuals if and only if it solves the normal equations: every column of the design matrix is orthogonal, relative to the weight matrix, to the residual vector. Moreover, if the design matrix has full column rank, then any two solutions of the normal equations coincide. This is the theorem that makes the CODATA adjustment procedure well defined: the adjusted constants of the 2022 report are determined as the solution of the normal equations, and by this equivalence they are exactly the minimizers of the chi-square statistic, uniquely so at full column rank.
import Mathlib import Definitions.Def_CODATA_lsa import Definitions.Def_CODATA_uncert import Definitions.Def_CODATA_values
/-!
# The normal equations characterize the minimizers
Section XII of the 2022 CODATA report describes the determination of
the recommended values as a least-squares adjustment: the adjusted
constants are chosen to minimize the chi-square statistic of the
weighted residuals. This milestone proves the classical equivalence
for the weighted model of `Def_CODATA_lsa`: when the weight matrix is
symmetric and strictly positive definite, the chi-square statistic is
a convex quadratic function of the adjusted constants, so its
minimizers are exactly the solutions of the normal equations; and when
the design matrix has full column rank, the solution of the normal
equations is unique. The milestone is proved on the way to the goal
theorem `CODATA.codata_self_consistent`.
-/
namespace CODATA
/-- For a least-squares problem whose weight matrix is symmetric and
strictly positive definite, the minimizers of the chi-square statistic
are exactly the solutions of the normal equations; and if the design
matrix has full column rank, then any two solutions of the normal
equations coincide. -/
theorem normal_equations {N M : ℕ} (L : LSQ N M) (hG : IsSPD L.G)
(hA : Function.Injective L.A.mulVec) (x : Fin M → ℝ) :
(Minimizes L x ↔ SolvesNormal L x) ∧
∀ z, SolvesNormal L z → z = x := by
sorry
end CODATA
Read-back
What the Lean code literally says, in plain math · glm-5-latest-short
The formal statement fixes a least-squares structure L with N input data and M adjusted constants, assumes the weight matrix G of L is symmetric and strictly positive definite (IsSPD), and assumes the map sending a parameter vector to the design matrix times that vector is injective (full column rank). The conclusion has two parts. First, a parameter vector x minimizes the chi-square statistic if and only if it solves the normal equations, that is, the double sum of the design matrix entries, the weight matrix entries, and the residuals vanishes for every column of the design matrix. Second, any parameter vector z that also solves the normal equations equals x. The statement renders the intended milestone faithfully: the adjustment procedure of the 2022 CODATA report - solving the normal equations - produces exactly the minimizers of the chi-square statistic, and uniquely so. No numerical value of any constant is claimed here.
False as stated. The second conjunct "forall z, SolvesNormal L z -> z = x" is asserted for an arbitrary vector x with no hypothesis that x solves the normal equations. Under hG (symmetric positive definite weight matrix) and hA (injective design matrix) the normal matrix is symmetric positive definite, so a solution z0 exists, and every x different from z0 refutes the conjunct whenever M is at least 1. The docstring (any two solutions coincide) is the intended statement. The corrected theorem CODATA.normal_equations_unique states the uniqueness clause as: for all z w, SolvesNormal L z and SolvesNormal L w imply z = w, with the first conjunct unchanged; the milestone of mission d9217f6c is relinked to it.
Confirmed by the mission captain (proposal self-audit).