item8Specialized

The module builds the smallest precise target that would close Item 8 (the open quark sub-leading mass correction) and make an all-sector generalization falsifiable. Residuals live on a sign-split ratio family whose active coefficient and $\eta$ are to be frozen from data; the refined family is the solvable, unique form used once consistency of the bare family fails.

The general target item8ClosureTarget is a Prop-valued predicate on two residual datasets and two couplings. This definition specializes it: up and down exact residuals, and $\alpha_s=2/17$ (the RS strong coupling) on both sides. Sibling material already gives $\exists!$ solvability for each sign class of the refined family and structural rigidity of the bare ratio family.

Upstream species tags (e.g. deconfined up with 12 DOF) fix the particle bookkeeping; the mass-side residual signatures and $\phi$-ladder yardstick sit outside this Prop and are assumed by the residual data arguments.

Not a proof: a one-line def equal to the general Item 8 closure target applied to four concrete arguments (exact up residuals, exact down residuals, $\alpha_s$, $\alpha_s$). No tactics, no lemmas discharged. Establishing the resulting Prop is left to a later theorem.

Item 8 is the open quark sub-leading correction in the RS mass ladder. Specializing the closure target to both quark sectors at $\kappa=\alpha_s=2/17$ is the precise statement whose proof would freeze the two global family coefficients from quark data alone.

The module doc frames this as the hinge before all-sector checks: once those coefficients are frozen, lepton residuals (shared sign class with up quarks) become an out-of-sample test under a free $\kappa_{\mathrm{lep}}$. No used_by edges are recorded yet; the declaration is the named verification obligation, not a proved link in T0–T8. It sits in the Verification domain beside residual signatures, ratio-family consistency, and refined-family uniqueness.