electron_residue
plain-language theorem explainer
The definition computes the electron residue as the base-phi logarithm of the ratio of observed electron mass to structural mass on the phi-ladder. Researchers testing the T9 mass formula against PDG data would cite this residue when verifying ledger closure for the lepton sector. The definition is a direct one-line expression that extracts the exponent offset from the structural prediction.
Claim. $Δ := log_φ(m_obs / m_struct)$, where $m_obs = 0.510998950$ MeV is the reference electron mass and $m_struct = Y · φ^{r_e - 8}$ is the structural mass with lepton yardstick $Y$ and baseline rung $r_e = 2$.
background
The module isolates core definitions for the T9 electron mass derivation to avoid import cycles. Structural mass is the product of the lepton yardstick and phi raised to the power of (electron rung minus the eight-tick octave period). The reference mass supplies the observed value solely for diagnostic extraction of the residue; it is not part of the forward prediction. The residue Δ therefore quantifies the logarithmic deviation of the measured mass from the pure geometric prediction forced by D = 3 cube geometry and the phi-ladder.
proof idea
This is a direct definition that applies Real.log to the ratio of mass_ref_MeV and electron_structural_mass, then divides by Real.log phi to obtain the base-phi exponent. No lemmas or tactics are invoked beyond the arithmetic operations on reals.
why it matters
The definition supplies the numerical input to the T9 electron mass ledger hypothesis and the residue bounds theorem. Those results test whether the extracted Δ lies within 0.002 of (gap 1332 minus refined shift). It therefore closes the diagnostic loop from the structural mass formula (itself derived from cube edges, wallpaper groups, and the eight-tick octave) to the observed electron mass, confirming consistency with the Recognition Science forcing chain at the lepton scale.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.