volumeCoeff_in_range
The volume coefficient in the semi-empirical mass formula satisfies the strict inequality 14 < volumeCoeff < 17 in MeV units. Nuclear modelers calibrating the liquid-drop binding energy term would cite this bound when matching Recognition Science constants to observed nuclear masses. The proof is a one-line term wrapper that unfolds the volumeCoeff definition and applies norm_num to discharge the numerical comparison.
claim$14 < a_V < 17$ (MeV) where $a_V$ denotes the volume coefficient in the semi-empirical mass formula.
background
The declaration lives inside the QCD-to-Nuclear Bridge module, whose purpose is to carry the strong coupling α_s = 2/17 and string tension σ = φ^{-5} into the coefficients of the semi-empirical mass formula. VolumeCoeff is the explicit real number that multiplies the mass-number term A in the binding-energy expression. The module imports supply the upstream constants from Constants, StrongForce, and BindingEnergy; the listed depends_on edges supply auxiliary is predicates that certify the underlying algebraic and combinatorial constructions remain collision-free.
proof idea
The proof is a term-mode one-liner: unfold volumeCoeff followed by norm_num. No lemmas are invoked beyond the definitional unfolding; the numerical evaluator directly confirms the two-sided inequality on the concrete real value.
why it matters in Recognition Science
The result closes one link in the chain from Recognition Science forcing (T5 J-uniqueness, T6 phi fixed point, T7 eight-tick octave) through the strong-force parameters to the nuclear liquid-drop coefficients. It supplies a machine-verified anchor for the volume term that downstream binding-energy theorems can use without re-deriving the numerical range. No open scaffolding remains for this particular bound.
scope and limits
- Does not derive volumeCoeff from an explicit QCD Lagrangian.
- Does not incorporate shell corrections or deformation effects.
- Does not supply statistical uncertainties around the interval bounds.
- Does not address nuclei with A < 16 or A > 250.
formal statement (Lean)
92theorem volumeCoeff_in_range :
93 (14 : ℝ) < volumeCoeff ∧ volumeCoeff < 17 := by
proof body
Term-mode proof.
94 unfold volumeCoeff; norm_num
95
96/-- Surface coefficient is larger than volume coefficient. -/