SignClassCoeffs
plain-language theorem explainer
Four real coefficients package two independent (amplitude, log-asymmetry) pairs, one for each B_pow sign class. Downstream mass-ratio fits cite this as the parameter space of the sign-class family. As a bare structure there is no proof: it is the carrier type for c and η on the negative and positive residual signatures.
Claim. A sign-class coefficient record is a 4-tuple $(c_{-},\eta_{-},c_{+},\eta_{+})\in\mathbb{R}^{4}$, giving one amplitude $c$ and one log-asymmetry $\eta$ for the negative $B_{\mathrm{pow}}$ sign class and one pair for the positive class.
background
Item 8 is the open quark sub-leading correction in the Recognition mass ladder. This module builds the smallest precise target that would close that item and make an all-sector generalization falsifiable: residual gen12/gen23 pairs per sector, fitted by families of coefficients against PDG-style data.
A residual signature carries a sign (from $B_{\mathrm{pow}}$), steps, and a coupling. The refined family uses a single $(c,\eta)$ per active sign; the sign-class family upgrades that to independent $\eta$ (and $c$) on each sign class so that up-quark, down-quark, and lepton sectors can share one global 4-parameter record while each sector still routes through its own sign.
Sibling constructions include residual pairs, ratio-family coefficients, and the three sector signatures (lepton, up, down). The module already proves rigidity and uniqueness results for the refined family; the sign-class record is the parameter type for the looser, all-sector test.
proof idea
No proof body: this is a structure definition with four ℝ fields. It only introduces the carrier type. Downstream definitions pattern-match on the signature sign and project the matching pair $(c,\eta)$ from the record.
why it matters
This record is the parameter space of the sign-class family: each sector’s gen12/gen23 residual is set by the $(c,\eta)$ of its $B_{\mathrm{pow}}$ sign, with overall scale from $c$ and the sector coupling. It feeds signClassFamily and the all-sector closure proposition signClassAllSectorTarget (six residual equations, four unknowns plus a free lepton $\kappa$).
In the Item 8 program, the refined family already has constructive solvability and uniqueness per sector. The sign-class layer is the next falsifiable step: one global 4-tuple must fit up, down, and lepton residuals at once. Collapse of sign-class to refined when $\eta_{-}=\eta_{+}$ is already recorded in the module summary, so this type sits on the path from per-sector $\exists!$ to a single cross-sector claim about sub-leading mass corrections on the $\varphi$-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.