refinedFamily_neg_solvable
plain-language theorem explainer
Any residual pair (g₁₂, g₂₃) with nonzero g₁₂, nonzero coupling κ, nondegenerate cross-difference D = g₁₂ s₁₂ − g₂₃ s₂₃, and distinct positive steps is hit by the refined family on a negative-sign sector. The proof builds explicit coefficients (cNeg, cPos=0, η) from the closed-form η-from-data formula and checks both components by the ηL identities. Cited by the full ∃! negative-sector closure.
Claim. Let $g_{12}, g_{23}, \kappa \in \mathbb{R}$ and $s_{12}, s_{23} \in \mathbb{N}$ with $s_{12}, s_{23} > 0$, $\kappa \neq 0$, $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 negative-sign signature $(s_{12}, s_{23}, \kappa)$ recovers the residual pair $(g_{12}, g_{23})$.
background
Item 8 is the open quark sub-leading mass correction in the Recognition Science verification stack. The module builds the smallest precise theorem layer that would close that item and make the all-sector generalization falsifiable.
A plain sign-split ratio family is too rigid: it forces $g_{12} s_{12} + g_{23} s_{23} = 0$, which PDG residuals violate. The refined family repairs this by three global coefficients $(c_{-}, c_{+}, \eta)$: two sign-class amplitudes and a universal log-asymmetry $\eta$ that modulates the gen12/gen23 ratio. On a negative-sign sector only $c_{-}$ and $\eta$ are active.
Upstream, $\eta$ is recovered in closed form from data, $\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$ (the $\eta L$ gen12/gen23 identities). Those identities are the algebraic engine of the existence proof.
proof idea
Constructive existence by explicit coefficients. First cast the positive naturals $s_{12}, s_{23}$ to nonzero reals. Invoke the two $\eta L$ identities for gen12 and gen23 to obtain the correction factor $1+\eta L$ and prove it is nonzero (rewrite via the gen12 identity, then cancel nonzero factors against $D$).
Witness coefficients are $c_{-} = g_{12}(s_{12}+s_{23})/(\kappa, s_{23},(1+\eta L))$, $c_{+}=0$, $\eta=\eta_{\mathrm{from,data}}(g_{12},g_{23},s_{12},s_{23})$.
Unfold the refined family and extensionalize on the residual pair. The gen12 component cancels directly by field simplification of $c_{-}\kappa s_{23}/\mathrm{total}\cdot(1+\eta L)$. The gen23 component substitutes both $\eta L$ identities and cancels $D/D$ after commuting the cross-difference.
why it matters
This is the existence half of negative-sector closure for Item 8. Downstream, refined_neg_sector_closure combines it with uniqueness to get full $\exists!$ on the active parameters $(c,\eta)$ for any admissible $.\mathrm{neg}$ sector; the sibling positive-sign solvability theorem mirrors the same construction. A helper showing $c_{+}$ is unused on negative signatures completes the sector package.
In the Recognition framework this is verification infrastructure, not a forcing-chain step: it makes the sub-leading mass correction (the log-asymmetry $\eta$ on the $\varphi$-ladder residuals) a uniquely solvable fit rather than an underdetermined ansatz. Once both sign sectors close, the all-sector generalization becomes a concrete falsifiable claim against PDG residual pairs. The module summary lists this among the sorry-free results that turn Item 8 from scaffolding into a closed local theorem.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.