leptonSectorClosure
plain-language theorem explainer
Unique existence of real coefficients (c, η) matching the refined lepton mass residuals at the candidate coupling κ_lep = 1/(4π·11). Freezes the active negative-sector pair independently of all quark data. Anyone citing Item-8 sub-leading mass closure for leptons uses this. Proof is a direct specialization of the general negative-sector ∃! lemma to lepton residuals and steps 11 and 6.
Claim. There exist $c,\eta\in\mathbb{R}$ such that the refined family with coefficients $\langle c,0,\eta\rangle$ on the lepton signature at $\kappa_{\mathrm{lep}}=1/(4\pi\cdot 11)$ equals the observed lepton residuals, and whenever any triple $\langle c',p',\eta'\rangle$ also matches those residuals on the same signature, one has $c'=c$ and $\eta'=\eta$.
background
Item 8 is the open sub-leading correction in the RS mass formula (yardstick times a φ-ladder rung with a residual gap). This module builds the smallest precise theorem layer that would close that item sector-by-sector and make the all-sector claim falsifiable.
The refined family is a three-coefficient ansatz $\langle c_{\mathrm{Neg}},c_{\mathrm{Pos}},\eta\rangle$ acting on a residual signature (generation steps, coupling κ, and signed residual pair). For a negative-sector signature only the active pair $(c_{\mathrm{Neg}},\eta)$ enters; $c_{\mathrm{Pos}}$ is idle. Solvability and uniqueness of that active pair are already proved in general as refined_neg_sector_closure: nonzero gen-12 residual, nondegenerate cross-difference, distinct positive steps, and nonzero κ force a unique $(c,\eta)$ matching any observed residual pair.
Here the lepton data are plugged in: generation steps $s_{12}=11$, $s_{23}=6$, candidate electromagnetic coupling $\kappa_{\mathrm{lep}}=1/(4\pi\cdot 11)$, and the concrete lepton residual pair. The theorem therefore freezes lepton $(c_{\mathrm{Neg}},\eta)$ with no reference to quark residuals.
proof idea
One-line specialization of the general negative-sector closure. Two trivial positivity facts $0<11$ and $0<6$ are discharged by norm_num. The goal is then rewritten by simpa along the definitions of the lepton signature and observed residuals, and handed to refined_neg_sector_closure applied to the lepton gen-12/gen-23 residuals, steps 11 and 6, kappaLeptonCandidate, and the four nonzero hypotheses (coupling, gen-12 residual, cross-difference, log-asymmetry). No new algebra is performed at this site.
why it matters
Gives the concrete lepton half of the Item-8 ∃! package advertised in the module summary: full unique solvability for any negative sector, instantiated at the lepton candidate coupling. Because the active pair is frozen independently of quark data, lepton and quark sectors can be closed (or falsified) separately before any joint consistency check. Downstream the same pattern is intended for up- and down-quark signatures; together they feed the unified sub-leading mass formula and the falsifiable all-sector generalization. No parent theorem yet cites this declaration (used-by is empty), so it currently sits as a terminal verification lemma rather than an intermediate step in a larger proved chain. Framework landmarks touched: the φ-ladder mass formula and the electromagnetic coupling scale that sits near the RS α band.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.