c_entry
plain-language theorem explainer
The c_entry definition supplies the SpeciesEntry record for the charm quark, fixing observed mass at 1.27 GeV with uncertainty 0.03 and predicted mass matching exactly. Quark fit lemmas such as acceptable_quarks and z_c_zero cite this entry when validating the six-quark witness list against Recognition Science mass assignments. The definition is a direct record construction carrying the simp attribute.
Claim. The charm quark is the SpeciesEntry record with name ``c'', observed mass $1.27$, uncertainty $0.03$, and predicted mass $1.27$.
background
SpeciesEntry is the structure holding a particle name, observed mass, experimental uncertainty sigma, and predicted mass for use in chi-squared fits. The PDG.Fits module assembles such entries for the six quarks and three leptons to test consistency with the Recognition Science phi-ladder mass formula. Upstream results include the arithmetic sigma abbreviation and the Agent sigma from decision theory, though the field here directly encodes the PDG uncertainty interval.
proof idea
This is a direct definition that constructs the SpeciesEntry record literal with the supplied numerical constants for the charm quark. No lemmas are applied and no tactics are invoked.
why it matters
c_entry populates the quarksWitness list and is checked by acceptable_quarks and z_c_zero. These lemmas confirm zero defect for the quark sector at the base rung, supporting the PDG fit validation step in the Recognition Science framework. The entry aligns the charm mass exactly with the observed value on the phi-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.