leptonSignature
plain-language theorem explainer
Packages the lepton sector's sub-leading residual law as a negative-$B$-power signature with SDGT rung steps $(11,6)$ and free coupling $\kappa$. Anyone writing all-sector or lepton-anchored Item-8 closure cites this constant structure. The body is a pure structure literal; positivity of the two steps is discharged by `decide`.
Claim. For every real coupling $\kappa$, the lepton residual signature is the structure with $B$-power sign negative, generation steps $s_{12}=11$ and $s_{23}=6$, coupling equal to $\kappa$, and both steps strictly positive.
background
Item 8 is the open quark sub-leading mass correction. This module builds the smallest precise target that would close it and make an all-sector generalization falsifiable. The working object is a residual signature: sign of the sector $B$-power, two SDGT rung spacings (cube-cell counts from the $Q_3$ decomposition) for generations $1\to 2$ and $2\to 3$, and a real coupling.
Sector $B$-powers are not free parameters. For leptons the anchor formula gives $B_{\mathrm{pow}}=-(2E_{\mathrm{passive}})=-22$, hence the negative sign class. The pair $(11,6)$ is the derived SDGT spacing used for leptons; the coupling is left as an input so electromagnetic candidates such as $\kappa_{\mathrm{lep}}=1/(4\pi\cdot 11)$ can be plugged in downstream.
proof idea
Definition, not a proof. Instantiates the residual-signature structure with sign negative, step12 := 11, step23 := 6, and coupling := kappa. The two positivity fields are closed by decide on the concrete naturals.
why it matters
This is the lepton handle for every Item-8 multi-sector test. leptonSectorClosure freezes a unique active pair $(c_{\mathrm{Neg}},\eta)$ on this signature at the candidate electromagnetic coupling. allSectorTest and refinedAllSectorTest ask whether coefficients frozen on quarks also reproduce lepton residuals under $(11,6)$ and $\kappa_{\mathrm{lep}}$: an out-of-sample check, since leptons share the negative sign class with up quarks. leptonAnchoredTarget and signClassAllSectorTarget reverse the anchor or allow independent $\eta$ per sign class. Without a fixed lepton signature those propositions have no concrete sector data to match.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.