nuclear_force_implies_surface_pos
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.
claimIf 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 in Recognition Science
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.
scope and limits
- Does not assign numerical values to any coefficient.
- Does not derive the ledger from more primitive Recognition Science axioms.
- Does not address corrections beyond the four-term decomposition.
- Does not connect to the phi-ladder or T0-T8 forcing chain.
formal statement (Lean)
23theorem nuclear_force_implies_surface_pos (h : nuclear_force_from_ledger) : surfaceCoeff > 0 :=
proof body
Term-mode proof.
24 h.2.1
25
26/-- Nuclear-force structure implies positive Coulomb coefficient. -/