nuclear_force_implies_asymmetry_pos
plain-language theorem explainer
Nuclear force structure from the ledger requires the asymmetry coefficient to be positive. Modelers of nuclear binding energies cite this when enforcing positivity in the semi-empirical mass formula. The proof extracts the fourth conjunct directly from the defining proposition of the force ledger.
Claim. If the nuclear force ledger holds, i.e., the volume, surface, Coulomb and asymmetry coefficients are each positive, then the asymmetry coefficient is positive.
background
The module establishes structural content for effective nuclear-force coefficients. The upstream definition nuclear_force_from_ledger is the proposition that volumeCoeff, surfaceCoeff, coulombCoeff and asymmetryCoeff are all greater than zero. This local setting isolates positivity constraints that feed into binding-energy calculations.
proof idea
The proof is a one-line term wrapper that projects the fourth conjunct from the four-fold conjunction in the hypothesis nuclear_force_from_ledger.
why it matters
This theorem completes one of the four positivity requirements in the nuclear force structure. It supports derivations of binding energies by guaranteeing the asymmetry term is stabilizing. The result sits inside the Recognition framework's treatment of nuclear coefficients but does not yet link to the phi-ladder or the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.