cert_e
plain-language theorem explainer
This definition supplies the residue certificate for the electron with gap bounds 13.95 to 13.96. Researchers auditing lepton masses against the integer-rung model at Z=1332 in Recognition Science cite it to confirm alignment with the phi-ladder. The body is a direct structure literal that applies the ResidueCert constructor and uses norm_num on the bound inequality.
Claim. The residue certificate $C_e$ for the electron $e$ is the structure with fermion field $e$, lower bound $13.95$, upper bound $13.96$, and the inequality $13.95 ≤ 13.96$.
background
ResidueCert is the structure with fields f : Fermion, lo and hi : ℚ, and lo_le_hi : lo ≤ hi. This module supplies the audit payload of numerical bounds on gap(Z) for each fermion, obtained by transporting experimental masses to the anchor scale. The electron certificate targets the theoretical gap near 13.95, consistent with the assignment ZOf e = 1332 and the display_identity_at_anchor axiom from AnchorPolicy.
proof idea
The definition is a direct record construction that assigns the electron to the fermion field, sets the explicit rational bounds 1395/100 and 1396/100, and discharges the inequality with the norm_num tactic.
why it matters
This certificate populates the leptonCerts list, which demonstrates clustering of lepton residues around F(1332). It supports verification of the display_identity_at_anchor axiom and the mass formula on the phi-ladder in the Recognition framework, where the forcing chain yields the eight-tick octave and D = 3.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.