mass_up_exp
plain-language theorem explainer
This definition supplies the PDG experimental value 2.16 for the up-quark mass inside the quarter-ladder model. Researchers comparing geometric phi-ladder predictions to measured quark masses cite it as the benchmark target. It is realized by a direct numeric assignment with no computation or lemmas applied.
Claim. The experimental mass of the up quark is defined by the constant value $2.16$ (in the units adopted by the quarter-ladder hypothesis).
background
The module formalizes quark masses via the Quarter-Ladder Hypothesis: quarks share the structural base mass of leptons but sit at quarter-integer rungs on the phi-ladder. The ideal rung for the up quark is given as $R = -17.75 = -71/4$. The phi-ladder itself is the self-similar fixed point arising from the Recognition forcing chain (T6), with masses scaled by yardstick times phi to the power of (rung minus 8 plus gap). Upstream results supply the Phi integral operator used in the broader cost framework, though the present definition is independent of that operator.
proof idea
The declaration is a direct numeric assignment of the experimental value 2.16. No lemmas are invoked; the body consists solely of the constant literal.
why it matters
The definition supplies the experimental target for the up-quark rung in the T12 quarter-ladder formalization. It is referenced by the RRF.Physics.QuarkMasses counterpart and supports direct comparison against the Recognition mass formula on the phi-ladder. The module note records that this layer remains outside the parameter-free core until an explicit reconciliation theorem is proved.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.