Z_lepton
plain-language theorem explainer
The definition supplies the integer scale for leptons given their charge Q as (6Q) to the second plus (6Q) to the fourth power. Mass-ladder and anomalous-moment calculations cite it to fix the gap parameter on the phi-ladder. The implementation is a direct algebraic expression with no lemmas or tactics.
Claim. For integer charge $Q$, the lepton scale factor is $Z(Q) = (6Q)^2 + (6Q)^4$.
background
The module introduces binary scales and φ-exponential wrappers that feed the Recognition Science mass formula. Z enters the gap function that shifts the rung on the phi-ladder, where mass equals yardstick times phi to the power (rung minus 8 plus gap(Z)). Upstream stubs in Masses.Ribbons and the concrete value 1332 in AnomalousMoments both rely on this general expression for Q = -6.
proof idea
Direct definition. It evaluates the sum of the second and fourth powers of the scaled charge 6Q using ordinary integer arithmetic.
why it matters
It supplies the Z input to Z_of_charge and gap_lepton, which in turn drive anomalous_e_tau_universal and the universality claim for lepton corrections. The formula realizes the discrete Z values required by the eight-tick octave and the phi-ladder construction in the T5-T8 forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.