res_strange
plain-language theorem explainer
This definition assigns the strange quark residue the value -10 on the phi-ladder. Researchers deriving quark masses from quarter-integer topological rungs cite the constant when placing the strange quark at R = -40/4. The assignment is introduced as a direct rational constant that matches the ideal position listed in the quarter-ladder hypothesis.
Claim. The strange quark residue is defined by $r_s := -10$.
background
The module derives quark masses from the Quarter-Ladder Hypothesis: quarks share the lepton structural base but occupy quarter-integer rungs on the phi-ladder. Ideal positions are listed explicitly, with the strange quark at R = -10.00 = -40/4. Upstream results in the same module define residues via successive steps, for example res_strange := res_charm - step_charm_strange, providing the incremental construction that this direct assignment targets.
proof idea
The declaration is a one-line definition that directly assigns the rational value -40/4 to the strange quark residue.
why it matters
The value feeds the theorem residues_match_steps, which verifies that the derived residues equal the ideal positions for bottom, charm, and strange quarks. It supplies the strange quark slot in the T12 quark masses derivation inside the Recognition Science framework, using the phi-ladder with quarter-integer steps. Light quark discrepancies are left to non-perturbative QCD effects outside the bare geometric model.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.