res_charm
plain-language theorem explainer
The definition computes the charm quark residue on the phi-ladder by subtracting the 2.5-rung bottom-to-charm step from the bottom residue. Researchers deriving second-generation quark masses under the quarter-ladder hypothesis cite this when chaining topological positions from the top quark. It is realized as a direct rational arithmetic definition with no additional computation.
Claim. The charm residue satisfies $r_c = r_b - 2.5$, where $r_b$ is the bottom quark residue on the phi-ladder and 2.5 is the quarter-integer step from bottom to charm.
background
The module formalizes quark masses under the Quarter-Ladder Hypothesis: quarks share the lepton structural mass base but sit at quarter-integer rungs on the phi-ladder. Ideal positions are top at 5.75, bottom at -2.00, charm at -4.50. The module notes explicit PDG targets and ad-hoc bounds, keeping it outside the parameter-free core mass layer until reconciliation is shown.
proof idea
One-line definition that subtracts the bottom-to-charm step (10/4) from the bottom residue to produce the charm residue.
why it matters
This supplies the charm position required by residues_match_steps, which verifies the chain res_bottom = -2, res_charm = -4.5, res_strange = -10. It feeds H_charm_mass_match and the RRF charm_mass_match certificate (error <2% against 1270 MeV). In the Recognition framework it realizes the T12 quarter-ladder step for the second generation, using the phi-ladder mass formula with rung -4.5.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.