m_electron
plain-language theorem explainer
Electron mass at the RS anchor scale μ*, from the lepton-sector mass law with baseline rung 2 and charge-band gap for Z = −1. Quark-ratio and residue-coordinate theorems cite it as the seam-free reference. The body is a one-line application of the forward mass predictor.
Claim. The electron mass at the anchor scale $\mu^*$ is $m_e(\mu^*)=A_{\mathrm{lepton}}\,\varphi^{r_e-8+\mathrm{gap}(Z_e)}$, where $r_e=2$ is the charged-lepton baseline rung and $Z_e$ is the lepton charge-band integer at charge $-1$.
background
This module runs a single Convention-A forward pipeline for the six quark masses: sector yardsticks from cube geometry, integer rungs from generation torsion, and $\mathrm{gap}(Z)$ from the charge-band map. No PDG mass enters. Absolute masses still need a calibration seam, so the pipeline reports dimensionless ratios $m_q/m_e$ at a fixed anchor $\mu^*$.
The mass law is $m_i(\mu^*)=A_s,\varphi^{r_i-8+\mathrm{gap}(Z_i)}$. Charged-lepton rungs are $e\mapsto 2$, $\mu\mapsto 13$, $\tau\mapsto 19$. The lepton sector supplies $A_{\mathrm{lepton}}$; the charge-band map at $Z=-1$ supplies the electron gap. The predictor predict_mass packages yardstick, rung, and gap into that formula.
Thus the electron entry is the reference mass against which every quark prediction is later normalized.
proof idea
Pure definition, not a proved theorem. It instantiates the forward mass predictor on three fixed inputs: the lepton sector (for the sector yardstick), the charged-lepton rung map at $"e"$ (integer 2), and the lepton charge-band integer at charge $-1$. No tactics or intermediate lemmas; well-typedness of those arguments is the only obligation.
why it matters
Fixes the electron anchor that makes quark outputs seam-free ratios rather than absolute masses. Downstream, positivity is recorded as a separate fact; residue coordinates are defined relative to this mass; the core pipeline is shown equal to the residue form with this reference; and all six quark predictions are rewritten as residue masses off the electron. That is the bridge between Convention A (cube yardsticks + rungs + gap) and Convention B (quarter/residue coordinates). Framework-wise it sits on the $\varphi$-ladder mass formula and on $\varphi$ forced by T5/T6; without it the "no PDG input" quark pipeline would still carry a free calibration scale.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.