chi2
plain-language theorem explainer
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.
Claim. Let $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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.