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