refinedFamily_pos_solvable
plain-language theorem explainer
For any positive-sign sector signature with nonzero steps, nonzero coupling, nonzero gen12 residual, nondegenerate cross-difference, and distinct rung steps, there exist refined coefficients (cNeg, cPos, η) whose refined family recovers a prescribed residual pair (g12, g23). Mass-formula auditors cite this for constructive solvability of the Item-8 sub-leading correction on BpowSign.pos sectors. The proof builds the coefficients explicitly from etaFromData and checks both residual components by field simplification against the η-log identities.
Claim. Fix residuals $g_{12}, g_{23} \in \mathbb{R}$, positive natural steps $s_{12}, s_{23} > 0$, and coupling $\kappa \neq 0$. Assume $g_{12} \neq 0$, $g_{12} s_{12} - g_{23} s_{23} \neq 0$, and $\log(s_{12}/s_{23}) \neq 0$. Then there exist refined coefficients $(c_{-}, c_{+}, \eta)$ such that the refined family on the positive-sign signature $(\mathrm{pos}, s_{12}, s_{23}, \kappa)$ equals the residual pair $(g_{12}, g_{23})$.
background
Item 8 Closure Target packages the smallest precise theorem layer that would close the open quark sub-leading correction and make the all-sector generalization falsifiable. The plain sign-split ratio family is too rigid: consistency forces $g_{12} s_{12} + g_{23} s_{23} = 0$, which PDG residuals violate. The refined family adds a universal log-asymmetry $\eta$ that modulates the gen12/gen23 ratio and absorbs that violation.
RefinedCoeffs holds three globals: inactive/active sign-class amplitudes $c_{-}, c_{+}$ and the log-asymmetry $\eta$. BpowSign is the sign class of $B_{\mathrm{pow}}$ (here .pos). Sector signatures carry the SDGT rung spacings $s_{12}, s_{23}$ (cube-cell counts from the $Q_3$ decomposition) and a coupling $\kappa$.
Upstream, etaFromData supplies 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 $1+\eta L = 2 g_{12}s_{12}/D$ and $1-\eta L = -2 g_{23}s_{23}/D$ (etaL_gen12_identity, etaL_gen23_identity). Those identities are the algebraic engine of the constructive solve.
proof idea
Constructive existence by explicit coefficients. First discharge the obvious nonzero casts $s_{12}, s_{23} \neq 0$ from positivity. Invoke etaL_gen12_identity and etaL_gen23_identity on $(g_{12}, g_{23}, s_{12}, s_{23})$ under the cross-difference and log hypotheses.
From the gen12 identity, deduce that the correction factor $1 + \eta_{\mathrm{data}} \cdot \log(s_{12}/s_{23})$ is nonzero (rewrite and use $g_{12} \neq 0$, $s_{12} \neq 0$, $D \neq 0$). Commute the cross-difference into the two orderings needed by later field_simp.
Witness coefficients: $c_{-} = 0$, $\eta = \mathrm{etaFromData}(g_{12},g_{23},s_{12},s_{23})$, and
$c_{+} = g_{12}(s_{12}+s_{23})/(\kappa, s_{23},(1+\eta_{\mathrm{data}} L))$.
Unfold refinedFamily, split on residual components: gen12 falls by field_simp; gen23 rewrites via both $\eta L$ identities then field_simp on the commuted denominators.
why it matters
This is the positive-sign half of the constructive solvability pillar for Item 8. Together with refinedFamily_neg_solvable it shows every admissible residual pair is hit by the refined family on its sector signature. The module pairs it with refinedFamily_pos_unique to obtain sectorwise $\exists!$ of the active coefficient and $\eta$; the negative side already closes fully as refined_neg_sector_closure.
In the Recognition mass ladder, sub-leading corrections sit on top of the $\phi$-rung yardstick formula. Closing Item 8 means the quark (and lepton) residual structure is no longer an ad-hoc fit but a uniquely solved coefficient problem once the signature and residuals are fixed. The $\eta$-log modulation is the minimal deformation that escapes the consistency obstruction of the plain ratio family while remaining algebraically rigid.
No downstream consumers are wired yet (used_by empty); the intended landing is the full positive-sector $\exists!$ closure and the eventual all-sector falsifiable statement against PDG residuals. Framework landmarks touched: $\phi$-ladder mass formula and the eight-tick/$Q_3$ rung spacings that supply $s_{12}, s_{23}$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.