signClassFamily
plain-language theorem explainer
Defines the four-parameter sign-class residual family: independent amplitude and log-asymmetry coefficients for each B_pow sign, producing generation 1→2 and 2→3 sub-leading corrections from a sector signature. Anyone testing Item 8 all-sector closure cites this map. The body is a pure constructor: branch on sign, form the weighted log-asymmetry ansatz, and package the pair.
Claim. Given global coefficients $(c_{-},\eta_{-},c_{+},\eta_{+})$ and a residual signature with sign $s\in\{+,-\}$, steps $s_{12},s_{23}>0$, and coupling $\kappa$, set $(c,\eta)=(c_{s},\eta_{s})$, $T=s_{12}+s_{23}$, $L=\log(s_{12}/s_{23})$, and return the residual pair $g_{12}=c\,\kappa\,s_{23}/T\,(1+\eta L)$, $g_{23}=-c\,\kappa\,s_{12}/T\,(1-\eta L)$.
background
Item 8 asks for a unified sub-leading mass correction across lepton and quark sectors. The module builds the smallest precise family that could close that item and make an all-sector fit falsifiable.
A residual signature packages the discrete data of one sector: the $B_{\mathrm{pow}}$ sign class, the two SDGT rung spacings $s_{12},s_{23}$ (cube-cell counts from the $Q_3$ decomposition), and a real coupling. A residual pair is simply the two real corrections $(g_{12},g_{23})$ for generations $1\to 2$ and $2\to 3$.
Sign-class coefficients supply four globals: amplitude and log-asymmetry pairs $(c_{-},\eta_{-})$ and $(c_{+},\eta_{+})$, one pair per sign. The refined family uses a single shared $\eta$; the sign-class family loosens that by allowing independent $\eta$ per sign while still tying amplitude to $c$ and the sector coupling.
proof idea
Definitional constructor, not a proof. Match on the signature sign to select the active pair $(c,\eta)$. Cast the natural steps to reals, form the total $T=s_{12}+s_{23}$ and the log-asymmetry $L=\log(s_{12}/s_{23})$, then assemble the weighted ansatz $g_{12}=c,\kappa,s_{23}/T,(1+\eta L)$ and $g_{23}=-c,\kappa,s_{12}/T,(1-\eta L)$. No lemmas are invoked beyond the structure fields and real arithmetic.
why it matters
This is the working residual map for the four-parameter Item 8 candidate. Downstream, signClassAllSectorTarget asserts existence of one coefficient tuple simultaneously matching up-quark, down-quark, and lepton residuals (six equations, four unknowns plus free lepton $\kappa$). The collapse theorem shows that equal $\eta$ values recover the refined three-parameter family, so the sign-class family strictly generalizes the refined ansatz.
In the Recognition mass ladder, these residuals are the sub-leading corrections on top of the $\varphi$-rung yardstick formula. Closing Item 8 would make the all-sector sub-leading law a concrete, falsifiable claim rather than a per-sector fit. The module already records that the stricter sign-split family is structurally rigid ($g_{12}s_{12}+g_{23}s_{23}=0$) and PDG-violating; this definition is the next, more flexible candidate under test.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.