item8ClosureTarget
plain-language theorem explainer
The smallest precise proposition that would close Item 8: unique global ratio-family coefficients simultaneously reproduce both exact up- and down-quark residual pairs at given couplings. Anyone freezing the two-sector mass-formula fit or setting up out-of-sample lepton tests cites this target. The body is a pure existence-uniqueness Prop, not a proved theorem.
Claim. Given exact up and down residual pairs $(r^{\mathrm{up}}_{12}, r^{\mathrm{up}}_{23})$ and $(r^{\mathrm{down}}_{12}, r^{\mathrm{down}}_{23})$, and couplings $\kappa_{\mathrm{up}}, \kappa_{\mathrm{down}} \in \mathbb{R}$, there exist unique ratio-family coefficients such that the family's predicted residuals on the up-quark signature at $\kappa_{\mathrm{up}}$ equal the up pair and those on the down-quark signature at $\kappa_{\mathrm{down}}$ equal the down pair.
background
Item 8 is the open quark sub-leading correction in the Recognition mass ladder. A residual pair is the pair of generation-step corrections $(g_{12}, g_{23})$ for rungs $1\to 2$ and $2\to 3$. The module builds the smallest theorem-shaped target that would place both quark sectors inside one closed coefficient family.
The candidate is a sign-split ratio family with two global coefficients $(c_{-}, c_{+})$. Predicted residuals are evaluated on sector signatures that carry a coupling $\kappa$ (typically $\alpha_s$). The plain sign-split family is rigid: it forces $g_{12}s_{12}+g_{23}s_{23}=0$ on every signature, a constraint PDG quark data violate (lepton data nearly satisfy it). Refined families with an $\eta$ parameter absorb that obstruction and already have per-sector $\exists!$ results in this module.
This definition packages the two-sector joint target: one coefficient set must hit both exact quark residual pairs at once.
proof idea
Definitional, not a proof. The body is the proposition $\exists!$ coeffs of type ratio-family coefficients such that predicted residuals on the up-quark signature at $\kappa_{\mathrm{up}}$ equal the supplied up residual pair and predicted residuals on the down-quark signature at $\kappa_{\mathrm{down}}$ equal the supplied down pair. No tactics or lemmas are applied; sibling uniqueness and solvability results for the refined family are the intended discharge path for specializations.
why it matters
This is the closure gate for Item 8. Downstream, item8Specialized instantiates it at the exact quark residuals with $\kappa=\alpha_s=2/17$ for both sectors; proving that instance freezes $(c_{-},c_{+})$ once and for all. Every later lepton, genetic, or $\theta$ residual match then becomes an out-of-sample test rather than a new fit, which is the module's stated falsifiability goal.
In the broader RS mass story the yardstick-$\phi$-ladder formula needs controlled sub-leading corrections; Item 8 is the quark half of that control. The module already proves structural obstruction of the plain sign-split family, closed-form $\eta$ identities, and per-sector refined $\exists!$. This target lifts those sector-wise facts to a single two-quark coefficient freeze.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.