downquark_params_derived

In the RS mass formula each species mass is $m = \mathrm{yardstick}(\mathrm{sector})\times\varphi^{r_0+r_{\mathrm{species}}}$, with $\mathrm{yardstick}=2^{B_{\mathrm{pow}}}\times E_{\mathrm{coh}}\times\varphi^{r_0}$ and coherence energy $E_{\mathrm{coh}}=\varphi^{-5}$. The integers $B_{\mathrm{pow}}$ and $r_0$ are sector-dependent and, per the anchor module, come from cube edge counting rather than free fits.

For the down-quark sector the definition of $B_{\mathrm{pow}}$ is $2E_{\mathrm{total}}-1$. With $E_{\mathrm{total}}=12$ this evaluates to 23. The companion offset $r_0$ is fixed at $-5$ by the same geometric bookkeeping. This module lives in the quarantined verification layer that compares those predictions to PDG 2024 values; experimental numbers are imported, not derived.

The goal is a conjunction. constructor splits it into two subgoals. The first is closed by the existing lemma that $B_{\mathrm{pow}}$ on the down-quark sector equals 23 (unfolding the cube-edge definition $2E_{\mathrm{total}}-1$). The second is closed by the companion lemma that $r_0$ on that sector equals $-5$. The theorem only packages those two equalities; it performs no fresh calculation.

This pins the geometric inputs for all down-type quark mass predictions in the verification suite (down, strange, and related comparisons against PDG). The yardstick formula in the module doc uses exactly these two integers inside the $\varphi$-ladder. Cube-derived $B_{\mathrm{pow}}=23$ and $r_0=-5$ are the concrete sector realization that the broader RS geometry (eight-tick structure, cube edge counts) is meant to force at the foundation level. No downstream used_by edges are recorded yet; the declaration is a leaf packaging step for the mass-comparison tables rather than a step in the T0–T8 forcing chain itself.