Z_electron
plain-language theorem explainer
Verification that ZOf applied to the electron fermion yields 1332 supports the anchor definitions in the mass ladder. Modelers checking consistency of Z-band assignments for leptons would cite it when aligning the phi-ladder positions. The proof reduces to a native computation of the ZOf expression on the electron constructor.
Claim. Let $Z$ be the integer label function on fermions defined by sector and tilde charge. Then $Z($electron$)=1332$.
background
The AnchorPolicy module supplies a precise Lean surface for single-anchor phenomenology in the mass framework. It wires to Constants.phi and RSBridge.Anchor while isolating assumptions about anchor scale and stability for downstream use in RG transport and flavor structure.
proof idea
The proof is a one-line wrapper that invokes native_decide to evaluate the ZOf definition on Fermion.e and confirm equality to 1332.
why it matters
This check ensures the electron's Z value matches the RSBridge definition, feeding into the mass formula yardstick * phi^(rung - 8 + gap(Z)) on the phi-ladder. It supports the single-anchor RG policy described in the module and contributes to T5 J-uniqueness and T6 phi fixed point through consistent Z assignments. No downstream uses are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.