island_of_stability_implies_nuclear_force
plain-language theorem explainer
The theorem shows that the island-of-stability structure derived from the ledger directly supplies the condition that effective nuclear-force coefficients are positive. Nuclear modelers linking ledger constraints to binding-energy calculations would cite this when propagating positivity requirements into force terms. The proof is a one-line term that returns the hypothesis because the island structure is defined to coincide with the force positivity proposition.
Claim. If the island-of-stability structure holds from the ledger, then the nuclear-force coefficients satisfy $volumeCoeff > 0$, $surfaceCoeff > 0$, $coulombCoeff > 0$, and $asymmetryCoeff > 0$.
background
Within the Nuclear module the proposition nuclear_force_from_ledger asserts that the four effective coefficients in the nuclear force model are strictly positive. The island_of_stability_from_ledger is introduced as the identical proposition, so the two are definitionally the same. This placement follows the upstream nuclear_force_from_ledger definition that supplies the structural content for positive coefficients.
proof idea
The proof is a one-line term that returns the hypothesis h, which already carries nuclear_force_from_ledger because island_of_stability_from_ledger is defined to be exactly that proposition.
why it matters
The declaration supplies a direct bridge from the island-of-stability ledger entry to the nuclear-force positivity condition. It closes a consistency link inside the Nuclear submodule and supports any later derivation that requires the force coefficients to be positive. No downstream uses are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.