lepton_Z_is_1332
plain-language theorem explainer
The electron rung index equals 1332 under the lepton-sector formula of the Recognition Science mass ladder. Researchers verifying the integer-rung model for leptons would cite this result to anchor the electron at the expected position on the phi-ladder. The proof reduces to a single native_decide tactic that evaluates the closed-form expression q² + q⁴ for the electron's charge quantum number.
Claim. $Z(e) = 1332$, where $Z$ is the integer rung index for the electron given by the lepton formula $q^2 + q^4$ and $q$ is the charge quantum number of the electron.
background
The module supplies audit certificates that bound the gap function for each fermion at the anchor scale. These bounds are intended to match the theoretical $F(Z)$ derived from the Recognition Composition Law. The $Z$ function computes the rung index for a fermion: for leptons it returns $q^2 + q^4$ where $q$ is the charge quantum number extracted from the fermion type. This theorem fixes the electron at rung 1332. Upstream, the $Z$ definition encodes the sector-specific formulas that place leptons on the integer-rung ladder rather than the quarter-ladder used for quarks.
proof idea
The proof is a one-line wrapper that invokes the native_decide tactic. This tactic evaluates the computable expression for $Z(e)$ by unfolding the lepton-sector formula and performing the arithmetic on the charge quantum number of the electron.
why it matters
This declaration supplies the numerical anchor for the lepton gap certificate in the audit payload. It confirms that the electron residue matches the theoretical gap $F(1332) ≈ 13.95$, supporting the integer-rung model for leptons as noted in the module documentation. The result feeds the verification of the display_identity_at_anchor axiom and quantifies the clustering of lepton residues around the same gap value.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.