volume_dominates_surface
plain-language theorem explainer
The result shows that for nuclear mass number A at least 8 the volume term exceeds the surface term in the binding-energy expression once the coefficients satisfy the positivity conditions of the structure. Nuclear-structure theorists using the semi-empirical mass formula would cite it to justify neglecting surface corrections for medium and heavy nuclei. The proof is a short tactic block that records positivity of A and feeds the coefficient signs together with the elementary inequality A^{2/3} ≤ A into a nonlinear-arithmetic solver.
Claim. Let $a_V>0$ and $a_S>0$ be the volume and surface coefficients. Then for every natural number $A$ with $A≥8$, $a_V A > a_S A^{2/3}$.
background
BindingCoefficients is the structure that packages the five conventional coefficients of the semi-empirical mass formula together with their positivity hypotheses; only the volume coefficient $a_V$ and surface coefficient $a_S$ appear in the present statement. The module derives nuclear binding from the J-cost functional on the φ-lattice, where the volume term arises from saturation of J-cost inside a filled shell and the surface term from the boundary cost on the same lattice. Upstream results supply the active-edge count A (equal to 1) and the 8-tick periodicity that already fixes the magic numbers 2, 8, 20, 28.
proof idea
The tactic first obtains strict positivity of the real number A by casting the natural-number hypothesis. It then invokes nlinarith on the four facts coeff.h_V_pos, coeff.h_S_pos, the positivity of A, and the auxiliary inequality (A:ℝ)^{2/3} ≤ A that holds for A ≥ 8 by the real-power monotonicity lemma.
why it matters
The declaration supplies the first concrete inequality needed to justify the volume-dominated regime inside the nuclear-binding module. It therefore supports the larger program of expressing binding energies via the four terms listed in the module header (volume, surface, Coulomb, asymmetry) while the 8-tick shell structure already accounts for the magic numbers. No downstream theorem yet consumes the result, leaving open the question of whether the same coefficients can be derived rather than postulated from the φ-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.