electron_relative_error
Recognition Science mass prediction for the electron lies within 0.3 percent of the experimental value 0.51099895069 MeV. Researchers auditing discrete spacetime models cite this bound when validating the phi-ladder formula against PDG data. The tactic proof rewrites the prediction via the auxiliary equality, invokes the interval bounds on the predicted mass, and closes the relative error inequality with linear arithmetic.
claimThe relative error between the Recognition Science predicted electron mass in MeV and the experimental value satisfies $|m_{RS}(Lepton, 2) - m_{e,exp}| / m_{e,exp} < 0.003$, where $m_{RS}$ is computed from the phi-ladder expression $2^{B_{pow}} phi^{-5} phi^{r_0} phi^r / 10^6$.
background
In the Masses.Verification module experimental lepton masses are treated as imported constants while RS predictions are derived from the phi-ladder. The function rs_mass_MeV computes the predicted mass for a given sector and rung r as $2^{B_{pow} s} phi^{-5} phi^{r_0 s} phi^r / 10^6$ in MeV units. For the lepton sector the formula specializes to $m(Lepton, r) = phi^{57+r} / (2^{22} times 10^6)$. The experimental electron mass is defined as m_e_exp := 0.51099895069. The auxiliary theorem electron_pred_eq equates rs_mass_MeV .Lepton 2 to the explicit electron_pred expression, while electron_mass_bounds establishes the tight interval 0.5098 < electron_pred < 0.5102.
proof idea
The proof applies the rewrite rule from electron_pred_eq to replace the RS mass term with electron_pred. It then obtains the bounding interval via electron_mass_bounds and establishes positivity of m_e_exp by norm_num. The target inequality is rewritten using div_lt_iff and abs_lt, after which nlinarith closes both sides of the resulting conjunction using the supplied bounds.
why it matters in Recognition Science
This theorem supplies the electron percentage error for the mass verification certificate and is invoked directly by row_electron_pct and phi_ladder_verified. It confirms that the phi-ladder model reproduces the electron mass to the stated tolerance, supporting the broader claim that Recognition Science derives lepton masses from the J-uniqueness fixed point and the eight-tick octave. The result closes one verification step in the lepton sector without deriving the experimental constant itself.
scope and limits
- Does not derive the experimental mass from the Recognition Science functional equation.
- Does not extend the 0.3 percent tolerance to the muon or tau sectors.
- Does not incorporate experimental uncertainties beyond the PDG central value.
- Does not prove the formula for arbitrary sectors or rungs.
Lean usage
theorem row_electron_pct : |rs_mass_MeV .Lepton 2 - m_e_exp| / m_e_exp < 0.003 := electron_relative_errorformal statement (Lean)
110theorem electron_relative_error :
111 |rs_mass_MeV .Lepton 2 - m_e_exp| / m_e_exp < 0.003 := by
proof body
Tactic-mode proof.
112 rw [electron_pred_eq]
113 have hb := electron_mass_bounds
114 have hexp_pos : (0 : ℝ) < m_e_exp := by unfold m_e_exp; norm_num
115 rw [div_lt_iff₀ hexp_pos, abs_lt]
116 unfold m_e_exp
117 constructor <;> nlinarith [hb.1, hb.2]
118
119/-! ## Muon Mass Verification -/
120