has_nuclear_force_structure
The declaration asserts that the nuclear-force coefficients extracted from the ledger are all positive. Nuclear modelers constructing binding-energy surfaces or the island of stability cite this positivity when assembling the effective potential. The proof is a one-line wrapper that directly invokes the numerical verification already performed on the unfolded coefficients.
claimThe effective nuclear-force coefficients satisfy volumeCoeff $> 0$, surfaceCoeff $> 0$, coulombCoeff $> 0$, and asymmetryCoeff $> 0$.
background
In the Recognition Science ledger for nuclear structure the predicate nuclear_force_from_ledger is the conjunction of four strict inequalities on the volume, surface, Coulomb, and asymmetry coefficients. These coefficients appear as the leading terms in the semi-empirical mass formula once the ledger is specialized to finite nuclei. The positivity statement is first proved by unfolding the definitions and applying norm_num inside the NuclearForceStructure module.
proof idea
The proof is a one-line wrapper that applies the theorem nuclear_force_structure from the imported NuclearForceStructure module.
why it matters in Recognition Science
The result supplies the nuclear-force-side hypothesis required by island_of_stability_structure and by neutron_star_eos_structure. It therefore closes the ledger-to-structure step for both the island-of-stability construction and the neutron-star equation of state. The parent theorem nuclear_force_structure rests on the same coefficient unfolding and supplies the concrete numerical check that the present declaration re-exports.
scope and limits
- Does not compute explicit numerical values for any coefficient.
- Does not derive the coefficients from the Recognition forcing chain.
- Does not incorporate relativistic or many-body corrections.
- Does not address the transition to the liquid-drop limit.
Lean usage
theorem island_of_stability_structure : island_of_stability_from_ledger := has_nuclear_force_structureformal statement (Lean)
10theorem has_nuclear_force_structure : nuclear_force_from_ledger := nuclear_force_structure
proof body
11