volumeCoeff_in_range
plain-language theorem explainer
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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.