module module high

`IndisputableMonolith.Nuclear.BindingEnergy`

Module Nuclear.BindingEnergy supplies definitions of nuclear magic numbers (2, 8, 20, 28) and binding coefficients for the semi-empirical mass formula. It is imported by NuclearForceStructure and QCDToNuclearBridge. The module contains only definitions with no theorems or proofs.

claimDefines $magic_2 = 2$, $magic_8 = 8$, $magic_{20} = 20$, $magic_{28} = 28$ together with $BindingCoefficients$ as the set of volume, surface, Coulomb, asymmetry and pairing terms in RS-native units.

background

The module resides in the Nuclear domain and imports Constants, whose sole documented object is the RS time quantum $\tau_0 = 1$ tick. Sibling declarations introduce the four classic magic numbers via dimension and cube constructions, plus the composite object BindingCoefficients. These objects supply the numerical inputs required by the semi-empirical mass formula.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

Supplies the magic numbers and BindingCoefficients consumed by NuclearForceStructure (positive effective nuclear-force coefficients) and by QCDToNuclearBridge (bridge from $\alpha_s = 2/17$ and string tension $\sigma = \phi^{-5}$ to SEMF coefficients). The downstream bridge states that all its theorems are machine-verified with zero sorry.

scope and limits

Does not derive binding coefficients from the T0-T8 forcing chain.
Does not evaluate binding energies for concrete nuclei.
Does not import or reference the Recognition Composition Law.
Does not address the alpha band or phi-ladder mass formula.

used by (2)

From the project-wide theorem graph. These declarations reference this one in their body.

IndisputableMonolith.Nuclear.NuclearForceStructure module_import
IndisputableMonolith.Nuclear.QCDToNuclearBridge module_import

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import

declarations in this module (18)

def magic_numbers L44
theorem magic_numbers_count L46
theorem magic_numbers_sorted L48
theorem two_is_magic L50
theorem eight_is_magic L51
theorem twenty_is_magic L52
theorem twentyeight_is_magic L53
theorem magic_2_from_dimension L63
theorem magic_8_from_cube L64
theorem magic_20_from_cube L65
theorem magic_28_from_cube L66
structure BindingCoefficients L73
def rs_binding_coefficients L85
def binding_energy L97
def binding_per_nucleon L103
theorem volume_dominates_surface L112
structure NuclearBindingCert L121
theorem nuclear_binding_cert_exists L129