electron_residue
plain-language theorem explainer
The electron residue is the base-phi logarithm of the ratio between the observed electron mass 0.510998950 MeV and the structural mass on the phi-ladder. Researchers auditing T9 mass predictions against PDG data would cite this quantity to extract the fractional exponent deviation. The definition is a direct one-line change-of-base formula using Real.log on the mass ratio divided by log phi.
Claim. $Δ = log_φ(m_ref / m_struct)$ where $m_ref = 0.510998950$ and $m_struct = Y · φ^{r-8}$ with $Y$ the lepton yardstick and $r$ the electron rung.
background
This definition sits in the T9 Electron Mass Definitions module, which isolates core expressions to break import cycles in the Recognition Science framework. The structural mass is lepton_yardstick multiplied by phi raised to (electron_rung minus the octave period 8). The reference mass 0.510998950 MeV serves only as a diagnostic placeholder for the residue computation, not for forward prediction. Upstream, Mass is the type ℝ in RS-native units.
proof idea
The definition is a one-line wrapper that applies the change-of-base formula: it computes the natural log of the mass ratio and divides by the natural log of phi. No lemmas or tactics are invoked; the body is the direct arithmetic expression.
why it matters
This supplies the residue value fed into electron_mass_ledger_hypothesis, which checks that the residue lies within 0.002 of (gap 1332 minus refined_shift). It completes the T9 Electron Mass Formula step in the forcing chain, connecting the phi-ladder mass formula yardstick · φ^(rung - 8 + gap(Z)) to experimental comparison. The separation of definitions supports downstream bounds and necessity results while leaving open the question of proving 1e-6 agreement under tighter inputs.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.