m_up
plain-language theorem explainer
Defines the forward-predicted up-quark mass at the RS anchor scale μ* from sector yardstick, integer rung, and charge-band gap only. Cited by ratio corollaries (charm/up = φ^11) and positivity lemmas in the quark pipeline. Pure abbreviation: applies the shared predict_mass law at UpQuark with rung r_up("u") and Z = 2/3.
Claim. The predicted up-quark mass at the anchor scale $\mu^*$ is $m_u(\mu^*) = \mathrm{predict\_mass}(\mathrm{Up}, r_u, Z_u)$, where $r_u$ is the integer rung for the up flavor and $Z_u = 2/3$ is the charge-band coordinate, equivalently $m_u = A_s\,\varphi^{r_u-8+\mathrm{gap}(Z_u)}$ under Convention A.
background
The QuarkForwardPipeline module builds a single forward mass law for all six quarks with no PDG inputs. Inputs are counting-layer integers, $\varphi$ (forced by T5/T6), and $\alpha$ from the same layer. Absolute masses use a sector yardstick $A_s = 2^{B_{\mathrm{pow}}(s)} E_{\mathrm{coh}} \varphi^{r_0(s)}$, an integer rung from generation torsion, and the band correction $\mathrm{gap}(Z)=\log_\varphi(1+Z/\varphi)$.
The mass formula is the RS ladder $m_i(\mu^*)=A_s,\varphi^{r_i-8+\mathrm{gap}(Z_i)}$. Dimensionless ratios $m_q/m_e$ cancel calibration seams. Here the species is UpQuark, the rung is the anchor value $r_{\mathrm{up}}("u")$, and the charge coordinate is $Z(\mathrm{UpQuark},2/3)$.
Upstream predict_mass packages that ladder; r_up and the charge-band map $Z$ supply the two free integer/rational parameters for this flavor.
proof idea
One-line definitional wrapper. Unfolds to predict_mass applied at sector UpQuark with rung r_up "u" and charge argument Z .UpQuark (2/3). No tactics, no lemmas discharged at this site; mathematical content lives in the mass law and the anchor/Z maps.
why it matters
Anchors the lightest up-type mass in the no-PDG quark pipeline, so every up-sector ratio and residue identity has a concrete left-hand side. Downstream charm_to_up_eq_phi11 obtains $m_c/m_u=\varphi^{11}$ from the rung gap $15-4=11$ after simplifying through this def. m_up_pos lifts yardstick positivity to $0<m_u$. The unification theorem all_quark_predictions_have_derived_residue_coordinates rewrites $m_u$ as a residue mass relative to the electron, tying the six-quark forward list to a single coordinate convention.
Sits on the RS mass ladder (yardstick $\times,\varphi^{r-8+\mathrm{gap}(Z)}$) and the $\varphi$-forced self-similarity (T5/T6). Closes the up entry of the Convention A table without fitting.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.