res_up
plain-language theorem explainer
The up-quark residue supplies the rational value -71/4 as the ideal rung position on the phi-ladder under the quarter-ladder hypothesis. A physicist computing bare geometric quark masses from the shared structural base would reference this constant when evaluating m_up = m_struct * phi^(-71/4). The entry is a direct constant definition with no computational reduction or lemma application.
Claim. The residue for the up quark on the phi-ladder is the rational number $r_u = -71/4$.
background
The module derives quark masses from the Quarter-Ladder Hypothesis: quarks share the structural base m_struct with leptons but sit at quarter-integer rungs on the phi-ladder. Ideal positions are listed explicitly, with the up quark at R = -17.75 = -71/4. Upstream results supply the inductive Quark type (up, down, strange, charm, bottom, top) and the phi-ladder lattice structure whose Poisson summation hypothesis supports the rung assignments.
proof idea
Direct definition that assigns the constant rational -71/4 with no lemmas or tactics applied.
why it matters
This constant fills the ideal rung for the up quark in the quarter-ladder model and feeds the predicted mass formula m = m_struct * phi^res used in the RRF mirror. It contributes to the T12 quark-mass step in the Recognition framework, where light-quark discrepancies are noted as arising from non-perturbative QCD effects not yet included in the geometric derivation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.