pith. machine review for the scientific record. sign in
def

nuclearMagicCert

definition
show as:
view math explainer →
module
IndisputableMonolith.Physics.NuclearMagicNumbersFromRS
domain
Physics
line
44 · github
papers citing
none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Physics.NuclearMagicNumbersFromRS on GitHub at line 44.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

used by

formal source

  41  has_8 : 8 ∈ magicNumbers
  42  has_2 : 2 ∈ magicNumbers
  43
  44def nuclearMagicCert : NuclearMagicCert where
  45  seven_magic := magicNumbersCard
  46  eight_from_8tick := magic_8_eq_2cubed
  47  has_8 := magic_numbers_contain_8
  48  has_2 := magic_numbers_contain_2
  49
  50end IndisputableMonolith.Physics.NuclearMagicNumbersFromRS

papers checked against this theorem

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