z_b_zero
plain-language theorem explainer
Researchers fitting PDG quark masses to the Recognition Science phi-ladder cite z_b_zero to record that the bottom quark contributes zero residual. The lemma states that z applied to b_entry equals zero because the entry's predicted and observed masses are identical. Its proof is a one-line simplification that unfolds the z definition on the explicit b_entry record.
Claim. $z(b_ {entry}) = 0$, where $b_{entry}$ is the SpeciesEntry record for the bottom quark with observed mass 4.18 GeV, predicted mass 4.18 GeV, and uncertainty 0.03 GeV.
background
In the PDG.Fits module the z function returns the normalized residual (mass_pred - mass_obs)/sigma for any SpeciesEntry while chi2 sums the squared residuals over a witness list of entries. The b_entry definition supplies the concrete bottom-quark numbers with matching masses. This lemma belongs to the suite of z_*_zero results that verify exact fits for the six quarks under the Recognition Science mass formula yardstick * phi^(rung - 8 + gap(Z)).
proof idea
The proof is a one-line wrapper that applies simp [z]. The tactic unfolds the definition of z on b_entry and cancels the identical mass_pred and mass_obs fields, leaving zero.
why it matters
z_b_zero is invoked inside chi2_quarks_zero to obtain chi2 quarksWitness = 0 and inside acceptable_quarks to confirm every quark entry satisfies the zero-residual condition. It supplies an empirical check that the b quark lies exactly on a phi-ladder rung, consistent with the T5 J-uniqueness, T6 phi fixed point, T7 eight-tick octave, and T8 D = 3 dimensions of the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.