IndisputableMonolith.Nuclear.NuclearForceStructure

   1import Mathlib
   2import IndisputableMonolith.Nuclear.BindingEnergy
   3
   4namespace IndisputableMonolith
   5namespace Nuclear
   6namespace NuclearForceStructure
   7
   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
  38