coulombCoeff_small
plain-language theorem explainer
The theorem establishes that the Coulomb coefficient is strictly smaller than the volume coefficient in the semi-empirical mass formula. Nuclear physicists calibrating binding-energy models would cite this inequality to confirm the relative scale of electromagnetic repulsion versus strong-force binding. The verification is a direct term-mode reduction that unfolds the two coefficient definitions and applies numerical normalization.
Claim. In the semi-empirical mass formula the Coulomb coefficient satisfies $c < v$, where $c$ is the electromagnetic repulsion term and $v$ is the volume binding term.
background
The module bridges QCD parameters (strong coupling constant 2/17 and string tension equal to phi to the minus five) to the coefficients of the semi-empirical mass formula that describes nuclear binding energies. The volume coefficient encodes the dominant attractive contribution per nucleon from the strong interaction, while the Coulomb coefficient encodes the repulsive electromagnetic contribution between protons. No upstream lemmas are required; the result stands on the explicit definitions of the two coefficients supplied in the same module.
proof idea
The proof is a one-line term-mode wrapper. It unfolds the definitions of both coefficients and invokes norm_num to discharge the resulting numerical comparison.
why it matters
The inequality confirms that the electromagnetic correction remains small relative to the leading volume term, consistent with the overall QCD-to-SEMF bridge that derives nuclear coefficients from wallpaper-group values of alpha_s and the phi-ladder value of string tension. It supplies one of the concrete bounds needed to keep the semi-empirical mass formula coefficients inside their physically observed ranges.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.