theorem proved term proof

`nuclear_force_structure`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

  14theorem nuclear_force_structure : nuclear_force_from_ledger := by

proof body

Term-mode proof.

  15  unfold nuclear_force_from_ledger volumeCoeff surfaceCoeff coulombCoeff asymmetryCoeff
  16  norm_num
  17
  18/-- Nuclear-force structure implies positive volume coefficient. -/

used by (2)

From the project-wide theorem graph. These declarations reference this one in their body.

has_nuclear_force_structure in IndisputableMonolith.Nuclear.IslandOfStabilityStructure decl_use
has_nuclear_force_structure in IndisputableMonolith.Nuclear.NeutronStarEOSStructure decl_use

depends on (2)

Lean names referenced from this declaration's body.

nuclear_force_from_ledger in IndisputableMonolith.Nuclear.NuclearForceStructure decl_use
volume in IndisputableMonolith.Papers.GCIC.BrainHolography decl_use