chi2_baryons_zero
plain-language theorem explainer
The lemma establishes that the chi-squared statistic for the baryon witness list evaluates to zero. Particle physicists fitting PDG mass data would cite this to confirm exact match for the selected baryons. The proof is a one-line simplification that unfolds the sum-of-squares definition and applies the zero lemmas for each entry's deviation function.
Claim. Let $B$ be the list of proton, neutron, and four Delta baryon species entries. Let $z$ be the deviation function for each entry. Then the chi-squared statistic defined by the sum of $z(e)^2$ over $e$ in $B$ equals zero.
background
The chi2 function computes the sum of squared deviations by folding the square of the z-value for each species entry in the input list. The baryonsWitness assembles the explicit list of proton, neutron, Delta++, Delta+, Delta0, and Delta- entries drawn from PDG data. Upstream lemmas establish that the deviation function z equals zero for each of the Delta entries and for the proton and neutron.
proof idea
This is a one-line simp wrapper. It unfolds the chi2 definition as a foldl accumulation of squares, substitutes the baryonsWitness list, and reduces every term to zero by applying the dedicated zero lemmas for proton, neutron, Delta++, Delta+, Delta0, and Delta-.
why it matters
This result is invoked by the acceptable_baryons lemma to certify that the baryon list meets the zero chi-squared and zero-deviation conditions. It supports verification that the PDG baryon masses align exactly with the Recognition Science mass formula on the phi-ladder. The zero outcome is consistent with the T5 J-uniqueness and T6 self-similar fixed point in the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.