`nuclear_force_structure`

proved

show as: view math explainer →

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

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Nuclear.NuclearForceStructure on GitHub at line 14.

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

  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.