`nuclear_force_from_ledger`

definition

show as: view math explainer →

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

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Nuclear.NuclearForceStructure on GitHub at line 11.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

used by

formal source

   8open BindingEnergy
   9
  10/-- Structural content: effective nuclear-force coefficients are positive. -/
  11def nuclear_force_from_ledger : Prop :=
  12  volumeCoeff > 0 ∧ surfaceCoeff > 0 ∧ coulombCoeff > 0 ∧ asymmetryCoeff > 0
  13
  14theorem nuclear_force_structure : nuclear_force_from_ledger := by
  15  unfold nuclear_force_from_ledger volumeCoeff surfaceCoeff coulombCoeff asymmetryCoeff
  16  norm_num
  17
  18/-- Nuclear-force structure implies positive volume coefficient. -/
  19theorem nuclear_force_implies_volume_pos (h : nuclear_force_from_ledger) : volumeCoeff > 0 :=
  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.