m_down
plain-language theorem explainer
Defines the down-quark mass at the RS anchor scale μ* as a pure forward prediction: sector yardstick times a φ-power fixed by the down rung and the charge-band gap at Z = −1/3. Anyone checking the six-quark pipeline or dimensionless m_q/m_e ratios cites it. The body is a one-line abbreviation of the shared predict_mass law.
Claim. The down-quark mass at the anchor $\mu^*$ is $m_d(\mu^*) = \mathrm{predict\_mass}(\mathrm{Down}, r_d, Z_{\mathrm{Down}}(-1/3))$, i.e. the sector yardstick times $\varphi^{r_d-8+\mathrm{gap}(Z)}$ with integer rung $r_d$ and band charge $Z=-1/3$.
background
The module runs a single Convention-A forward pipeline for all six quarks: no PDG mass is an input. Inputs are counting-layer integers (cube geometry), $\varphi$ from the T5/T6 forcing chain, and $\alpha$ from the same layer. Absolute masses are written only at the anchor $\mu^*$; the testable outputs are dimensionless ratios to the electron.
The mass law is $m_i(\mu^*)=A_s,\varphi^{r_i-8+\mathrm{gap}(Z_i)}$, where $A_s$ is the sector yardstick from cube geometry, $r_i$ is the integer rung (baseline plus generation torsion), and $\mathrm{gap}(Z)=\log_\varphi(1+Z/\varphi)$ is the charge-band correction. For the down quark the charge argument is the standard $Z=-1/3$, and the rung is the anchor value $r_{\mathrm{down}}(\mathrm{d})$.
Sibling abbreviations $m_{\mathrm{up}},m_{\mathrm{strange}},\ldots$ instantiate the same predict_mass template on the other flavors; positivity lemmas such as $m_{\mathrm{down}}>0$ follow immediately from positivity of the yardstick and of $\varphi$-powers.
proof idea
Pure definitional abbreviation: expand predict_mass on species .DownQuark with rung r_down "d" and band coordinate Z .DownQuark (-1/3). No tactic proof; the mathematical content is entirely in the shared mass law and the anchor/Z-map data those arguments carry.
why it matters
Fills the down slot of the six-quark forward table that the module advertises as PDG-free. Downstream, m_down_pos records $0<m_d$, and all_quark_predictions_have_derived_residue_coordinates packages all six masses (including this one) as residue coordinates relative to $m_e$, proving the quarter/residue convention is derived from the same pipeline rather than fitted.
In the broader RS mass story this is one concrete instance of the primer formula yardstick $\times,\varphi^{\mathrm{rung}-8+\mathrm{gap}(Z)}$ on the $\varphi$-ladder, with $\varphi$ forced by T5/T6. It is the object a referee compares to the experimental $m_d/m_e$ ratio once the electron yardstick is fixed the same way.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.