refinedItem8Specialized
plain-language theorem explainer
Specializes the refined Item 8 closure proposition to physical up- and down-quark residuals with the strong coupling fixed at α_s = 2/17 in both sectors and one shared η. Auditors of the RS sub-leading mass formula cite this as the concrete overdetermined test (three free parameters against four residual equations). The body is a one-line specialization of the general refined closure target.
Claim. The proposition that both the up-quark and down-quark residual pairs are simultaneously realized by the refined log-asymmetry ratio family with sector couplings $\kappa_{\mathrm{up}}=\kappa_{\mathrm{down}}=\alpha_s=2/17$ and a single universal $\eta$. Existence-uniqueness of those three parameters against the four residual equations is the content of the claim.
background
Item 8 is the open quark sub-leading correction in the RS mass ladder. The module builds the smallest precise target that would close it and make an all-sector generalization falsifiable. Residuals are organized by sector (lepton, up-quark, down-quark) and fed to a log-asymmetry ratio family whose free data are a pair of active coefficients and a universal tilt $\eta$.
The plain sign-split family is rigid: it forces a linear relation among generation steps that PDG residuals violate. The refined family absorbs that obstruction via a closed-form $\eta$ built from the gen-12 and gen-23 data, restoring solvability. Upstream work already gives constructive existence and uniqueness of $(c,\eta)$ on each signed sector separately, so a joint quark claim is a genuine overdetermined test rather than a tautology.
Here $\alpha_s$ is frozen at the RS-native value $2/17$, and both quark residual pairs are plugged into the general refined closure target as the specialized instance.
proof idea
Pure definitional specialization: the proposition is the general refined Item 8 closure target applied to the exact up-quark residual pair, the exact down-quark residual pair, and $\alpha_s$ in both coupling slots. No tactic proof; the mathematical content is whatever that general target asserts once those four arguments are fixed.
why it matters
This is the sharpest currently packaged falsification target for Item 8 inside the verification layer. Closing it would mean the three coefficients fixed by quark data are not free fits but a constrained solution of an overdetermined system, consistent with the RS mass formula on the $\phi$-ladder (yardstick times $\phi$ to a rung offset). The module already proves per-sector $\exists!$ for the refined family and the structural failure of the unrefined sign-split family; this definition names the joint quark instance that would finish the item. No downstream consumers are wired yet, so it stands as the named closure interface rather than a lemma in a longer chain. It does not by itself touch T5–T8 or the RCL; its role is mass-sector bookkeeping under the already-forced $\phi$ ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.