island_of_stability_from_ledger
plain-language theorem explainer
The definition sets the island-of-stability proposition equal to the requirement that all four effective nuclear-force coefficients are positive. Nuclear modelers working inside the Recognition Science ledger would cite this when they need a single handle for stability islands that inherits the force positivity directly. The construction is a one-line alias with no additional lemmas or reductions.
Claim. The island-of-stability proposition holds precisely when the volume, surface, Coulomb, and asymmetry coefficients of the nuclear force are each positive: $V > 0$, $S > 0$, $C > 0$, $A > 0$.
background
The Nuclear.IslandOfStabilityStructure module builds directly on the imported NuclearForceStructure. There the upstream definition nuclear_force_from_ledger encodes the structural content of the effective nuclear force by requiring the four coefficients to be strictly positive. This positivity is the ledger-derived input that later theorems use to locate stable nuclear configurations.
proof idea
The declaration is a one-line definition that aliases the island-of-stability proposition to the nuclear_force_from_ledger proposition. No tactics or lemmas intervene.
why it matters
The definition supplies the hypothesis for island_of_stability_structure, which asserts the proposition via has_nuclear_force_structure, and for the implication theorem that recovers the force coefficients from the island structure. It therefore closes the link between the nuclear domain and the ledger forcing chain while preserving the positivity conditions required by the Recognition Science mass formula.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.