kappaLeptonCandidate_pos
plain-language theorem explainer
The lepton coupling candidate κ_lep = 1/(4π·11) is strictly positive. Anyone building the Item-8 refined mass family for the lepton sector cites this to justify division and nonzero-coupling hypotheses. The proof unfolds the definitions and finishes by Mathlib positivity on 4π·11.
Claim. Let $\kappa_{\mathrm{lep}} := 1/\alpha_{\mathrm{seed}}$ with geometric seed $\alpha_{\mathrm{seed}} = 4\pi\cdot 11$. Then $0 < \kappa_{\mathrm{lep}}$.
background
Item 8 is the open quark sub-leading correction in the Recognition Science mass ladder. This module builds the smallest precise theorem layer that would close that item and make an all-sector generalization falsifiable: sign-split residual families, a closed-form η that absorbs consistency violations, and refined families with unique solvable coefficients per sector.
The electromagnetic geometric seed is $\alpha_{\mathrm{seed}} = 4\pi\cdot 11$, the baseline spherical closure cost over 11-edge interaction paths (ledger structure). The lepton coupling candidate is the reciprocal $\kappa_{\mathrm{lep}} = 1/\alpha_{\mathrm{seed}}$. Downstream refined-family solvability needs a nonzero coupling; positivity is the first arithmetic fact on that candidate.
proof idea
Term-mode one-liner after unfolding. Expand kappaLeptonCandidate to $1/\texttt{Constants.alpha_seed}$ and alpha_seed to $4\pi\cdot 11$, then apply Mathlib's positivity tactic, which discharges $0 < 1/(4\pi\cdot 11)$ from $4>0$, $\pi>0$, and $11>0$.
why it matters
Feeds kappaLeptonCandidate_ne_zero immediately via ne_of_gt, which is the form refined-family hypotheses typically demand (nonzero coupling). In the Item-8 closure stack, lepton-sector solvability and uniqueness for the refined family require a nonzero active coupling; this pins the RS electromagnetic seed reciprocal as a concrete positive real rather than an abstract parameter.
Framework link: $\alpha^{-1}$ lives in the certified band near 137, and the seed $4\pi\cdot 11$ is the geometric baseline of that pipeline. The theorem does not close Item 8 itself; it only clears the positivity gate for the lepton κ candidate used in residual-family constructions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.