nuclear_force_from_ledger
plain-language theorem explainer
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.
Claim. The 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.