leptonObserved
plain-language theorem explainer
Packages the two observed lepton sub-leading rung residuals (gen 1→2 and 2→3) into a single ResidualPair from pole-mass ratios, so there is no RG-scale ambiguity. Approximate values are about +0.08 and −0.13 rungs. Downstream all-sector and lepton-sector closure targets cite this as the lepton data vector. The body is a two-field structure literal over the precomputed residuals.
Claim. Define the observed lepton residual pair as the pair $(\delta_{12}^{\ell}, \delta_{23}^{\ell})$ of sub-leading rung corrections for generations $1\to 2$ and $2\to 3$, taken from pole-mass ratios (no running-scale ambiguity). Numerically $\delta_{12}^{\ell}\approx +0.08$ and $\delta_{23}^{\ell}\approx -0.13$ rungs.
background
Item 8 in the Recognition mass ladder is the open sub-leading correction that sits on top of the integer rung formula. This module builds the smallest precise target that would close that item and make an all-sector generalization falsifiable.
A ResidualPair is just the two real corrections for generation steps $1\to 2$ and $2\to 3$. For leptons the inputs are pole-mass ratios (muon/electron and tau/muon class), so the residual is free of the RG-scale ambiguity that affects quark masses. The gen-12 entry is the rung residual of the PDG muon/electron mass ratio against rung 11; gen-23 is the analogous tau-sector residual.
The local setting is the sign-split and refined ratio families that predict residual pairs from a few global coefficients and a sector signature (rungs, coupling $\kappa$, and $B$-power sign).
proof idea
Definition only: a structure literal of type ResidualPair whose gen12 field is the precomputed lepton gen-12 residual and whose gen23 field is the precomputed lepton gen-23 residual. No proof obligations.
why it matters
This is the lepton data vector that every all-sector falsification target must match. allSectorTest and refinedAllSectorTest require a single coefficient set frozen on quarks to reproduce this pair under the lepton signature; that is the out-of-sample check (leptons share the negative $B$-power sign with up quarks). leptonSectorClosure proves unique refined coefficients $(c,\eta)$ for the lepton sector alone at the candidate electromagnetic coupling $\kappa_{\mathrm{lep}}=1/(4\pi\cdot 11)$, freezing the active pair independently of quarks. leptonAnchoredTarget and signClassAllSectorTarget likewise equate predictions to this observed pair. In the RS mass picture the residuals sit on the $\varphi$-ladder yardstick formula; closing Item 8 freezes the global sub-leading coefficients across sectors.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.