nuclear_force_structure
The theorem proves that the effective nuclear-force coefficients are all positive according to the ledger definition. Nuclear physicists modeling binding energies or neutron-star equations of state would cite this result when confirming structural positivity of the force terms. The proof is a one-line term wrapper that unfolds the target proposition and the four coefficient definitions then applies norm_num.
claimThe nuclear-force coefficients satisfy $volumeCoeff > 0$, $surfaceCoeff > 0$, $coulombCoeff > 0$, and $asymmetryCoeff > 0$.
background
The module Nuclear.NuclearForceStructure supplies structural facts about effective nuclear forces. Its central definition nuclear_force_from_ledger is the proposition that the four coefficients (volume, surface, Coulomb, asymmetry) are each strictly positive. The proof also references the volume definition imported from BrainHolography, which simply returns the cardinality of a Finset of vertices.
proof idea
The term proof unfolds nuclear_force_from_ledger together with the four coefficient definitions volumeCoeff, surfaceCoeff, coulombCoeff, and asymmetryCoeff, then applies norm_num to verify the resulting numerical inequalities.
why it matters in Recognition Science
The result is used verbatim by the has_nuclear_force_structure theorems in IslandOfStabilityStructure and NeutronStarEOSStructure. It supplies the required positivity of nuclear-force coefficients inside the Recognition framework's treatment of binding energies. No open questions or scaffolding remain.
scope and limits
- Does not derive explicit numerical values for any coefficient.
- Does not connect the coefficients to the underlying ledger construction.
- Does not address stability or binding-energy magnitudes.
Lean usage
theorem has_nuclear_force_structure : nuclear_force_from_ledger := nuclear_force_structureformal statement (Lean)
14theorem nuclear_force_structure : nuclear_force_from_ledger := by
proof body
Term-mode proof.
15 unfold nuclear_force_from_ledger volumeCoeff surfaceCoeff coulombCoeff asymmetryCoeff
16 norm_num
17
18/-- Nuclear-force structure implies positive volume coefficient. -/