mass_down_exp
plain-language theorem explainer
The definition assigns the experimental down quark mass the value 4.67 in the Recognition Science units. Model builders comparing quarter-ladder predictions for quarks to measured values reference this constant. It arises from a direct numeric assignment based on PDG data.
Claim. The experimental down quark mass is given by $m_d^{exp} = 4.67$ in the model's native units.
background
This module formalizes the quark masses under the Quarter-Ladder Hypothesis. Quarks share the same structural base mass as leptons (Sector Gauge B = -22, R0 = 62) but occupy quarter-integer rungs on the phi-ladder. The down quark is assigned the ideal topological position R = -16.00 = -64/4, with light-quark discrepancies attributed to non-perturbative QCD effects. The supplied definition gives the explicit PDG experimental target used for comparison in this geometric derivation.
proof idea
This is a one-line definition that directly assigns the constant 4.67 as the experimental value for the down quark mass.
why it matters
The declaration supplies the data target for the down quark within the T12 quark mass formalization. It is referenced by the corresponding declaration in the RRF.Physics.QuarkMasses module to support mass reconciliation. The quarter-ladder hypothesis predicts the rung position on the phi-ladder but leaves QCD corrections for later inclusion.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.