Z_lepton
plain-language theorem explainer
The lepton-sector band label is the even quartic Z = a Q̃² + b Q̃⁴ evaluated at the integerized electron charge Q̃ = −6. Mass-layer forcing and anomalous-moment arguments cite it when fixing or applying the topological Z-map. It is a one-line specialization of the general degree-≤4 even polynomial to that fixed charge.
Claim. For integer coefficients $a,b$, the lepton band label is $Z_{\ell}(a,b) := a\,\tilde{Q}_{\ell}^{2} + b\,\tilde{Q}_{\ell}^{4}$, where $\tilde{Q}_{\ell} = -6$ is the face-count integerization $6Q$ of the electron charge $Q=-1$.
background
This module derives the charge-to-band map from recognition boundaries on the 3-cube, without anchor masses. Stage 1 fixes the integerization scale: a boundary of charge $Q$ couples to the $F=2D$ faces, and at $D=3$ one has $F=6$, the least positive even $k$ with $kQ\in\mathbb{Z}$ for all SM charges ${-1,2/3,-1/3}$. Thus $\tilde{Q}:=6Q$, and for the electron $\tilde{Q}_{\ell}=-6$.
Stage 2 requires the band label $Z$ to be even in $\tilde{Q}$, non-negative, and zero at neutrality. The minimal such polynomial is $Z=a\tilde{Q}^{2}+b\tilde{Q}^{4}$ (no constant term). The in-module Z_poly is exactly that form: $a Q^{2}+b Q^{4}$. Stage 3 adds a color offset only in the quark sector; leptons stay bare.
So the lepton map is the bare polynomial at the fixed lepton charge, still parametric in $(a,b)$ until family separation forces $a=b=1$.
proof idea
Pure definitional specialization: apply the general even polynomial $Z_{\mathrm{poly}}(a,b,Q)=a Q^{2}+b Q^{4}$ at $Q=\tilde{Q}_{\ell}=-6$. No tactics, no lemmas beyond unfolding those two defs.
why it matters
This is the lepton half of Stage 3 in the topological Z-map derivation (module doc: $Z_{\mathrm{lepton}}=\tilde{Q}^{2}+\tilde{Q}^{4}$ once $a=b=1$). Downstream, bare_Z_values evaluates it at $(1,1)$ to get $1332$, matching the mass-layer anchor ChargeIndex.Z Sector.Lepton (-1)=1332. That equality is the lepton hypothesis of canonical_tuple_forced_from_anchor_outputs, which forces $(a,b,c)=(1,1,4)$ from topology-compatible family forms. Anomalous-moment code reuses the same numerical $Z=1332$ for a universal lepton gap on the $\varphi$-ladder (anomalous_e_tau_universal, gap_lepton). The construction sits on T8 ($D=3\Rightarrow F=6$ faces, color offset $2^{D-1}=4$) and feeds the mass formula via the charge-index rung.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.