theorem
proved
old_value_differs
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Physics.ProtonRadius on GitHub at line 58.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
55theorem leptonic_universality : ∃ r : ℝ, r = proton_radius_codata := ⟨_, rfl⟩
56
57/-- The "large" old value differs by > 3% from CODATA. -/
58theorem old_value_differs : 0.877 - proton_radius_codata > 0.03 := by norm_num
59
60/-- RS form factor correction from standard dipole. -/
61noncomputable def form_factor_correction (Q L : ℝ) : ℝ :=
62 1 - 0.15 * (Q / L)^2
63
64theorem form_factor_near_one {Q L : ℝ} (hL : 0 < L) (h : (Q/L)^2 ≤ 0.01) :
65 |form_factor_correction Q L - 1| ≤ 0.0015 := by
66 unfold form_factor_correction
67 have hnn : 0 ≤ 0.15 * (Q / L)^2 := by positivity
68 rw [show 1 - 0.15 * (Q / L)^2 - 1 = -(0.15 * (Q / L)^2) from by ring]
69 rw [abs_neg, abs_of_nonneg hnn]
70 nlinarith
71
72end ProtonRadius
73end Physics
74end IndisputableMonolith