res_bottom
plain-language theorem explainer
The res_bottom definition places the bottom quark at rung -2 on the phi-ladder by subtracting the 7.75-rung top-to-bottom step from the top residue 23/4. Researchers applying the quarter-ladder hypothesis to quark generation spacing cite this residue when checking mass predictions. It is realized as a direct arithmetic definition using the precomputed step constant.
Claim. Let $r_t = 23/4$ be the ideal top residue and let $s = 31/4$ be the rung step from top to bottom. The bottom residue is then defined by $r_b := r_t - s$, which evaluates to $-2$.
background
The QuarkMasses module develops the quarter-ladder hypothesis: quarks share the structural mass base with leptons but sit at quarter-integer rungs on the phi-ladder. Ideal positions include top at 5.75 and bottom at -2.00, with generation intervals of 7.75, 2.50, and 5.50 rungs. Upstream, step_top_bottom supplies the 7.75-rung interval while res_top fixes the starting residue at 23/4. The module records that light-quark discrepancies are ascribed to non-perturbative QCD effects outside the bare geometric derivation.
proof idea
One-line definition that subtracts the value of step_top_bottom from res_top.
why it matters
This residue supplies the input to H_bottom_mass_match, which verifies the predicted bottom mass lies within 1% of the observed value, and to residues_match_steps, which confirms consistency of the full residue chain. It also appears in the RRF.Physics.QuarkMasses mirror. Within the Recognition framework the definition realizes the T12 quarter-ladder step for the bottom quark, linking directly to the phi-ladder mass formula and the eight-tick octave structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.