mass_up_exp
plain-language theorem explainer
The declaration assigns the experimental up quark mass the value 2.16 for comparison against the quarter-ladder geometric prediction. Researchers validating phi-ladder residues for light quarks would cite this constant when checking the match at rung -17.75. The implementation is a direct numeric assignment with no computation or lemmas required.
Claim. The experimental mass of the up quark is defined by $m_u^{exp} := 2.16$.
background
The module formalizes T12 quark masses under the Quarter-Ladder Hypothesis: quarks share the lepton structural base but sit at quarter-integer rungs on the phi-ladder. The up quark is placed at R = -17.75 = -71/4, with the supplied experimental value serving as the benchmark; light-quark discrepancies are noted as arising from chiral symmetry breaking not included in the bare derivation. Upstream results supply the Phi integral definitions from the Aczel cost theorems that generate the underlying recognition cost function.
proof idea
The definition is a one-line numeric assignment of the constant 2.16 with no lemmas or tactics applied.
why it matters
This supplies the experimental anchor for the up quark residue computation in the same module and fills the T12 step of the quarter-ladder derivation. It connects to the Recognition Science mass formula (yardstick times phi to the power of rung minus 8 plus gap(Z)) and the forcing chain landmarks T5-T8 that fix phi, the eight-tick octave, and D = 3. The module leaves open the inclusion of non-perturbative QCD corrections for light quarks.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.