refinedItem8ClosureTarget
plain-language theorem explainer
Unique refined coefficients are required to match both up- and down-quark residual pairs under the log-asymmetry ratio family at given couplings. Anyone testing whether a three-parameter sub-leading mass correction can close Item 8 for quarks cites this predicate. The body is the joint ∃! statement itself: a Prop definition, not a proved theorem.
Claim. Given residual pairs $(g_{12}^{\mathrm{up}},g_{23}^{\mathrm{up}})$ and $(g_{12}^{\mathrm{down}},g_{23}^{\mathrm{down}})$ and couplings $\kappa_{\mathrm{up}},\kappa_{\mathrm{down}}\in\mathbb{R}$, there exist unique refined coefficients such that the refined prediction on the up-quark signature at $\kappa_{\mathrm{up}}$ equals the up pair and the refined prediction on the down-quark signature at $\kappa_{\mathrm{down}}$ equals the down pair.
background
Item 8 is the open quark sub-leading correction on the Recognition Science mass ladder (yardstick times $\phi$ raised to a rung). A residual pair packages the two generation steps $1\to 2$ and $2\to 3$. The bare sign-split ratio family is rigid: consistency forces $g_{12}s_{12}+g_{23}s_{23}=0$, which PDG data violate (consistency_of_ratioFamily).
The refined family adds a log-asymmetry parameter $\eta$ that absorbs the violation via the closed form $\eta=(g_{12}s_{12}+g_{23}s_{23})/(\ln(s_{12}/s_{23})\cdot(g_{12}s_{12}-g_{23}s_{23}))$, with algebraic identities reducing $c$ to a single division. The module already proves per-sector solvability and uniqueness for each sign class. This definition packages the joint two-sector uniqueness claim that would close Item 8.
proof idea
No proof body: this is a Prop-valued definition. It asserts unique existence of one RefinedCoeffs triple whose refined predictions simultaneously reproduce both supplied residual pairs on the up- and down-quark signatures at the given couplings. Downstream specializations freeze the data and $\kappa$; the per-sector $\exists!$ theorems (refinedFamily_neg_unique / refinedFamily_pos_unique, and refined_neg_sector_closure) are the local pieces the joint claim would combine.
why it matters
Direct parent is refinedItem8Specialized, which freezes both couplings to $\alpha_s=2/17$ and asks whether one universal $\eta$ fits both quark sectors. That specialization is overdetermined (3 parameters, 4 equations) and is therefore a genuine falsification target, not a tautology. The module already records the obstruction: current mixed-scheme PDG quark data yield incompatible $\eta$ (lepton $\eta$ perturbative at $\sim 4%$; up-sector $\eta$ non-perturbative and sign-flipping). Settling this target decides whether the refined log-asymmetry family is the right sub-leading correction on the $\phi$-ladder mass formula across sectors, which is the content of Item 8 in the verification chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.