m_down_pos
plain-language theorem explainer
The forward-predicted down-quark mass at the anchor scale is strictly positive. Anyone auditing the seam-free quark pipeline cites this to ensure m_d and the ratio m_d/m_e are well-defined. The proof is a one-line application of the general mass-law positivity lemma to the down-quark sector, rung, and charge-band inputs.
Claim. The Convention-A forward prediction of the down-quark mass at the anchor scale $\mu^*$ is strictly positive: $0 < m_d(\mu^*)$, where $m_d(\mu^*)$ is the sector-yardstick times $\varphi$ raised to the integer rung and charge-band gap for the down quark.
background
The QuarkForwardPipeline module builds a single forward mass law for all six quarks under Convention A only: sector yardsticks from cube geometry, integer rungs from generation torsion, and gap(Z) from the charge-band map. No PDG mass enters any formula. Outputs are dimensionless ratios to the electron mass at the anchor $\mu^*$, so absolute calibration seams drop out.
The mass formula is $m_i(\mu^*) = A_s \times \varphi^{r_i - 8 + \mathrm{gap}(Z_i)}$, with $A_s$ the sector yardstick, $r_i$ the integer rung, and $\mathrm{gap}(Z) = \log_\varphi(1 + Z/\varphi)$. The down-quark mass is that formula on the DownQuark sector, the down rung, and $Z$ for charge $-1/3$.
Upstream, predict_mass_pos states that mass is positive for any valid sector, rung, and $Z$. The yardstick factors (coherence energy, powers of two, powers of $\varphi$) are positive by construction from the counting layer and the golden ratio forced at T5/T6.
proof idea
One-line wrapper: apply the general positivity theorem for the mass law to the three arguments that define the down-quark prediction (DownQuark sector, down rung, and charge-band $Z$ for $-1/3$). That theorem unfolds the product form of the predicted mass and chains positivity of the yardstick with positivity of the $\varphi$-power, so the specialized inequality $0 < m_d$ follows immediately.
why it matters
Positivity of each forward quark mass is a sanity gate on the no-PDG pipeline: without it, dimensionless ratios $m_q/m_e$ are not guaranteed to be positive testable numbers. The module pairs this fact with the same statement for up, charm, top, strange, and bottom, and with yardstick positivity, so the full six-quark forward table is well-defined before any numerical comparison.
In the broader Recognition framework the mass sits on the $\varphi$-ladder (yardstick times $\varphi^{r-8+\mathrm{gap}(Z)}$), with $\varphi$ forced by T5/T6 and the eight-tick / cube counting layer supplying the integers. No downstream theorem currently depends on this lemma in the graph, but it closes the elementary well-definedness obligation for the down entry in the unified forward pipeline.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.