nuclear_force_implies_volume_pos
plain-language theorem explainer
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.
Claim. If $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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.