pith. sign in
module module high

IndisputableMonolith.Nuclear.NuclearForceStructure

show as:
view Lean formalization →

The NuclearForceStructure module establishes that effective nuclear-force coefficients derived from the phi-ladder are positive. Nuclear physicists extending binding-energy calculations to stability islands or neutron-star equations of state would cite these sign results. The module imports the BindingEnergy derivations and organizes ledger-based force terms into volume, surface, Coulomb, and asymmetry components whose positivity follows directly from the J-cost structure.

claimEffective nuclear-force coefficients satisfy $a_V > 0$, $a_S > 0$, $a_C > 0$, $a_A > 0$, where each term arises from the J-cost function $J(x) = (x + x^{-1})/2 - 1$ evaluated on the phi-ladder.

background

The upstream BindingEnergy module poses Q16: whether nuclear binding energies can be derived from the phi-ladder framework, noting that the seven magic numbers are already verified as eight-tick consequences. This module extends that foundation by isolating the structural sign properties of the force coefficients themselves. In the Recognition Science setting the J-cost and phi-ladder supply the underlying scale, while the nuclear force structure extracts the conventional semi-empirical terms and records that each carries a positive coefficient.

proof idea

This is a definition module, no proofs. It imports the BindingEnergy results, defines the ledger-derived force structure, and states the four positivity claims for the volume, surface, Coulomb, and asymmetry coefficients.

why it matters in Recognition Science

The module supplies the positivity constraints required by the IslandOfStabilityStructure and NeutronStarEOSStructure modules. It completes the structural sign requirements for the nuclear force terms in the Recognition Science derivation of binding energies, as outlined in the phi-ladder extension of Q16.

scope and limits

used by (2)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (6)