t_entry
plain-language theorem explainer
The top-quark data record supplies observed mass 172.76 GeV with uncertainty 0.30 for PDG fits in the Recognition framework. Model builders cite it when constructing the list of quark species for mass verification. It is a direct record construction with no computation steps.
Claim. Let the top-quark entry be the structure with name ``t'', observed mass $172.76$, uncertainty $0.30$, and predicted mass $172.76$.
background
SpeciesEntry is a record type that holds the name, observed mass, experimental uncertainty, and model-predicted mass for each particle species. In this module the entries are assembled into witness lists to confirm that the Recognition Science mass predictions fall inside the experimental bands. The sigma field here denotes the standard deviation of the mass measurement, distinct from the sigma-charge in decision theory or the divisor-sum function in number theory.
proof idea
One-line definition that constructs the SpeciesEntry record with the supplied numerical values for the top quark.
why it matters
This entry is referenced by the quarksWitness list and supports the acceptable_quarks lemma together with the zero-deviation result for the top quark. It supplies the empirical anchor for the top-quark rung on the phi-ladder, consistent with the J-uniqueness and self-similar fixed-point steps of the forcing chain. The exact match between observed and predicted mass closes one data point in the D=3 spatial dimension spectrum.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.