leptonLogAsym_ne_zero

The ambient module builds the smallest precise theorem layer that would close Item 8 (the open quark sub-leading mass correction) and make the all-sector residual family falsifiable. Residuals are organized by sector signatures and a refined coefficient family $(c,\eta)$ whose closed-form $\eta$ involves logarithms of generation-step ratios in the denominator.

In the lepton sector the concrete rational $11/6$ appears as a log-asymmetry factor tied to the candidate electromagnetic coupling $\kappa_{\mathrm{lep}}=1/(4\pi\cdot 11)$ and the $\mu/e$ residual structure. A sibling positivity result already shows $\log(11/6)>0$ (the observed ratio sits above the corresponding $\varphi$-ladder threshold). Non-vanishing is the weaker algebraic fact needed before uniqueness and solvability arguments may divide by that factor.

One-line term proof. Apply the standard real fact that every strictly positive real is nonzero to the upstream positivity lemma establishing $\log(11/6)>0$. No further arithmetic is required.

Feeds the concrete lepton-sector closure theorem, which asserts unique active coefficients $(c,\eta)$ for the lepton negative-sign sector at the candidate coupling $\kappa_{\mathrm{lep}}=1/(4\pi\cdot 11)$, independent of quark data. That closure is one of the proved $\exists!$ pillars listed in the module summary (solvability plus uniqueness for refined families on a fixed signature).

Without non-vanishing of the lepton log-asymmetry, the refined-family identities and the cancellation steps that freeze $\eta$ would be blocked. The result is local bookkeeping inside the Item 8 verification stack rather than a new forcing-chain landmark, but it is required before the lepton residual can be treated as a closed, data-matched sector alongside the quark cases.