acceptable_baryons
The lemma establishes that the baryon witness list meets the strict zero-deviation acceptance thresholds. PDG fitters would cite it when confirming that proton, neutron, and Delta resonance masses match predictions exactly under the chi-squared metric. The tactic proof splits the goal into a membership universal quantified by exhaustive case analysis on the six entries and a direct simplification to the precomputed zero chi-squared result.
claimLet $B$ be the list of baryon entries consisting of the proton, neutron, and four Delta resonances. Then every entry $e$ in $B$ satisfies $|z(e)| = 0$ and the chi-squared statistic of $B$ equals zero, where $z$ denotes the normalized mass deviation for each species entry.
background
In the PDG.Fits module the acceptance predicate is the conjunction of a uniform bound on absolute normalized deviation across a list of species entries and an upper bound on the aggregate chi-squared of that list. The baryonsWitness supplies the concrete list of six entries (proton, neutron, Delta++, Delta+, Delta0, Delta-) with mass_pred set equal to mass_obs for each. Upstream lemmas establish that the normalized deviation vanishes individually for each of these entries and that the chi-squared of the full list is identically zero.
proof idea
The proof refines the goal into the two conjuncts of acceptable. The deviation bound is discharged by case analysis on list membership, substituting each of the six possible entries and simplifying with the corresponding z-zero lemma. The chi-squared conjunct is discharged by direct simplification against the pre-established chi2_baryons_zero lemma.
why it matters in Recognition Science
This lemma is invoked inside acceptable_all_default_zero to close the baryon sector of the default-dataset verification. It supplies the zero-threshold baseline for the PDG fit checks that support Recognition Science mass predictions on the phi-ladder. The result anchors the light-baryon sector of the framework's comparison between theoretical yardsticks and experimental central values.
scope and limits
- Does not extend the acceptance check to leptons, quarks, or bosons.
- Does not incorporate experimental uncertainties beyond the supplied sigmas in the entries.
- Does not prove uniqueness of the zero-deviation fit or address parameter variations.
- Does not cover higher resonances or exotic baryons outside the listed six entries.
Lean usage
simpa [defaultDataset] using acceptable_baryonsformal statement (Lean)
139@[simp] lemma acceptable_baryons : acceptable baryonsWitness 0 0 := by
proof body
Tactic-mode proof.
140 refine And.intro ?hzs ?hchi
141 · intro e he
142 have hcases : e = p_entry ∨ e = n_entry ∨ e = Delta_pp_entry ∨ e = Delta_p_entry ∨ e = Delta_0_entry ∨ e = Delta_m_entry := by
143 simpa [baryonsWitness] using he
144 rcases hcases with h | h | h | h | h | h
145 · subst h; simp [z_p_zero]
146 · subst h; simp [z_n_zero]
147 · subst h; simp [z_Dpp_zero]
148 · subst h; simp [z_Dp_zero]
149 · subst h; simp [z_D0_zero]
150 · subst h; simp [z_Dm_zero]
151 · simpa using chi2_baryons_zero
152
153/-! Parameterized PDG fits: thresholds and dataset wrappers. -/
154