Z_lepton
plain-language theorem explainer
Z_lepton assigns the constant integer 1332 to every member of the Lepton inductive type. Researchers deriving RS corrections to lepton anomalous moments cite this shared value to obtain a universal φ-ladder term independent of generation. The definition follows at once from the charge scaling Q = -1, which produces Q6 = -6 and the integer map Z = Q6² + Q6⁴.
Claim. For every lepton species $l$, define the integer $Z(l) := 1332$, obtained from the scaled charge map with $Q = -1$ via $Z = (6Q)^2 + (6Q)^4$.
background
The module extends the φ-ladder residue mechanism to QED anomalous moments $a_l = (g-2)/2$ for charged leptons. All three species share the same gauge charge $Q = -1$, so they receive the identical integer $Z = 1332$ that enters the RS correction term. The upstream Anchor.Z definition supplies the general formula $Z = Q6^2 + Q6^4$ for the lepton sector with $Q6 = 6Q$, while the local Lepton inductive type enumerates the three charged species e, mu, tau.
proof idea
Direct constant definition that evaluates the charge formula once for $Q = -1$ and hard-codes the resulting integer 1332 for any input lepton.
why it matters
Supplies the common Z value consumed by gap_lepton and anomalous_e_tau_universal, which together establish that the RS correction is identical for electron and tau. It implements the φ-ladder step for QED moments inside the Recognition framework, consistent with the eight-tick octave and the universal J-cost structure. The definition closes the scaffolding needed for the universality claim while leaving the matching of higher-loop QED terms to PDG data as an open comparison.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.