`r_min`

definition

show as: view math explainer →

module: IndisputableMonolith.Nuclear.QCDToNuclearBridge
domain: Nuclear
line: 113 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Nuclear.QCDToNuclearBridge on GitHub at line 113.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

used by

formal source

 110/-! ## Saturation Properties -/
 111
 112/-- Nuclear saturation radius r_min = √(α_s/σ). -/
 113noncomputable def r_min : ℝ := Real.sqrt (alpha_strong / stringTension)
 114
 115/-- r_min is positive. -/
 116theorem r_min_pos : 0 < r_min :=
 117  Real.sqrt_pos_of_pos (div_pos alpha_strong_pos stringTension_pos)
 118
 119/-- α_s/σ is positive (both terms are positive). -/
 120theorem alpha_over_sigma_pos :
 121    0 < alpha_strong / stringTension := by
 122  exact div_pos alpha_strong_pos stringTension_pos
 123
 124/-- α_s/σ > 1 (strong coupling exceeds string tension). -/
 125theorem alpha_over_sigma_gt_one :
 126    1 < alpha_strong / stringTension := by
 127  have hα : alpha_strong = 2/17 := by unfold alpha_strong alpha_s_geom; norm_num
 128  have hσ := stringTension_bounds
 129  have hσ_pos := stringTension_pos
 130  -- 1 < (2/17) / σ: cross-multiply by σ to get σ < 2/17
 131  rw [hα]
 132  have hσ_ne : stringTension ≠ 0 := ne_of_gt hσ_pos
 133  have hgoal : stringTension < 2/17 := by nlinarith [hσ.2]
 134  calc 1 = stringTension / stringTension := (div_self hσ_ne).symm
 135    _ < (2/17) / stringTension := by
 136        apply div_lt_div_of_pos_right hgoal hσ_pos
 137
 138/-- Strong coupling is larger than EM coupling. -/
 139theorem strong_vs_em : (1/137 : ℝ) < alpha_strong := by
 140  unfold alpha_strong alpha_s_geom; norm_num
 141
 142end
 143

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.