quark_Z_from_charges
plain-language theorem explainer
The charge-band map sends up-quark charge 2/3 to the integer Z=276 and down-quark charge -1/3 to Z=24. Anyone assembling the non-circularity certificate for the quark forward pipeline cites this equality. The proof unfolds the definition of Z and closes both numeric goals by normalization.
Claim. Under the charge-band map, the integer attached to the up quark at electric charge $2/3$ equals $276$, and the integer attached to the down quark at electric charge $-1/3$ equals $24$.
background
The Unified Quark Forward Pipeline predicts all six quark masses with no PDG mass input. Inputs are counting-layer integers, the golden ratio $\varphi$ (forced at T5/T6), and $\alpha$ from the same layer. Masses are written $m_i(\mu^)=A_s,\varphi^{r_i-8+\mathrm{gap}(Z_i)}$ with dimensionless ratios against the electron at the anchor $\mu^$.
The band correction is $\mathrm{gap}(Z)=\log_\varphi(1+Z/\varphi)$. The integer $Z$ is not free: it is the image of the particle's electric charge under a fixed charge-band map. This theorem records the two values that map needs for the up and down sectors (charges $2/3$ and $-1/3$).
Those $Z$ values feed every subsequent up/down mass ratio in the pipeline and are the only charge by which charge enters the exponent.
proof idea
Term-style tactic proof in two steps. First simp only [Z] replaces both sides by the concrete charge-band formula. Then norm_num evaluates the resulting rational arithmetic and closes the conjunction $Z_{\mathrm{up}}(2/3)=276\land Z_{\mathrm{down}}(-1/3)=24$. No external lemmas are required beyond the definition of the map.
why it matters
The declaration is the $Z$-leg of the non-circularity certificate: non_circular packages geometric yardsticks, torsion rungs, and Z_from_charges := quark_Z_from_charges into a single QuarkNonCircularity witness. That witness is what lets the module claim every quark mass is a genuine forward prediction rather than a fit to measured masses.
In the RS mass law, $Z$ sits inside $\mathrm{gap}(Z)$ on the $\varphi$-ladder (yardstick $\times,\varphi^{r-8+\mathrm{gap}(Z)}$). Pinning $Z$ to charge alone closes the charge-to-band step of Convention A and keeps the pipeline aligned with the no-PDG-input design of the module. Without this equality the non-circularity structure would not typecheck.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.