chi2_leptons_zero
plain-language theorem explainer
The sum of squared z-deviations over the lepton witness list evaluates to zero. Researchers checking particle data group fits against Recognition Science predictions would cite this to confirm the electron, muon and tau entries contribute no deviation. The proof is a one-line simplification that unfolds the chi-squared sum and applies the individual zero lemmas for each lepton entry.
Claim. $chi^2(L) = sum_{e in L} z(e)^2$. For the lepton witness list $L = [e, mu, tau]$, $chi^2(L) = 0$.
background
In the PDG fits module, chi2 is defined as the fold-left accumulation of squared z-values over a list of species entries. The leptonsWitness is the concrete list containing the electron, muon and tau entries. Three upstream lemmas establish that z equals zero on each of these entries by simplification with the definition of z and the rule div_eq_mul_inv.
proof idea
The proof is a one-line wrapper that applies the simp tactic to the definitions of chi2 and leptonsWitness together with the three zero lemmas for the electron, muon and tau entries.
why it matters
This lemma is invoked inside acceptable_leptons to discharge the chi-squared component of the acceptability predicate at zero. It thereby verifies that the lepton sector contributes no deviation in the PDG fit, consistent with the Recognition Science goal of matching observed particles to the phi-ladder predictions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.