b_entry
The b quark data record supplies the PDG entry with observed mass 4.18, uncertainty 0.03, and predicted mass matching the observation. Researchers checking quark mass fits against the Recognition Science phi-ladder cite this record when verifying the full quarksWitness list. The definition is a direct structure literal with no computation or lemmas.
claimThe bottom-quark species record is the structure with name ``b'', observed mass $4.18$, uncertainty $0.03$, and predicted mass $4.18$.
background
SpeciesEntry is the structure holding a particle species name as string, observed mass as real, sigma as uncertainty, and predicted mass as real. The PDG.Fits module assembles these records from Particle Data Group values to compare against phi-ladder predictions in Recognition Science. The sigma field denotes experimental uncertainty and is unrelated to the sigma-charge from decision theory or the sum-of-divisors function imported from number theory.
proof idea
The definition is a direct structure literal that populates the four fields with the hardcoded PDG values for the b quark. No lemmas or tactics are applied.
why it matters in Recognition Science
This record populates the quarksWitness list and is used in acceptable_quarks to confirm zero defect for all quarks and in z_b_zero to show the b entry yields zero under the z function. It supplies the concrete data point for the bottom quark in PDG fits, supporting verification that observed masses align with the Recognition Science mass formula on the phi-ladder.
scope and limits
- Does not derive the predicted mass from the phi-ladder.
- Does not include leptons or other species.
- Does not compute chi-squared or fit statistics.
- Does not specify physical units or conversion factors.
Lean usage
lemma z_b_zero : z b_entry = 0 := by simp [z]formal statement (Lean)
64@[simp] def b_entry : SpeciesEntry := { name := "b", mass_obs := 4.18, sigma := 0.03, mass_pred := 4.18 }