m_strange
plain-language theorem explainer
Strange-quark mass at the RS anchor μ*, from the single forward mass law on the down sector with the strange rung and charge band Z = −1/3. Cited by anyone checking dimensionless quark ratios or the bottom/strange = φ^6 corollary. One-line binding of the sector yardstick–rung–gap pipeline; no free parameters and no PDG input.
Claim. The strange quark mass at the anchor scale $\mu^*$ is the forward prediction $m_s(\mu^*)=A_{\mathrm{down}}\,\varphi^{r_s-8+\mathrm{gap}(Z_s)}$, where $A_{\mathrm{down}}$ is the down-sector yardstick, $r_s$ is the integer rung assigned to the strange generation, and $Z_s=-1/3$ is the down-sector charge-band coordinate.
background
The module runs one forward pipeline for all six quarks under Convention A: sector yardsticks from cube geometry, integer rungs from generation torsion, and band corrections gap(Z) from the charge map. Inputs are only counting-layer integers, φ (forced at T5/T6), and α from the same layer. No measured quark mass enters any formula.
The mass law is $m_i(\mu^)=A_s,\varphi^{r_i-8+\mathrm{gap}(Z_i)}$ with $\mathrm{gap}(Z)=\log_\varphi(1+Z/\varphi)$. Absolute MeV values need a calibration seam; the module therefore emphasizes dimensionless ratios $m_q/m_e$ at μ, which are seam-free.
Here the strange sits in the down sector (charge −1/3). The rung $r_{\mathrm{down}}(\mathrm{s})$ and the charge-band map $Z$ are supplied by the mass-anchor and Z-map modules; this declaration only specializes the common predictor to that triple.
proof idea
Pure definition: bind the real constant to predict_mass on the down-quark sector, the strange rung from the down-family anchor map, and the charge-band value $Z=-1/3$. No tactics, no lemmas unfolded at this site; positivity and ratio identities are proved downstream from the shared predictor lemmas.
why it matters
Closes the strange slot in the six-quark forward table so every later ratio is a pure φ-power identity rather than a fit. Downstream, m_strange_pos records positivity; bottom_to_strange_eq_phi6 obtains $m_b/m_s=\varphi^6$ from the rung gap $21-15=6$ via the structural charm-to-up ratio on the down sector; and all_quark_predictions_have_derived_residue_coordinates packages all six masses as residue coordinates relative to the electron. Sits on the RS mass ladder (yardstick × φ^{rung−8+gap(Z)}) forced by T5/T6 uniqueness of J and φ, with the eight-tick octave fixing the −8 offset. Supports the module claim that the pipeline is genuine forward prediction, not PDG targeting.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.