m_bottom_pos
plain-language theorem explainer
The forward-pipeline bottom-quark mass at the anchor scale is strictly positive. Cited by anyone checking the six-quark ladder, dimensionless ratios to the electron, or numerical sanity of Convention A. Proof is a one-line application of the general mass-law positivity lemma to the bottom configuration.
Claim. The predicted bottom-quark mass at the anchor scale $\mu^*$ is strictly positive: $0 < m_b(\mu^*)$, where $m_b$ is the Convention-A mass $A_s\,\varphi^{r-8+\mathrm{gap}(Z)}$ for the down-quark sector with bottom rung and charge-band $Z$.
background
The module builds a single forward-prediction pipeline for all six quark masses under Convention A only: sector yardsticks from cube geometry, integer rungs from generation torsion, and gap$(Z)$ from the charge-band map. No measured PDG quark mass enters any formula. Outputs are dimensionless ratios $m_q/m_e$ at the anchor $\mu^*$, which are seam-free.
The mass law is $m_i(\mu^*)=A_s,\varphi^{r_i-8+\mathrm{gap}(Z_i)}$, with $A_s=2^{B_{\mathrm{pow}}(s)}E_{\mathrm{coh}}\varphi^{r_0(s)}$ and $\mathrm{gap}(Z)=\log_\varphi(1+Z/\varphi)$. Here $\varphi$ is the golden ratio forced by T5/T6. The bottom mass is the down-quark-sector instance with bottom rung and $Z$ for charge $-1/3$.
Upstream, predict_mass_pos states that mass is positive for any valid sector, rung, and $Z$ configuration, by positivity of the yardstick and of the $\varphi$-power.
proof idea
One-line wrapper: apply the general lemma that predict_mass is positive for every valid sector, integer rung, and charge-band $Z$, instantiating those arguments with the bottom configuration (down-quark sector, bottom rung, $Z$ for charge $-1/3$). No extra algebra; the holes are filled by the definition of the bottom mass.
why it matters
Closes the positivity check for the heaviest down-type quark in the no-PDG forward pipeline. Together with the sibling positivity facts for up, charm, top, down, and strange, it guarantees every Convention-A quark mass on the $\varphi$-ladder is a positive real, so dimensionless ratios $m_q/m_e$ are well-defined and comparable to data. Sits in the verification layer that audits the mass formula $A_s,\varphi^{r-8+\mathrm{gap}(Z)}$ built from counting-layer integers, $\varphi$ (T5/T6), and $\alpha$, without calibration seams. No downstream dependents are recorded yet; the natural consumers are ratio lemmas and numerical export of the six-quark ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.