acceptable_leptons
plain-language theorem explainer
The lemma shows that the lepton witness list satisfies the zero-threshold acceptability condition. PDG fit auditors would cite it when verifying that the default lepton masses produce exact zero residuals under the Recognition mass formula. The proof proceeds by case analysis on the three lepton entries combined with direct simplification of the chi-squared sum.
Claim. Let $L = [e_0, mu_0, tau_0]$ be the list of lepton species entries. Then every entry $e$ in $L$ obeys $|z(e)| = 0$ and the chi-squared statistic of the list satisfies $chi2(L) = 0$.
background
In the PDG.Fits module the predicate acceptable L zMax chi2Max asserts that every species entry in the list L has absolute standardized residual at most zMax and that the total chi-squared deviation of the list is at most chi2Max. The lepton witness is the concrete list containing the electron, muon and tau entries whose observed masses are set equal to the Recognition predictions, forcing all residuals to zero. This lemma sits downstream of the individual z-zero lemmas for each lepton and of the chi-squared vanishing lemma; it is invoked by the aggregate acceptability statement for the full default dataset.
proof idea
The proof opens with And.intro to split the conjunction. The first conjunct is discharged by introducing an arbitrary entry and performing case analysis on the three-element list membership; each case reduces immediately to one of the zero lemmas via simp. The second conjunct is obtained by direct simplification against the pre-proved chi2_leptons_zero lemma.
why it matters
This lemma supplies the lepton component of the baseline zero-deviation result for the entire default PDG dataset. It is cited inside acceptable_all_default_zero, which in turn verifies that the Recognition mass ladder reproduces the central PDG values for all standard-model species at the chosen precision. Within the Recognition framework the result confirms that the phi-ladder assignments for the three charged leptons lie exactly on the predicted mass curve, closing one sector of the T5–T8 forcing chain verification.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.