res_top
plain-language theorem explainer
res_top supplies the quarter-ladder position 23/4 for the top quark in the Recognition Science mass formula. Researchers deriving quark masses from the phi-ladder would reference this value to compute the predicted top mass and check agreement with experiment. The definition sets the base residue from which all other quark residues are obtained by subtracting fixed steps.
Claim. The ideal topological residue for the top quark on the phi-ladder is the rational number $R = 23/4$.
background
The module formalizes T12, the Quarter-Ladder Hypothesis for quark masses. Quarks share the structural base mass with leptons but sit at quarter-integer rungs on the phi-ladder. The ideal positions are listed explicitly: top at 5.75 = 23/4, bottom at -2, charm at -4.5, and so on, with discrepancies in light quarks attributed to non-perturbative QCD effects not included in the bare geometric derivation.
proof idea
This is a direct constant definition that assigns the rational 23/4 to res_top. No lemmas or tactics are invoked; the value is introduced as the starting rung for the top quark.
why it matters
The definition anchors the top-quark entry in the Quarter-Ladder Hypothesis of T12. It is used directly by H_top_mass_match to bound the relative error below 0.05 percent, by res_bottom to generate the next residue, and by residues_match_steps to verify the full set of generation steps. It supplies the concrete rung that enters the Recognition Science mass formula yardstick * phi^(rung - 8 + gap(Z)).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.