`nuclear_force_implies_surface_pos`

proved

show as: view math explainer →

module: IndisputableMonolith.Nuclear.NuclearForceStructure
domain: Nuclear
line: 23 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Nuclear.NuclearForceStructure on GitHub at line 23.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

nuclear_force_from_ledger IndisputableMonolith.Nuclear.NuclearForceStructure

formal source

  20  h.1
  21
  22/-- Nuclear-force structure implies positive surface coefficient. -/
  23theorem nuclear_force_implies_surface_pos (h : nuclear_force_from_ledger) : surfaceCoeff > 0 :=
  24  h.2.1
  25
  26/-- Nuclear-force structure implies positive Coulomb coefficient. -/
  27theorem nuclear_force_implies_coulomb_pos (h : nuclear_force_from_ledger) : coulombCoeff > 0 :=
  28  h.2.2.1
  29
  30/-- Nuclear-force structure implies positive asymmetry coefficient. -/
  31theorem nuclear_force_implies_asymmetry_pos (h : nuclear_force_from_ledger) :
  32    asymmetryCoeff > 0 :=
  33  h.2.2.2
  34
  35end NuclearForceStructure
  36end Nuclear
  37end IndisputableMonolith

papers checked against this theorem

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