acceptable_bosons
plain-language theorem explainer
The lemma establishes that the boson species list satisfies the zero-threshold acceptance criteria for both individual deviations and overall chi-squared. Particle physicists fitting PDG data to Recognition Science models would cite this to confirm the W, Z, and Higgs entries align exactly with predictions under default parameters. The proof proceeds by case analysis on the list elements combined with direct simplification using the zero lemmas for each z and chi2.
Claim. Let $L$ be the list of boson species entries. Then the acceptance condition holds: $|z(e)| = 0$ for every $e$ in $L$ and the total chi-squared of $L$ equals zero.
background
The acceptance predicate on a list of species entries requires that the absolute deviation of each entry is at most a given zMax and that the chi-squared sum over the list is at most chi2Max. The bosonsWitness list is defined as the concrete triple consisting of the W, Z, and Higgs entries taken from PDG central values. The deviation function z and the chi-squared aggregator are defined on each SpeciesEntry so that the upstream zero lemmas establish z(W_entry) = 0, z(Z_entry) = 0, and chi-squared of the full bosons list equals zero.
proof idea
The term proof splits the conjunction into the universal quantifier over list membership and the chi-squared bound. Case analysis on the three possible elements of the list dispatches each membership hypothesis to the corresponding zero lemma via simplification. The chi-squared conjunct is discharged directly by the dedicated zero lemma for the bosons list.
why it matters
This result is invoked inside the proof that the full default PDG dataset satisfies the zero-threshold acceptance condition. It confirms that the boson sector contributes no residual deviation under the Recognition Science mass formula. The lemma therefore supports the claim that the model reproduces the observed W, Z, and Higgs masses exactly when the default witness is used.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.