anchor_electron_Z
plain-language theorem explainer
The electron charge index evaluates to 1332 under the lepton-sector formula of ZOf. Researchers modeling lepton masses on the phi-ladder cite this fixed anchor when placing the electron rung. The proof is a one-line reflexivity that evaluates the definition of ZOf on the electron.
Claim. $Z(e) = 1332$, where $Z$ is the lepton charge index given by $q^2 + q^4$ evaluated at the integerized charge $q = -6$.
background
The Z-map assigns an integer charge index to each fermion. For leptons the index follows the even polynomial $Z = q^2 + q^4$ with $q = tildeQ(f)$, while quarks receive an extra offset of 4. The integerization step sets $tildeQ_e = 6 times (-1) = -6$, where the prefactor 6 equals the face count of the 3-cube and supplies one independent 2D symmetry channel per face. This construction is stated as a geometric structural input rather than a consequence of the T0-T8 forcing chain.
proof idea
The proof is a one-line reflexivity that directly evaluates the definition of ZOf on the electron fermion.
why it matters
This theorem supplies the concrete anchor value 1332 for the electron in the Z-map derivation. It supports the sibling results on Z_lepton_eq and Z_lepton_decomposition that decompose the lepton indices. Within the Recognition framework it fixes the starting rung for the electron mass formula yardstick times phi to the power (rung minus 8 plus gap(Z)), closing the charge-integerization step that precedes the phi-ladder mass assignments. The module notes that the face count k=6 is a geometric input rather than a consequence of the T0-T8 forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.