mass_down_exp
plain-language theorem explainer
The declaration supplies the measured down-quark mass 4.67 in Recognition Science native units. Researchers comparing quarter-ladder geometric predictions against data would cite this constant when testing the R = -16 rung assignment. It is introduced as a direct numeric definition with no derivation.
Claim. The experimental mass of the down quark is defined to be $4.67$ in Recognition Science units.
background
The Quark Masses module formalizes the six quark masses via the Quarter-Ladder Hypothesis. Quarks share the structural base mass of leptons (Sector Gauge B = -22, R0 = 62) but sit at quarter-integer rungs on the phi-ladder. The down quark is placed at rung R = -16.00 = -64/4; the experimental value serves as the benchmark for the bare geometric prediction before non-perturbative QCD corrections are added.
proof idea
The declaration is a one-line definition that directly assigns the numeric constant 4.67.
why it matters
This constant anchors the comparison of the quarter-ladder prediction against experiment for the down quark. It supports the module's goal of matching observed masses to topological positions on the phi-ladder. The documented light-quark discrepancies point to the open question of incorporating chiral symmetry breaking.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.