`volumeCoeff_in_range`

proved

show as: view math explainer →

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

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Nuclear.QCDToNuclearBridge on GitHub at line 92.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

formal source

  89/-! ## SEMF Coefficients -/
  90
  91/-- Volume coefficient is in the range [14, 17] MeV. -/
  92theorem volumeCoeff_in_range :
  93    (14 : ℝ) < volumeCoeff ∧ volumeCoeff < 17 := by
  94  unfold volumeCoeff; norm_num
  95
  96/-- Surface coefficient is larger than volume coefficient. -/
  97theorem surfaceCoeff_gt_volumeCoeff : volumeCoeff < surfaceCoeff := by
  98  unfold volumeCoeff surfaceCoeff; norm_num
  99
 100/-- Coulomb coefficient is small. -/
 101theorem coulombCoeff_small : coulombCoeff < volumeCoeff := by
 102  unfold coulombCoeff volumeCoeff; norm_num
 103
 104/-- The EM-derived Coulomb coefficient prediction. -/
 105def coulombCoeff_predicted : ℝ := (3/5) * (1/137.036) * (197.3 / 1.2)
 106
 107theorem coulombCoeff_consistent : |coulombCoeff - coulombCoeff_predicted| < 0.2 := by
 108  unfold coulombCoeff coulombCoeff_predicted; norm_num
 109
 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

papers checked against this theorem

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