cornell_at_r0_formula
plain-language theorem explainer
The theorem verifies that the Cornell potential at the nuclear radius equals its defining Coulomb plus linear terms. Nuclear modelers connecting QCD to the semi-empirical mass formula cite this when checking the potential form at r0 = 1.2 fm. The proof proceeds by direct reflexivity after unfolding the radius definition and normalizing its positivity proof.
Claim. Let $V(r) = -a_s/r + s r$ denote the Cornell potential, where the strong coupling $a_s$ equals $2/17$ and the string tension $s$ equals $phi^{-5}$. Then at the nuclear radius $r_0 = 1.2$ fm, $V(r_0) = -a_s/r_0 + s r_0$.
background
This module bridges the QCD description of the strong force, with alpha_s = 2/17 from wallpaper groups and string tension sigma = phi^{-5}, to the nuclear semi-empirical mass formula coefficients. The Cornell potential is defined as V(r) = -alpha_s/r + sigma r for positive r. The local setting assumes all theorems are machine-verified with zero sorry or axiom, as stated in the module documentation. Upstream results supply the geometric definition of alpha_strong and ensure algebraic consistency in the foundational ledger.
proof idea
The proof is a one-line reflexivity after unfolding r0_fm and applying norm_num to discharge the positivity hypothesis in the potential definition.
why it matters
This equality confirms the sign structure of the Cornell potential at r0, supporting the QCD-to-nuclear bridge that derives SEMF coefficients from Recognition Science constants. It aligns with the phi-ladder mass formula and the alpha band constraints in the framework. The result closes a step in the module's verification that nuclear scales follow from the J-uniqueness and eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.