down_yardstick_components
plain-language theorem explainer
The down-quark sector yardstick is fixed by the integer pair (power-of-two exponent, base rung) equal to (23, −5). Anyone building Convention-A forward mass ratios for light quarks cites this pair when assembling A_s = 2^{B} E_coh φ^{r0}. The proof is a one-line packaging of the two already-proved component equalities for the down sector.
Claim. The sector-yardstick components for the down quark are $B_{\mathrm{pow}}(\mathrm{down})=23$ and $r_0(\mathrm{down})=-5$.
background
The module implements a single forward-prediction pipeline for all six quark masses under Convention A: sector yardsticks from cube geometry, integer rungs from generation torsion, and gap(Z) from the charge-band map. No PDG quark mass enters any formula; inputs are counting-layer integers, φ (from T5/T6), and α from the same layer.
The sector yardstick is $A_s = 2^{B_{\mathrm{pow}}(s)} \times E_{\mathrm{coh}} \times \varphi^{r_0(s)}$. Predicted mass at the anchor is then $m_i(\mu^*) = A_s \times \varphi^{r_i - 8 + \mathrm{gap}(Z_i)}$, and the reported observables are dimensionless ratios $m_i/m_e$. This declaration pins the two integer ingredients of $A_s$ for the down sector alone.
Sibling declarations supply the analogous pairs for up, charm, top, strange, and bottom, plus positivity facts used when forming ratios.
proof idea
Term-mode one-liner: the conjunction is assembled by pairing the two preexisting equalities B_pow_DownQuark_eq and r0_DownQuark_eq. No further algebra or case analysis occurs here.
why it matters
Without fixed $(B_{\mathrm{pow}}, r_0)$ the yardstick $A_s$ is undefined, so the whole forward chain $A_s \to \varphi^{r-8+\mathrm{gap}(Z)} \to m_q/m_e$ cannot start for the down quark. The module's non-circularity certificate traces predict_mass through yardstick to exactly these counting-layer integers, so this pair is part of the design assertion that no measured quark mass feeds the formulas.
It sits inside the RS mass ladder (yardstick times $\varphi^{\mathrm{rung}-8+\mathrm{gap}(Z)}$) driven by φ from the T5/T6 forcing chain. Downstream use is local to the quark pipeline (no external used_by edges recorded); the value is consumed when forming $m_{\mathrm{down}}$ and the ratio to the electron anchor.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.