lepton_Z_from_charge
plain-language theorem explainer
The lepton sector at electric charge −1 carries the integer band coordinate Z = 1332 under the charge-band map. Cite this when anchoring the electron in the forward mass pipeline or when checking gap(Z) for leptons. Proof is definition unfold plus numeric evaluation.
Claim. Under the charge-band map $Z$, the lepton sector at charge $-1$ satisfies $Z(\mathrm{lepton},-1)=1332$.
background
The module builds a single forward mass pipeline for quarks (and the lepton anchor) with no PDG targets. Sector yardsticks come from cube geometry, integer rungs from generation torsion, and the band correction is $\mathrm{gap}(Z_i)=\log_\varphi(1+Z_i/\varphi)$. Predicted masses are $m_i(\mu^*)=A_s,\varphi^{r_i-8+\mathrm{gap}(Z_i)}$, and testable outputs are dimensionless ratios to the electron.
The integer $Z$ is the charge-band coordinate of a species: it encodes how electric charge sits in the band map used by the gap. For leptons the electron anchor needs a fixed $Z_e$ so that ratios $m_q/m_e$ cancel the calibration seam. This theorem records that value at charge $-1$.
Constants in play are $\varphi$ (T5/T6 fixed point) and counting-layer integers; $\alpha$ enters yardsticks elsewhere. The equality itself is pure evaluation of the band map on the lepton sector.
proof idea
Term-mode proof in two tactics: unfold the charge-band map $Z$ with simp only [Z], then close the resulting numeral equality by norm_num. No lemmas beyond the definition of $Z$; no case splits.
why it matters
In the Convention-A pipeline the electron is the seam-free reference mass. Fixing $Z(\mathrm{lepton},-1)=1332$ pins $\mathrm{gap}(Z_e)$ in every ratio $m_i/m_e=[A_s,\varphi^{r_i-8+\mathrm{gap}(Z_i)}]/[A_\ell,\varphi^{r_e-8+\mathrm{gap}(Z_e)}]$. Without this integer the lepton denominator is undefined in Lean.
The module’s claim is genuine forward prediction from counting integers, $\varphi$, and $\alpha$ only. This check is the lepton-side counterpart of the quark $Z$ assignments used for up/down/strange/charm/bottom/top. It sits in the Verification layer rather than the forcing chain (T0–T8), but it is required for any audited mass-ratio theorem that quotes the electron anchor.
Graph used_by is currently empty; sibling mass definitions (m_electron, quark masses) are the natural consumers once ratio lemmas are stated.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.