nuclear_force_structure
plain-language theorem explainer
The declaration proves that the four effective nuclear force coefficients (volume, surface, Coulomb, asymmetry) are each strictly positive. Nuclear modelers working inside the Recognition Science framework would cite it when establishing binding-energy signs or stability conditions. The proof is a one-line wrapper that unfolds the defining conjunction and normalizes the coefficient constants.
Claim. $volumeCoeff > 0 ∧ surfaceCoeff > 0 ∧ coulombCoeff > 0 ∧ asymmetryCoeff > 0$
background
The NuclearForceStructure module supplies the structural claim that effective nuclear-force coefficients are positive. Its central definition nuclear_force_from_ledger is exactly the conjunction of those four strict inequalities. The volume function imported from BrainHolography is the cardinality of a finite vertex set and appears among the unfolded identifiers, though the positivity statement itself is a direct numerical fact.
proof idea
The proof unfolds nuclear_force_from_ledger together with the four coefficient definitions, then applies norm_num to discharge the resulting numerical inequalities.
why it matters
The theorem supplies the nuclear_force_from_ledger fact to has_nuclear_force_structure in both IslandOfStabilityStructure and NeutronStarEOSStructure. It realizes the module doc-comment that effective nuclear-force coefficients are positive, thereby anchoring the nuclear sector of the Recognition Science mass ladder and forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.