leptonGen12Residual_ne_zero
plain-language theorem explainer
The generation-1–2 lepton mass residual is nonzero. Anyone proving unique solvability of the refined sub-leading mass family in the lepton sector needs this nondegeneracy hypothesis. The proof is a one-line wrapper: positivity of the residual implies it cannot vanish.
Claim. The signed residual of the first-to-second generation lepton mass ratio against its pure $\varphi$-ladder prediction is nonzero: $r_{12}^{(\ell)} \neq 0$.
background
Item 8 of the Recognition verification stack asks for a unified sub-leading correction to the pure $\varphi$-ladder mass formula across lepton and quark sectors. Residuals measure the signed mismatch between an observed generation ratio and the corresponding integer power of $\varphi$ (the self-similar fixed point forced at T6). The generation-1–2 lepton residual is the first coordinate of the lepton residual pair.
The refined family that absorbs these residuals is solvable only when the gen-12 residual is nonzero, the cross-difference of steps is nondegenerate, and the sector coupling is nonzero. The module therefore isolates each of those nondegeneracy facts as a named lemma before assembling sector closures.
Local setting: the Item 8 closure target develops the smallest precise theorem framework that would close the open quark sub-leading correction and make the all-sector generalization falsifiable. Lepton data are treated first because the candidate electromagnetic coupling $\kappa_{\mathrm{lep}}=1/(4\pi\cdot 11)$ freezes independently of the quarks.
proof idea
One-line term proof. Apply the standard real lemma ne_of_gt to the already-proved positivity statement that the generation-1–2 lepton residual is strictly positive. No algebraic expansion or case split is required.
why it matters
Feeds leptonSectorClosure, the concrete $\exists!$ closure for the lepton negative-sign sector at $\kappa_{\mathrm{lep}}=1/(4\pi\cdot 11)$. That parent freezes the active pair $(c_{-},\eta)$ independently of quark data. Nonzero gen-12 residual is exactly the nondegeneracy hypothesis demanded by the refined-family solvability theorems (refinedFamily_neg_solvable and the combined refined_neg_sector_closure).
In the broader Recognition chain this sits downstream of the $\varphi$-ladder mass formula (yardstick times $\varphi^{\mathrm{rung}-8+\mathrm{gap}(Z)}$) and of T6 forcing of $\varphi$. It does not itself touch T5 J-uniqueness or the eight-tick octave; it only certifies that the lepton gen-12 data point is off the pure ladder, so a genuine sub-leading coefficient is forced rather than optional.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.