pith. sign in
theorem

surfaceCoeff_gt_volumeCoeff

proved
show as:
module
IndisputableMonolith.Nuclear.QCDToNuclearBridge
domain
Nuclear
line
97 · github
papers citing
none yet

plain-language theorem explainer

The theorem establishes that the surface coefficient exceeds the volume coefficient in the semi-empirical mass formula derived from QCD parameters. Nuclear modelers calibrating binding energies against strong-force constants would cite this inequality when applying the liquid-drop terms. The proof proceeds by direct unfolding of the two coefficient definitions followed by numerical normalization.

Claim. In the semi-empirical mass formula the surface coefficient satisfies $a_s > a_v$, where both coefficients are obtained from the QCD string tension and strong coupling.

background

The module converts the Recognition-Science values α_s = 2/17 and string tension σ = φ^{-5} into the volume and surface coefficients of the semi-empirical mass formula. The local setting is the bridge from the strong-force description (wallpaper-group origin of α_s, phi-ladder origin of σ) to the liquid-drop terms used for nuclear binding energies. Upstream structural results supply the collision-free and edge-length hypotheses that underwrite the coefficient definitions, but the present proof does not invoke them explicitly.

proof idea

The proof is a one-line term-mode wrapper. It unfolds the definitions of volumeCoeff and surfaceCoeff, then applies norm_num to compare the resulting numeric expressions and confirm the strict inequality.

why it matters

The inequality guarantees that the surface term is the leading correction to the volume term, consistent with the phi-ladder mass formula and the eight-tick octave structure. It supplies a verified step in the QCD-to-nuclear bridge that feeds the overall derivation of binding energies from the Recognition-Science constants (c = 1, ħ = φ^{-5}, G = φ^5/π). No open scaffolding remains in this declaration.

Switch to Lean above to see the machine-checked source, dependencies, and usage graph.