res_top
plain-language theorem explainer
The definition supplies the rational 23/4 as the ideal residue for the top quark on the phi-ladder under the quarter-ladder hypothesis. Researchers deriving quark masses from the Recognition Science structural base cite this constant when verifying predicted masses against experiment. It is introduced by direct assignment of the fraction 23/4 with no further computation.
Claim. Let $r$ denote the ideal residue on the phi-ladder for the top quark. Then $r = 23/4$.
background
The module formalizes T12 on quark masses via the quarter-ladder hypothesis: quarks share the structural base mass with leptons but sit at quarter-integer rungs on the phi-ladder. The top quark is placed at rung 5.75, written as the rational 23/4. This placement is taken from the upstream definition in the RRF.Physics.QuarkMasses module, which states the same constant for use in mass predictions and bounds.
proof idea
The declaration is a direct definition that assigns the rational 23/4. No lemmas or tactics are invoked; the value serves as a named constant for downstream residue arithmetic and mass-match checks.
why it matters
This constant anchors the top-quark prediction in the quarter-ladder model and feeds the hypothesis check that the predicted mass lies within 0.05 percent of experiment. It realizes the ideal position R = 5.75 stated in the T12 module documentation and is consistent with the phi-ladder mass scaling in the Recognition framework. The value enables the step-wise residue definitions for the remaining quarks before non-perturbative QCD effects are added for the light sector.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.