ZOf_charged_leptons
plain-language theorem explainer
The ZOf invariant evaluates to 1332 for each of the three charged leptons. This equality is collected in the scorecard to confirm that equal-Z fermions occupy the same anchor rung. The proof is a one-line term that dispatches the conjunction by direct evaluation of the defining formula.
Claim. $Z_0(e) = 1332$, $Z_0(mu) = 1332$, and $Z_0(tau) = 1332$, where $Z_0$ is the integer map on fermions given by $q^2 + q^4$ for charged leptons and $q$ is the reduced charge of the fermion.
background
ZOf is the sector-dependent integer map on fermions: for charged leptons it reduces to the quadratic form $q^2 + q^4$ with $q$ the reduced charge. The QuarkScoreCard module consolidates existing proofs for the Phase 0 row of the physical derivation plan; it records theorem-grade facts about equal-Z particles without adding new physics. Upstream, the definition appears in RSBridge.Anchor and is cross-referenced by the anchor map Z in Masses.Anchor, which supplies the integer used in the anchor relation.
proof idea
The proof is a term-mode one-liner. It refines the three-way conjunction into separate subgoals and dispatches each by the decide tactic, which computes the concrete integer value of ZOf on the electron, muon, and tau directly from the definition.
why it matters
This supplies the lepton entry ZOf_lep in the QuarkScoreCardCert constructed by quarkScoreCardCert_holds. It confirms the module statement that e/μ/τ share ZOf = 1332, which is required for the pure φ-power mass ratios between equal-Z fermions. The result closes one theorem-grade item in the scorecard while the absolute mass match remains open pending the bridge equivalence theorem that would incorporate the gap(ZOf) correction.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.