`nuclear_binding_cert_exists`

proved

show as: view math explainer →

module: IndisputableMonolith.Nuclear.BindingEnergy
domain: Nuclear
line: 129 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Nuclear.BindingEnergy on GitHub at line 129.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

formal source

 126  coefficients_positive : 0 < rs_binding_coefficients.a_V ∧
 127    0 < rs_binding_coefficients.a_S ∧ 0 < rs_binding_coefficients.a_C
 128
 129theorem nuclear_binding_cert_exists : Nonempty NuclearBindingCert :=
 130  ⟨{ seven_magic := magic_numbers_count
 131     magic_sorted := magic_numbers_sorted
 132     eight_from_cube := magic_8_from_cube
 133     twenty_from_cube := magic_20_from_cube
 134     coefficients_positive := ⟨rs_binding_coefficients.h_V_pos,
 135       rs_binding_coefficients.h_S_pos, rs_binding_coefficients.h_C_pos⟩ }⟩
 136
 137end
 138
 139end IndisputableMonolith.Nuclear.BindingEnergy

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.