upQuarkSignature
plain-language theorem explainer
Packages the up-quark sector residual law as a negative-B_pow signature with SDGT rung steps (13, 11) and free coupling κ. Anyone writing Item-8 closure, all-sector, or lepton-anchored residual tests cites this as the up-sector input. The body is a structure literal with positivity discharged by decide.
Claim. The up-quark residual signature at coupling $\kappa\in\mathbb{R}$ is the structure with sign class negative (matching $B_{\mathrm{pow}}(\mathrm{UpQuark})=-1$), generation steps $s_{12}=13$ and $s_{23}=11$, coupling field $\kappa$, and both steps strictly positive.
background
Item 8 concerns the open quark sub-leading mass correction. This module builds the smallest precise target that would close it: a single coefficient family whose predictions match exact up and down residual pairs, then freeze global coefficients for out-of-sample lepton tests.
A residual signature is the minimal sector package for that law: a $B_{\mathrm{pow}}$ sign class, two SDGT rung spacings $s_{12},s_{23}$ (cube-cell counts from the $Q_3$ decomposition), a real coupling, and positivity of the steps. Sector $B_{\mathrm{pow}}$ values are not free; they come from cube edge counting. For up quarks, $B_{\mathrm{pow}}=-1$, so the sign class is negative, shared with leptons.
The pair $(13,11)$ is the derived SDGT spacing for the up sector. The coupling argument is typically $\alpha_s$ (strong coupling) at the anchor scale when the signature is plugged into closure targets.
proof idea
Definitional structure instance, not a proof. Fields are set to $\mathrm{sign}=\mathrm{neg}$, $s_{12}=13$, $s_{23}=11$, $\mathrm{coupling}=\kappa$. The two positivity obligations $0<13$ and $0<11$ are closed by decide. No lemmas are invoked beyond that kernel decision procedure.
why it matters
This is the canonical up-sector input to every Item-8 verification object in the module. item8ClosureTarget and refinedItem8ClosureTarget demand unique coefficients whose predicted residuals on upQuarkSignature κ_up equal the exact up pair (and likewise for down). allSectorTest and refinedAllSectorTest reuse the same up signature at $\alpha_s$ so quark-frozen coefficients can be checked against lepton residuals.
Because up quarks and leptons share the negative $B_{\mathrm{pow}}$ class, freezing $c_{\mathrm{Neg}}$ on quarks (or on leptons in the anchored path) is a genuine cross-sector test: leptonAnchoredUpPrediction transports lepton-derived $(c,\eta)$ onto this signature at $\alpha_s$. Closing Item 8 would turn later lepton, genetic, and $\theta$ instantiations into out-of-sample checks rather than refits. The mass side sits on the RS $\phi$-ladder yardstick formula; this object only packages the sub-leading residual law's sector data.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.