has_nuclear_force_structure
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not derive explicit numerical values for the coefficients.
- Does not incorporate relativistic or pairing corrections.
- Does not address shell-structure effects beyond the four coefficients.
Lean usage
theorem neutron_star_eos_structure : neutron_star_eos_from_ledger := has_nuclear_force_structureformal statement (Lean)
10theorem has_nuclear_force_structure : nuclear_force_from_ledger := nuclear_force_structure
proof body
11