nuclear_force_implies_coulomb_pos
plain-language theorem explainer
Nuclear force structure from the ledger implies a positive Coulomb coefficient. Nuclear physicists using the semi-empirical mass formula would cite this to guarantee the repulsive term carries the correct sign. The proof is a direct term extraction of the third conjunct from the four-way conjunction that defines the ledger.
Claim. If the ledger condition holds (volume, surface, Coulomb and asymmetry coefficients all positive), then the Coulomb coefficient is positive.
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 is one of four sibling extractions that isolate each conjunct.
proof idea
One-line term proof that selects the third conjunct (h.2.2.1) from the conjunction supplied by the ledger hypothesis.
why it matters
The declaration confirms positivity of the Coulomb term inside the nuclear-force ledger. It belongs to the set of results that establish all four coefficients are positive, supporting the structural claims of the NuclearForceStructure module. No downstream uses are recorded and no open questions are closed by this extraction.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.