Lepton
plain-language theorem explainer
Recognition Science enumerates the charged leptons as a three-constructor inductive type whose cases are the electron, muon, and tau. Workers extending the φ-ladder residue mechanism to anomalous magnetic moments cite this enumeration to fix the common gauge charge Q = -1 and therefore the common Z = 1332 for the universal RS correction term. The definition is a direct inductive introduction of the three cases with no further structure or computation.
Claim. The charged leptons form the three-element set $L = {e, μ, τ}$, each carrying electric charge $Q = -1$ and therefore the same recognition number $Z = 1332$.
background
The module develops anomalous moments $a_l = (g-2)/2$ by adding an RS correction, derived from the φ-ladder, to the standard Schwinger term. All three charged leptons share the same gauge charge, so the correction is identical across $e$, $μ$, and $τ$. The upstream definition of $μ$ supplies the scalar coefficient in the quadratic projector relation $A^2 = μ A$. A sibling Lepton type in CubeFaceUniversality includes neutrinos, while the tau function from Masses.Anchor records generation torsion values 0, 11, 17.
proof idea
The declaration is a plain inductive definition that introduces the three constructors e, mu, tau directly; no lemmas or tactics are applied.
why it matters
The type supplies the common Z required for the universality statement anomalous_moment e = anomalous_moment τ. It is consumed by CubeFaceUniversalityCert (via HasCubeFaceCount Lepton), by the fermion-count theorems quark_lepton_sum and fermion_antifermion_total, and by the sector power B_pow in the mass anchor. The construction therefore closes the loop from the φ-ladder residue mechanism to the predicted equality of RS corrections for all charged leptons.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.