module module

`IndisputableMonolith.Nuclear.BindingEnergy`

show as: view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

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