phi_pos

formal source

  14
  15noncomputable def φ : ℝ := (1 + Real.sqrt 5) / 2
  16
  17theorem phi_pos : 0 < φ := by unfold φ; positivity
  18
  19theorem phi_gt_one : 1 < φ := by
  20  unfold φ
  21  have h5 : (1:ℝ) < Real.sqrt 5 := by
  22    have : Real.sqrt 1 < Real.sqrt 5 := Real.sqrt_lt_sqrt (by norm_num) (by norm_num)
  23    simpa [Real.sqrt_one] using this
  24  linarith
  25
  26/-- m_μ/m_e = φ^11 (rungs: r_e = 2, r_μ = 13, difference = 11). -/
  27noncomputable def muon_electron_ratio : ℝ := φ ^ 11
  28
  29theorem muon_heavier : 1 < muon_electron_ratio := by
  30  unfold muon_electron_ratio
  31  exact one_lt_pow₀ phi_gt_one (by norm_num)
  32
  33theorem muon_ratio_pos : 0 < muon_electron_ratio :=
  34  lt_trans one_pos muon_heavier
  35
  36/-- Muonic Bohr radius is smaller → probes shorter distances. -/
  37theorem muonic_smaller : 1 / muon_electron_ratio < 1 := by
  38  rw [div_lt_one muon_ratio_pos]; exact muon_heavier
  39
  40/-- RS proton radius estimate from confinement + form factor. -/
  41noncomputable def proton_radius_estimate (h_over_mpc α_s : ℝ) : ℝ :=
  42  (1/4) * h_over_mpc * Real.sqrt (6 * Real.pi / α_s)
  43
  44theorem proton_radius_positive {h_over_mpc α_s : ℝ}
  45    (hh : 0 < h_over_mpc) (hα : 0 < α_s) :
  46    0 < proton_radius_estimate h_over_mpc α_s := by
  47  unfold proton_radius_estimate