Z_electron
The theorem asserts that ZOf applied to the electron fermion constructor equals 1332. Physicists anchoring fermion masses to the Recognition Science phi-ladder would cite this to fix the electron rung. The proof is a one-line native_decide tactic that directly evaluates the ZOf definition on the lepton sector case.
claim$ZOf(e) = 1332$ where $e$ is the electron constructor in the Fermion inductive type and $ZOf$ returns the integer label $q^2 + q^4$ for leptons with $q = tildeQ(f)$.
background
The Fermion type is an inductive enumeration of standard-model fermions with constructors including e for the electron. ZOf is the function that computes the integer Z label: for leptons it returns qq + qqqq where q = tildeQ(f), while up/down sectors add an offset of 4. The module provides a Lean surface for single-anchor RG policy, wiring Constants.phi to RSBridge.Anchor infrastructure and representing the integrated RG residue f_i(μ⋆) as the hypothesis that equals gap(ZOf i).
proof idea
The proof is a one-line wrapper that applies the native_decide tactic to evaluate the equality by direct computation of the ZOf definition on Fermion.e.
why it matters in Recognition Science
This declaration verifies that the electron Z value matches the RSBridge.ZOf definition, supporting the single-anchor phenomenology used in the mass framework. It supplies a concrete anchor point for the phi-ladder mass formula yardstick * phi^(rung - 8 + gap(Z)) and isolates the RG transport hypothesis f_i(μ⋆) = F(Z_i) for downstream modules. No parent theorems are listed in the used_by edges, leaving the link to explicit mass predictions as an open connection.
scope and limits
- Does not derive the Z assignment from the forcing chain or RCL.
- Does not implement or verify the RG integral for anomalous dimensions.
- Does not address radiative stability or flavor structure beyond the numerical check.
- Does not connect to the eight-tick octave or D=3 spatial dimensions.
formal statement (Lean)
106theorem Z_electron : ZOf Fermion.e = 1332 := by native_decide