BpowSign
plain-language theorem explainer
Two-valued sign class for the exponent of the sub-leading mass correction: negative or positive. Sector residual signatures carry this tag so the refined ratio family can branch on which coefficient is active. Anyone citing Item 8 closure or single-sector ∃! solvability needs it. The declaration is a bare inductive enumeration with decidable equality.
Claim. There is a two-element type $\{\mathrm{neg},\,\mathrm{pos}\}$ classifying the sign of $B_{\mathrm{pow}}$ in the sub-leading mass correction law.
background
Item 8 of the Recognition verification stack concerns the open quark sub-leading mass correction. The module builds the smallest theorem framework that would close that item and make an all-sector generalization falsifiable.
The correction law is organized by a residual signature: a sign tag, two sector-specific SDGT rung spacings (cube-cell counts from the $Q_3$ decomposition), and a coupling. The sign tag records whether $B_{\mathrm{pow}}$ is negative or positive, which selects which coefficient in the refined ratio family is active.
Downstream, the refined family for the negative branch is shown solvable and unique under mild non-degeneracy hypotheses on the residual pair and the steps. The same sign class appears in the specialized Item 8 target that freezes quark coefficients at $\kappa=\alpha_s=2/17$.
proof idea
No proof body: the declaration is an inductive type with constructors neg and pos, deriving DecidableEq and Repr. It is pure data, not a derived theorem.
why it matters
This tag is the first field of ResidualSignature, the structural carrier for every sector's sub-leading law. Solvability and uniqueness theorems for the refined family (refinedFamily_neg_solvable and its positive twin) case-split on it; the specialized Item 8 closure proposition and the lepton-anchored anchor test both thread signatures that carry it.
In the broader RS picture the mass formula sits on the $\varphi$-ladder (yardstick times $\varphi^{\mathrm{rung}-8+\mathrm{gap}(Z)}$). Item 8 is the remaining obstruction to a uniform sub-leading correction across lepton and quark sectors. Freezing the sign class as a discrete choice is what lets the module state a precise $\exists!$ per sector and a falsifiable all-sector target once quark data fix the global coefficients.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.