chi2
The chi2 definition sums squared z-scores over a list of species entries to yield an unnormalized chi-squared statistic. Galaxy rotation modelers and particle mass fitters cite it when quantifying agreement between observed and predicted values in SPARC or PDG datasets. The implementation is a direct left-fold that accumulates the squared terms from an initial zero accumulator.
claimLet $L$ be a list of species entries, each carrying an observed mass $m_ {obs}$, uncertainty $σ$, and predicted mass $m_ {pred}$. Then $χ^2(L) := ∑_{e∈L} z(e)^2$, where $z(e)$ is the standardized residual $(m_ {obs}(e) - m_ {pred}(e))/σ(e)$ for entry $e$.
background
In the PDG.Fits module, SpeciesEntry is the structure that packages a species name, its observed mass, measurement uncertainty sigma, and the model-predicted mass. The chi2 definition aggregates these entries into a total squared-residual statistic via list folding. Upstream results include the Ledger L from Recognition, which encodes debit-credit balance rules, and the zero Ledger from Cycle3, both available for conservation checks in sibling computations.
proof idea
This is a one-line definition that applies List.foldl to the input list, adding the square of z applied to each SpeciesEntry to an accumulator initialized at zero.
why it matters in Recognition Science
The definition supplies the chi-squared metric consumed by the SPARCFalsifier module, including gas_stars_swap_control, generous_threshold, and global_only_policy. These theorems test whether control swaps and zero-free-parameter policies inflate the statistic above the RS-predicted median of 2.75, thereby supporting the phi-ladder mass formula and eight-tick octave predictions in the gravity sector.
scope and limits
- Does not normalize by degrees of freedom or produce reduced chi-squared.
- Does not incorporate covariances between entries.
- Returns zero on the empty list without special handling.
- Depends on an external z function for per-entry residuals.
formal statement (Lean)
17def chi2 (L : List SpeciesEntry) : ℝ :=
proof body
Definition body.
18 L.foldl (fun acc e => acc + (z e) * (z e)) 0
19