pith. machine review for the scientific record. sign in
theorem proved tactic proof

proton_relative_error

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

 308theorem proton_relative_error :
 309    |proton_binding_pred - m_p_exp| / m_p_exp < 0.035 := by

proof body

Tactic-mode proof.

 310  have hb := proton_mass_bounds
 311  have hexp_pos : (0 : ℝ) < m_p_exp := by unfold m_p_exp; norm_num
 312  rw [div_lt_iff₀ hexp_pos, abs_lt]
 313  unfold m_p_exp
 314  constructor <;> nlinarith [hb.1, hb.2]
 315
 316/-! ## Verification Supersedes mass_ladder_assumption
 317
 318The concrete interval-arithmetic bounds above replace the placeholder
 319`mass_ladder_assumption` from `Assumptions.lean`. The following theorem
 320provides the direct replacement: the phi-ladder model with geometry-derived
 321parameters matches PDG masses without any external assumption. -/
 322
 323/-- Direct verification that the phi-ladder model matches PDG to stated tolerances.
 324    This supersedes `Masses.mass_ladder_assumption`. -/

depends on (8)

Lean names referenced from this declaration's body.