res_down
plain-language theorem explainer
res_down fixes the quarter-ladder residue for the down quark at -64/4, which sets the topological rung R = -16. Researchers deriving bare quark masses from the phi-ladder cite this constant to locate the down quark before applying the mass scaling formula. The definition is a direct rational assignment chosen to satisfy the quarter-integer hypothesis for quark generations.
Claim. The residue for the down quark on the quarter-ladder is defined by $r_{down} = -64/4$.
background
The module derives quark masses from the Quarter-Ladder Hypothesis, under which quarks share the lepton structural base but sit at quarter-integer rungs on the phi-ladder. The down quark is assigned the ideal position R = -16.00, written as the residue -64/4, with an approximate 5% match to experiment. Discrepancies for light quarks are ascribed to non-perturbative QCD effects omitted from the bare geometric model.
proof idea
The declaration is a direct constant definition that assigns the rational value -64/4.
why it matters
This residue supplies the input rung for the down-quark mass computation inside the RRF quark-masses framework. It implements the quarter-ladder position required by the T12 derivation and feeds the phi-ladder mass formula yardstick * phi^(rung - 8 + gap(Z)). The value closes one slot in the generation sequence and supports consistency checks against measured masses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.