pith. machine review for the scientific record. sign in
def definition def or abbrev high

r0_fm

show as:
view Lean formalization →

The nuclear radius parameter r₀ is fixed at 1.2 fm to evaluate the Cornell potential in the bridge from QCD string tension to nuclear binding energies. Researchers modeling semi-empirical mass formulas cite this value when inserting the strong force parameters into the potential at nuclear scales. The definition consists of a direct numerical assignment with no additional computation or lemmas.

claimThe nuclear radius parameter is given by $r_0 = 1.2$ fm.

background

In the QCD-to-Nuclear Bridge module, this constant connects the strong coupling α_strong = 2/17 and string tension σ = φ^{-5} to the semi-empirical mass formula coefficients. The parameter r₀ appears in the Cornell potential V(r) = -α_s/r + σ r evaluated at the nuclear radius. Upstream results establish α_strong as the RS-derived strong coupling and confirm algebraic properties via the is theorems in foundational modules.

proof idea

This is a direct constant definition assigning the value 1.2 with no lemmas applied or tactics invoked.

why it matters in Recognition Science

The definition supplies the evaluation point for the theorem cornell_at_r0_formula, which confirms the correct sign structure of the Cornell potential. It advances the Recognition Science bridge from the phi-ladder and eight-tick octave to nuclear physics, supporting the derivation of SEMF coefficients from α_s and string tension. The module verifies all results with zero sorry.

scope and limits

formal statement (Lean)

  35def r0_fm : ℝ := 1.2

proof body

Definition body.

  36
  37/-- alpha_strong is positive. -/

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (5)

Lean names referenced from this declaration's body.