has_nuclear_force_structure
plain-language theorem explainer
The declaration asserts that nuclear force coefficients from the ledger are strictly positive. Nuclear physicists building equations of state for neutron stars cite this when connecting ledger constraints to binding-energy models. The proof is a one-line wrapper that invokes the nuclear_force_structure theorem.
Claim. The nuclear force coefficients satisfy $volumeCoeff > 0$, $surfaceCoeff > 0$, $coulombCoeff > 0$, and $asymmetryCoeff > 0$.
background
Recognition Science derives nuclear structures from ledger constraints on effective coefficients. The predicate nuclear_force_from_ledger is the conjunction requiring the volume, surface, Coulomb, and asymmetry coefficients to be positive. The upstream nuclear_force_structure theorem unfolds this definition and confirms the inequalities by norm_num.
proof idea
The proof is a one-line wrapper that directly applies the nuclear_force_structure theorem.
why it matters
This result supplies the nuclear-force positivity input required by island_of_stability_structure and neutron_star_eos_structure. It completes the ledger-to-structure step for nuclear forces in the Recognition framework, enabling downstream neutron-star EOS constructions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.