leptonCrossDiff_ne_zero
plain-language theorem explainer
The lepton generation residuals have a non-vanishing weighted cross-difference 11·r₁₂ − 6·r₂₃. Anyone proving unique solvability of the lepton refined-family sector (Item 8) cites this non-degeneracy. The argument is a one-line reduction from the corresponding strict-positivity lemma via ne_of_gt.
Claim. The weighted cross-difference of the lepton generation residuals is nonzero: $11\,r_{12}^{\ell}-6\,r_{23}^{\ell}\neq 0$, where $r_{12}^{\ell}$ and $r_{23}^{\ell}$ are the observed lepton gen-1–2 and gen-2–3 residual values.
background
Item 8 of the Recognition verification stack asks for a unified sub-leading mass correction that fits all fermion sectors. The module builds a refined residual family whose active coefficients $(c,\eta)$ absorb the sign-split consistency violation that plain PDG ratios exhibit.
Solvability of that family on a fixed signature requires four numerical side conditions: nonzero gen-12 residual, distinct logarithmic steps, nonzero electromagnetic coupling, and a non-degenerate cross-difference of the two generation residuals. For leptons the candidate coupling is $\kappa_{\mathrm{lep}}=1/(4\pi\cdot 11)$, and the cross-difference takes the concrete weighted form $11,r_{12}-6,r_{23}$.
The present statement isolates that last non-degeneracy hypothesis as a standalone real inequality, so later uniqueness and existence theorems can invoke it by name rather than re-proving the arithmetic.
proof idea
One-line term proof. Apply the standard Mathlib lemma ne_of_gt to the already-established strict positivity result that the same weighted combination is positive. No further algebraic expansion is needed here.
why it matters
This non-degeneracy is a required hypothesis of the refined-family solvability theorems for the .neg sector. Downstream it is consumed by leptonSectorClosure, which freezes a unique active pair $(c_{\mathrm{Neg}},\eta)$ for the lepton signature at $\kappa_{\mathrm{lep}}=1/(4\pi\cdot 11)$, independently of the quark data.
That concrete $\exists!$ is the lepton half of the Item 8 closure target: once both lepton and quark sectors have unique refined coefficients, the all-sector sub-leading mass formula becomes a falsifiable numerical claim rather than an open fitting problem. Within the broader Recognition chain the result sits in the verification layer above the forcing landmarks (T5–T8, RCL, $\phi$-ladder masses); it does not re-derive those landmarks, but it makes their mass-side predictions checkable sector by sector.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.