leptonAnchoredCoeffs
plain-language theorem explainer
Packages the three refined-family coefficients after freezing the lepton sector: negative-branch amplitude from the lepton kappa, positive-branch amplitude set to zero, and the lepton-derived log-asymmetry eta. Anyone building out-of-sample quark residual predictions under lepton anchoring cites this package. It is a three-field structure constructor, not a proved equality.
Claim. Given a real lepton scale parameter $\kappa_\ell$, form the refined coefficient triple $(c_-, c_+, \eta)$ by taking $c_-$ from the lepton-anchored negative-branch amplitude at $\kappa_\ell$, setting $c_+ = 0$, and taking $\eta$ equal to the lepton-sector log-asymmetry. The zero $c_+$ records that leptons only freeze the negative sign-class branch.
background
Item 8 of the verification stack asks for a unified sub-leading mass formula that makes quark residuals falsifiable once lepton data fix the free coefficients. The refined family uses three globals: a negative sign-class amplitude $c_-$, a positive sign-class amplitude $c_+$, and a universal log-asymmetry $\eta$ that modulates the gen12/gen23 ratio.
Leptons live on the negative branch only, so the positive amplitude is unused for them. The module already proves existence and uniqueness of $(c_-,\eta)$ on any admissible negative-sector residual pair, and that $c_+$ is irrelevant for that sector. This definition simply assembles those lepton-frozen numbers into the RefinedCoeffs package that later predictions consume.
Downstream transport of PDG quark masses to the RS anchor scale $\mu^* = 182.201,\mathrm{GeV}$ (one-loop $\alpha_s$, $n_f=6$) is the bridge that lets the same package be evaluated on quark signatures.
proof idea
Pure structure construction: the triple is the constructor application with first component the lepton-anchored negative amplitude at the supplied $\kappa_\ell$, second component the literal $0$, and third component the fixed lepton eta. No lemmas, no tactics, no computation beyond packing three already-named reals.
why it matters
This is the coefficient handle for lepton-anchored out-of-sample tests. The immediate consumer is the up-sector prediction that evaluates the refined family on the up-quark signature after freezing $(c_-,\eta)$ on leptons; the same package feeds the paired down-sector amplitudes whose equality is the one-parameter consistency check under lepton anchoring.
In the Item 8 program, closing the quark sub-leading correction means showing that coefficients fixed by leptons either match scheme-consistent quark residuals or fail cleanly. Packaging $c_+=0$ with lepton $c_-$ and $\eta$ makes that freeze explicit and reusable. It sits downstream of the proved negative-sector $\exists!$ closure and upstream of the LO quark-transport scaffold that compares predictions to PDG residuals on the phi-ladder mass formula.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.