leptonEta
plain-language theorem explainer
Defines the lepton-sector sub-leading parameter η from pole-mass gen12 and gen23 residuals with rung steps 11 and 6, numerically about +0.065. Anyone closing Item 8 or anchoring quark transport to the lepton sector cites this constant. It is a direct application of the closed-form eta-from-data formula to the lepton residual pair.
Claim. The lepton $\eta$ is the real number obtained by feeding the lepton generation-1–2 and generation-2–3 pole-mass residuals, together with the rung steps $11$ and $6$, into the closed-form residual-to-$\eta$ map $\eta=(g_{12}s_{12}+g_{23}s_{23})/(\ln(s_{12}/s_{23})\cdot(g_{12}s_{12}-g_{23}s_{23}))$.
background
Item 8 asks for a unified sub-leading correction to the RS mass ladder across lepton and quark sectors. The module builds a refined residual family whose free parameters are an active amplitude $c$ and a dimensionless tilt $\eta$. The plain sign-split family is rigid: it forces $g_{12}s_{12}+g_{23}s_{23}=0$, which PDG residuals violate. The closed-form map etaFromData absorbs that violation by solving for $\eta$ from the two residuals and their rung steps.
Leptons are the preferred anchor because pole masses carry no RG-scheme ambiguity. The steps $11$ and $6$ are the lepton rung gaps on the $\varphi$-ladder (electron–muon and muon–tau). The resulting $\eta\approx +0.065$ is the cleanest empirical input the module freezes before transporting coefficients into the quark sectors.
proof idea
One-line definitional wrapper: apply the already-proved closed-form residual-to-$\eta$ constructor to the lepton gen12 residual, the lepton gen23 residual, and the fixed steps $11$ and $6$. No tactics; the value is whatever that formula returns on those four inputs.
why it matters
Freezes the lepton $\eta$ that every lepton-anchored Item 8 object reuses. Downstream, leptonAnchoredCNeg and leptonAnchoredCoeffs build the unique active $.\mathrm{neg}$ coefficient package once $\eta$ is fixed; leptonSectorClosure then states the concrete $\exists!$ match to lepton data at $\kappa_{\mathrm{lep}}=1/(4\pi\cdot 11)$. The same constant is plugged into the down-sector anchor amplitudes downAnchorCPosFromGen12 and downAnchorCPosFromGen23, so equality of those two expressions becomes the one-parameter consistency test under lepton anchoring.
In the broader RS picture this is the empirical tilt on the $\varphi$-ladder mass formula (yardstick times $\varphi^{\mathrm{rung}-8+\mathrm{gap}(Z)}$) after the leading rung assignment. It does not itself prove T5–T8; it supplies the sector-level number those closures need to become falsifiable against PDG.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.