cert_e
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not derive the theoretical gap F(Z) from the Recognition Composition Law.
- Does not prove equality between the bounded interval and any experimental residue.
- Does not cover quark certificates or the charm anomaly.
- Does not compute physical masses from the yardstick and phi power.
formal statement (Lean)
62def cert_e : ResidueCert := {
proof body
Definition body.
63 f := e,
64 lo := 1395/100, -- 13.95
65 hi := 1396/100, -- 13.96
66 lo_le_hi := by norm_num
67}
68