pith. machine review for the scientific record. sign in
def definition def or abbrev high

nuclear_force_from_ledger

show as:
view Lean formalization →

nuclear_force_from_ledger defines the proposition that the volume, surface, Coulomb, and asymmetry coefficients of the nuclear force are all positive. Nuclear physicists constructing models of binding energies or stability islands cite this as the ledger-derived structural condition. It is introduced as a direct definition consisting of a single conjunction of four inequalities.

claimThe ledger condition for nuclear force structure holds when the volume coefficient, surface coefficient, Coulomb coefficient, and asymmetry coefficient are each strictly positive.

background

In the NuclearForceStructure module this definition captures the positivity requirement on the coefficients of the semi-empirical nuclear mass formula. The module imports the coefficient definitions from the BindingEnergy module. This positivity serves as the structural premise for subsequent claims about nuclear stability and neutron-star equations of state.

proof idea

The declaration is a definition. It directly encodes the conjunction of the four strict positivity conditions on the nuclear force coefficients.

why it matters in Recognition Science

This definition supplies the nuclear force ledger condition required by has_nuclear_force_structure in the IslandOfStabilityStructure and NeutronStarEOSStructure modules. It also anchors the definitions of island_of_stability_from_ledger and neutron_star_eos_from_ledger. Within the Recognition Science framework it provides the nuclear-force input for models of nuclear binding and stability.

scope and limits

formal statement (Lean)

  11def nuclear_force_from_ledger : Prop :=

proof body

Definition body.

  12  volumeCoeff > 0 ∧ surfaceCoeff > 0 ∧ coulombCoeff > 0 ∧ asymmetryCoeff > 0
  13

used by (11)

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