up_yardstick_components
plain-language theorem explainer
The up-quark sector yardstick is fixed by the integer pair (binary power, base rung) = (−1, 35), derived from cube-edge and wallpaper counting. Anyone assembling the Convention A forward mass pipeline for up-type quarks cites this pair. The proof is a one-line pairing of the two already-proved component equalities.
Claim. For the up-quark sector, the binary power equals $-1$ and the base $\varphi$-exponent offset equals $35$.
background
The Quark Forward Pipeline predicts all six quark masses from counting-layer integers alone (cube geometry $V,E,F$, passive edges, wallpaper groups $W$, active edges $A$), the golden ratio $\varphi$ forced at T5/T6, and $\alpha$. No PDG mass enters any formula. Absolute masses are avoided; the seam-free outputs are dimensionless ratios $m_q/m_e$ at the anchor scale.
Each sector carries a yardstick $A_s = 2^{B(s)},E_{\mathrm{coh}},\varphi^{r_0(s)}$. The binary powers $B(s)$ come from cube edge counting; for up-quarks, $B = -A = -1$. The offsets $r_0(s)$ come from wallpaper-plus-cube geometry; for up-quarks, $r_0 = 2W + A = 2\cdot 17 + 1 = 35$. The mass law then multiplies by $\varphi^{r_i-8+\mathrm{gap}(Z_i)}$.
Upstream equalities already discharge each component separately by simplifying the sector definitions and evaluating the counting constants.
proof idea
One-line term proof: pair the two upstream equalities. The first states that the up-quark binary power equals $-1$; the second states that the up-quark base rung equals $35$. The conjunction is exactly the claim.
why it matters
This locks the up-sector yardstick ingredients used by the Convention A pipeline: $A_{\mathrm{up}} = 2^{-1},E_{\mathrm{coh}},\varphi^{35}$. Without fixed $(B,r_0)$, the subsequent rung, gap, and ratio steps cannot be pure forward predictions. The values sit on the same counting layer that forces $\varphi$ (T5/T6) and the eight-tick geometry, so the up-quark mass formula inherits the RS mass-ladder structure $\mathrm{yardstick}\times\varphi^{r-8+\mathrm{gap}(Z)}$ with no free sector parameters. No downstream theorem currently depends on this packaging lemma; it is a local convenience for the pipeline module and its sibling mass definitions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.