nuclear_force_implies_volume_pos
The declaration extracts positivity of the volume coefficient from the nuclear force structure proposition. Nuclear modelers deriving binding energies from Recognition Science ledger principles cite it to fix the sign of the leading term in the semi-empirical mass formula. The proof is a one-line projection of the first conjunct in the defining conjunction.
claimIf $volumeCoeff > 0$, $surfaceCoeff > 0$, $coulombCoeff > 0$ and $asymmetryCoeff > 0$ all hold, then $volumeCoeff > 0$.
background
The module states that effective nuclear-force coefficients are positive. The upstream definition nuclear_force_from_ledger packages this as the conjunction volumeCoeff > 0 ∧ surfaceCoeff > 0 ∧ coulombCoeff > 0 ∧ asymmetryCoeff > 0. The present theorem belongs to a family of projections that isolate each conjunct for use in binding-energy calculations.
proof idea
The proof is a one-line wrapper that applies the first conjunct of the hypothesis nuclear_force_from_ledger.
why it matters in Recognition Science
The result supplies one of the four positivity statements required by the nuclear-force structure module. It therefore supports downstream derivations of binding energies that rely on signed coefficients. The module itself sits inside the Recognition Science program of obtaining nuclear parameters from ledger constraints rather than empirical fitting.
scope and limits
- Does not assign a numerical value to volumeCoeff.
- Does not derive the ledger or the conjunction itself.
- Does not address surface, Coulomb or asymmetry coefficients beyond their joint presence in the hypothesis.
formal statement (Lean)
19theorem nuclear_force_implies_volume_pos (h : nuclear_force_from_ledger) : volumeCoeff > 0 :=
proof body
Term-mode proof.
20 h.1
21
22/-- Nuclear-force structure implies positive surface coefficient. -/