m_charm_pos
plain-language theorem explainer
The forward-predicted charm mass at the RS anchor is strictly positive. Anyone auditing the quark pipeline for well-defined mass ratios or log-scale comparisons cites this. Proof is a one-line application of the general mass-law positivity lemma to the charm sector, rung, and charge-band inputs.
Claim. The Convention-A forward prediction for the charm quark mass at the anchor scale $\mu^*$ is strictly positive: $0 < m_c(\mu^*)$, where $m_c$ is built from the up-quark sector yardstick, the charm generation rung, and the charge-band gap at $Z = 2/3$.
background
The QuarkForwardPipeline module builds all six quark masses from a single forward recipe with no PDG targets: sector yardstick $A_s$ from cube geometry and $\varphi$, integer rung from generation torsion, and band correction $\mathrm{gap}(Z)=\log_\varphi(1+Z/\varphi)$. The mass law is $m_i(\mu^*)=A_s,\varphi^{r_i-8+\mathrm{gap}(Z_i)}$. Outputs used for tests are dimensionless ratios to the electron mass at the same anchor.
Charm is placed in the up-quark sector with charge fraction $2/3$. Its predicted mass is the specialization of predict_mass to that sector, the charm rung, and $Z$ for charge $2/3$. Upstream, predict_mass_pos states that every such configuration yields a positive real: yardstick factors (coherence energy, powers of two, powers of $\varphi$) and the exponential $\varphi$-ladder term are all positive.
proof idea
One-line wrapper: apply predict_mass_pos to the three arguments already fixed by the charm mass definition (up-quark sector, charm rung, and $Z$ at charge $2/3$). The general lemma unfolds the mass formula and multiplies positive factors (yardstick positivity and $\varphi$-power positivity), so the specialized inequality $0<m_c$ follows immediately.
why it matters
Positivity is the first well-definedness check in the no-PDG quark pipeline: ratios $m_q/m_e$ and any log-distance comparisons require $m_c>0$. The declaration sits beside the sibling positivity facts for the other quarks and the electron yardstick, closing the elementary sign obligations before numerical band checks.
It rests on the RS mass formula (yardstick times $\varphi^{r-8+\mathrm{gap}(Z)}$) forced from the T5/T6 $\varphi$ fixed point and the charge-band map. No downstream theorem currently depends on it in the graph, but the module's stated purpose (seam-free dimensionless ratios) needs every predicted mass positive. It does not touch open calibration or PDG-matching questions; it only certifies the sign of the forward charm output.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.