nuclear_force_implies_surface_pos
plain-language theorem explainer
The theorem extracts positivity of the surface coefficient from the nuclear force ledger assumption. Nuclear modelers working with binding energy decompositions would cite it to justify the sign of the surface term. The proof is a direct projection from the conjunction that defines the ledger.
Claim. If volumeCoeff > 0 ∧ surfaceCoeff > 0 ∧ coulombCoeff > 0 ∧ asymmetryCoeff > 0, then surfaceCoeff > 0.
background
The module NuclearForceStructure encodes structural positivity of effective nuclear-force coefficients. Its central definition nuclear_force_from_ledger is the proposition volumeCoeff > 0 ∧ surfaceCoeff > 0 ∧ coulombCoeff > 0 ∧ asymmetryCoeff > 0. This supplies the single hypothesis from which the four individual sign statements are extracted.
proof idea
The proof is a one-line term that projects the surface positivity conjunct from the ledger hypothesis h.
why it matters
The result belongs to the family of extraction theorems that unpack the nuclear_force_from_ledger definition. It directly supports the module claim that effective nuclear-force coefficients are positive. No downstream applications are recorded.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.