kappaLeptonCandidate
plain-language theorem explainer
Defines the leading lepton electromagnetic coupling candidate as the reciprocal of the RS geometric seed: κ_lep = 1/(4π·11). Anyone working the Item 8 lepton-anchored closure or refined-family uniqueness cites this constant. It is a one-line noncomputable real definition, not a proved statement.
Claim. The lepton coupling candidate is the real number $\kappa_{\mathrm{lep}} := 1/\alpha_{\mathrm{seed}}$, where the electromagnetic seed is the geometric ledger quantity $\alpha_{\mathrm{seed}} = 4\pi \cdot 11$. Equivalently, $\kappa_{\mathrm{lep}} = 1/(4\pi \cdot 11)$.
background
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. The refined family solves for active coefficients $(c,\eta)$ against residual signatures; uniqueness and existence are already proved for any admissible residual pair.
The electromagnetic seed $\alpha_{\mathrm{seed}} = 4\pi \cdot 11$ is the geometric baseline spherical closure cost over 11-edge interaction paths (ledger structure). Its reciprocal is the natural dimensionless coupling scale for the lepton sector before higher-order running or curvature corrections enter.
In RS-native units the fine-structure band sits near $\alpha^{-1}\in(137.030,137.039)$; the seed $4\pi\cdot 11\approx 138.23$ is the leading geometric input from which that band is refined.
proof idea
Pure definition: unfold to $1/\mathrm{Constants.alpha_seed}$, with $\mathrm{alpha_seed}=4\pi\cdot 11$. No tactics, no lemmas. Downstream positivity and non-zeroness are immediate from $\pi>0$ and the constant $11>0$.
why it matters
Freezes the lepton-sector coupling so that refined-family uniqueness can be stated at a concrete electromagnetic scale, independent of quark data. Downstream, leptonSectorClosure gives $\exists!$ for the lepton $.\mathrm{neg}$ sector at this $\kappa_{\mathrm{lep}}$, and leptonAnchoredAnchorTest uses the same candidate as the anchor-scale falsification target (up prediction must match transported residuals; down sector must induce a single consistent $c_{+}$).
This is the lepton half of the Item 8 closure strategy: lock $\kappa$ from the RS seed, solve $(c,\eta)$ uniquely on lepton residuals, then transport the anchor into the quark sectors. It sits upstream of the all-sector generalization that would finish the sub-leading mass formula.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.