refinedFamily
plain-language theorem explainer
The refined residual family maps three global coefficients (two sign-class amplitudes and a universal log-asymmetry η) and a sector signature to the pair of generation-step corrections (1→2 and 2→3). Anyone closing Item 8 (quark sub-leading masses) or proving single-sector ∃! cites it as the candidate law. The body is a pure definition: pick the active amplitude by sign, weight by opposite step over total, and modulate by ±η log(s₁₂/s₂₃).
Claim. Given refined coefficients $(c_{-}, c_{+}, \eta)$ and a residual signature with sign $\sigma$, rung steps $s_{12}, s_{23} > 0$, and coupling $\kappa$, let $c$ be $c_{-}$ if $\sigma$ is negative and $c_{+}$ if positive, $T = s_{12}+s_{23}$, and $L = \log(s_{12}/s_{23})$. The refined family returns the residual pair $$g_{12} = c\,\kappa\,\frac{s_{23}}{T}(1+\eta L),\qquad g_{23} = -c\,\kappa\,\frac{s_{12}}{T}(1-\eta L).$$
background
Item 8 asks for a unified sub-leading mass correction across lepton and quark sectors. A residual signature packages the minimal sector data: a Bpow sign class, two positive natural rung steps $s_{12}, s_{23}$ (cube-cell counts from the $Q_3$ decomposition), and a real coupling $\kappa$. A residual pair is simply the two real corrections $g_{12}$ (gen $1\to 2$) and $g_{23}$ (gen $2\to 3$).
The coarser sign-split family (ratio family) forces the rigidity $g_{12}s_{12}+g_{23}s_{23}=0$, which PDG data violate. Refined coefficients add a single universal log-asymmetry $\eta$ beside the two sign-class amplitudes $c_{-}, c_{+}$. The module builds the smallest precise theorem layer that would close Item 8 and make the all-sector generalization falsifiable.
At $\eta=0$ the refined law collapses exactly to the ratio family. The closed-form data formula for $\eta$ absorbs the consistency defect via algebraic identities $1+\eta L=2 g_{12}s_{12}/D$ and $1-\eta L=-2 g_{23}s_{23}/D$.
proof idea
Definition, not a proof. Match on the signature sign to select the active amplitude ($c_{-}$ for .neg, $c_{+}$ for .pos). Cast the two natural steps to reals, form their sum $T$ and the log-asymmetry $L=\log(s_{12}/s_{23})$, then assemble the residual pair by the weighted formulas above: each generation correction is proportional to the opposite step over $T$, times $(1\pm\eta L)$, with an overall minus on $g_{23}$. No lemmas are invoked; downstream theorems unfold this definition by simp.
why it matters
This is the candidate law for Item 8 closure: the smallest family that keeps two global sign-class amplitudes plus one universal $\eta$ while remaining solvable and unique on each sector. Downstream, refinedFamily_neg_solvable / refinedFamily_pos_solvable construct explicit $(c,\eta)$ from data, and the matching uniqueness theorems give single-sector $\exists!$. Helpers neg_cPos_irrelevant and pos_cNeg_irrelevant show the inactive amplitude is free. refined_at_eta_zero embeds the older ratio family as the $\eta=0$ slice.
leptonSectorClosure freezes $(c_{-},\eta)$ on the lepton .neg sector at the candidate electromagnetic coupling $\kappa_{\mathrm{lep}}=1/(4\pi\cdot 11)$, independent of quark data. That separation is what makes an all-sector generalization falsifiable: quarks must reuse the same $\eta$ (or a controlled deformation) once leptons fix it. In the broader RS chain this sits under mass-ladder sub-leading structure (phi-ladder rungs and sector couplings), not under T5–T8 forcing itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.