`cornellPotential`

definition

show as: view math explainer →

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

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Nuclear.QCDToNuclearBridge on GitHub at line 81.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

used by

formal source

  78/-! ## Cornell Potential -/
  79
  80/-- Cornell potential structure: V = -α_s/r + σ·r. -/
  81def cornellPotential (r : ℝ) (_hr : r > 0) : ℝ :=
  82  -(alpha_strong / r) + stringTension * r
  83
  84/-- The Cornell potential at r₀ = 1.2 has the correct sign structure. -/
  85theorem cornell_at_r0_formula :
  86    cornellPotential r0_fm (by unfold r0_fm; norm_num) =
  87    -(alpha_strong / r0_fm) + stringTension * r0_fm := rfl
  88
  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

papers checked against this theorem

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