leptonAnchoredCNeg
plain-language theorem explainer
Closed-form lepton anchor for the active negative-branch amplitude in the refined sub-leading mass family. Given a lepton coupling scale, it returns the unique c_neg fixed by the lepton gen-1/2 residual once eta is set to the lepton value. Anyone packaging lepton-anchored refined coefficients for Item 8 cites it. The body is a pure algebraic quotient, not a proof.
Claim. For a lepton coupling scale $\kappa_\ell\in\mathbb{R}$, the lepton-anchored negative amplitude is $c_{-}^{(\ell)}(\kappa_\ell)=\dfrac{r_{12}^{(\ell)}\,(11+6)}{\kappa_\ell\cdot 6\cdot\bigl(1+\eta_\ell\,\log(11/6)\bigr)}$, where $r_{12}^{(\ell)}$ is the lepton generation-1/2 residual and $\eta_\ell$ is the fixed lepton eta parameter.
background
Item 8 is the open quark sub-leading correction in the RS mass ladder. This module builds the smallest precise target that would close it: a sign-split refined residual family with coefficients $(c_{-},c_{+},\eta)$, solvability and uniqueness per sector, and an explicit lepton anchor that freezes the negative branch.
The refined family corrects generation residuals by a logarithmic step factor. Once $\eta$ is fixed to the lepton value $\eta_\ell$, the gen-1/2 equation becomes linear in the active coefficient $c_{-}$. The integers $11$ and $6$ are the generation step labels entering that log ratio $\log(11/6)$, matching the identities $1+\eta L=2 g_{12}s_{12}/D$ proved elsewhere in the module.
Sibling packaging then sets $c_{+}=0$ for leptons, because only the negative branch is frozen by lepton data.
proof idea
Definition, not a theorem. The body is the explicit algebraic solution of the lepton gen-1/2 residual equation for $c_{-}$: numerator residual times step sum $(11+6)$; denominator coupling times step $6$ times the eta-corrected log factor $(1+\eta_\ell\log(11/6))$. No lemmas are invoked; evaluation is direct once leptonGen12Residual and leptonEta are in scope.
why it matters
Feeds leptonAnchoredCoeffs, which packages $(c_{-},0,\eta_\ell)$ as the global lepton-anchored refined coefficient triple. That package is the LO scaffold for transporting PDG quark masses to the RS anchor scale and for making the all-sector Item 8 generalization falsifiable.
In the module's proved stack, refined-family solvability and uniqueness already give $\exists!$ $(c,\eta)$ on any negative sector. This definition supplies the concrete lepton-side $c_{-}$ that those uniqueness theorems guarantee exists, so downstream quark-transport and cross-sector consistency checks have a fixed numerical anchor rather than a free parameter.
It sits inside the verification layer of the mass-formula program (yardstick $\cdot\varphi^{\mathrm{rung}-8+\mathrm{gap}(Z)}$), not inside the T0–T8 forcing chain itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.