ResidualSignature
plain-language theorem explainer
Packages the minimal data of a fermion sector's sub-leading mass correction: a B_pow sign class, two positive SDGT rung spacings (gen 1→2 and 2→3), and one coupling scalar. Downstream ratio and refined families read only this bundle, so equal signatures force equal residual predictions. Cited wherever Item 8 sector instances (leptons, up/down quarks) are built or consistency is checked.
Claim. A residual signature is a 4-tuple $(\sigma, s_{12}, s_{23}, \kappa)$ with $\sigma \in \{\mathrm{neg},\mathrm{pos}\}$ the sign class of $B_{\mathrm{pow}}$, $s_{12}, s_{23} \in \mathbb{N}$ the sector SDGT rung spacings for generations $1\to 2$ and $2\to 3$ (required positive), and $\kappa \in \mathbb{R}$ a coupling weight.
background
Item 8 of the Recognition verification stack concerns the open quark sub-leading mass corrections. This module builds the smallest precise theorem target that would close that item and make an all-sector generalization falsifiable: one closed residual family, frozen global coefficients, and out-of-sample tests on later sectors.
The sign class BpowSign is the two-valued inductive type {neg, pos} induced by the sign of $B_{\mathrm{pow}}$. The integers $s_{12}$ and $s_{23}$ are the sector-specific SDGT rung spacings, interpreted as cube-cell counts from the $Q_3$ decomposition; they weight the generation steps in the candidate families. The coupling $\kappa$ is the single continuous scalar left free once sign and steps are fixed.
Upstream rung tables (e.g. electron 2, muon 13, tau 19; up/charm/top and down/strange/bottom sharing 4, 15, 21) fix the integer ladder positions; the residual signature abstracts only the differential step data needed for the sub-leading law, not the absolute rungs themselves.
proof idea
Definitional structure, no proof body. Fields are declared with positivity side-conditions 0 < step12 and 0 < step23 as structure fields (so every inhabitant carries the inequalities). Downstream constructors such as leptonSignature and downQuarkSignature discharge those obligations by decide on concrete naturals.
why it matters
This is the carrier type for every Item 8 family. ratioFamily and predictedResiduals take a residual signature and emit a residual pair; consistency_of_ratioFamily proves the structural identity $g_{12} s_{12} + g_{23} s_{23} = 0$ for that family, and consistency_necessary lifts the identity to any exact pair the family matches. Concrete sector bundles (leptonSignature with steps $(11,6)$ and negative sign; downQuarkSignature with $(6,8)$ and positive sign; likewise up-quark) are instances of this structure.
Equal signatures give equal predictions (same_signature_same_prediction), which is the no-extra-knob property needed so that freezing $(c_{\mathrm{Neg}}, c_{\mathrm{Pos}})$ turns later lepton, genetic, or $\theta$ instantiations into genuine out-of-sample tests. The refined family and its $\exists!$ sector-closure theorems also quantify over this type. In the broader RS picture it sits on the $\varphi$-ladder mass formula (yardstick times $\varphi^{\mathrm{rung}-8+\mathrm{gap}}$), isolating the sub-leading correction layer that Item 8 must close.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.