leptonCrossDiff_pos

Item 8 Closure Target builds the smallest precise theorem layer that would close the open quark sub-leading mass correction and make the all-sector generalization falsifiable. Residuals measure how far an observed mass ratio sits from a pure φ-ladder step: $R = \mathrm{rungResidual}(m_a/m_b, n)$ compares $\log(m_a/m_b)/\log\varphi$ to the integer rung $n$.

For leptons the gen-12 residual uses the μ/e ratio at step 11, and the gen-23 residual uses τ/μ at step 6. Upstream, $R_{12}^{\ell}>0$ because the observed μ/e ratio exceeds $\varphi^{11}$, while $R_{23}^{\ell}<0$ because τ/μ lies below $\varphi^{6}$. The cross-difference $11 R_{12}-6 R_{23}$ is the non-degeneracy quantity that refined-family solvability demands of any residual pair.

One-line wrapper. Feed nlinarith the two signed residual facts: $R_{12}^{\ell}>0$ and $R_{23}^{\ell}<0$. With positive coefficients 11 and 6, the product $11 R_{12}$ is positive and $-6 R_{23}$ is positive, so their sum (equivalently the stated difference) is strictly positive. No unfolding of rungResidual or PDG constants is needed at this layer.

Direct parent is leptonCrossDiff_ne_zero, obtained by ne_of_gt from this positivity. Nonzero cross-difference is a hypothesis of the refined-family solvability theorems (refinedFamily_neg_solvable / refinedFamily_pos_solvable) that underwrite unique $(c,\eta)$ closure per sector. For leptons this freezes the candidate electromagnetic coupling path toward ∃! sector closure. In the broader RS picture the residuals sit on the φ-ladder mass formula (yardstick · φ^{rung−8+gap}); the sign pattern and non-degeneracy are what let the η-corrected sub-leading formula absorb the consistency violation that the bare sign-split family cannot.