res_strange
plain-language theorem explainer
The definition sets the strange quark residue to the charm residue minus the 5.5-rung topological step on the quarter-ladder. Modelers of quark mass hierarchies via phi-ladder positions cite it to track generation spacing. It is a direct arithmetic definition with no further obligations.
Claim. $r_s = r_c - 5.5$, where $r_c$ is the charm residue obtained from the prior bottom-to-charm step and 5.5 is the rung spacing from charm to strange.
background
The Quark Masses module formalizes the Quarter-Ladder Hypothesis: quarks occupy quarter-integer rungs on the phi-ladder while sharing the lepton structural base. Ideal positions include strange at R = -10. Upstream, step_charm_strange is defined as 22/4 and res_charm is defined as res_bottom minus the bottom-to-charm step.
proof idea
One-line definition that subtracts the numeric value of step_charm_strange from res_charm.
why it matters
The residue is used by the theorem residues_match_steps, which verifies that computed residues equal the ideal positions including res_strange = -10. It fills the charm-to-strange generation step in the T12 quark mass derivation and connects to the phi-ladder structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.