Nuclear Nuclear

The nuclear cost template

Nuclear physics has a famous workhorse: the Bethe-Weizsäcker formula, which estimates the binding energy of an atomic nucleus from its number of protons and neutrons. It balances a volume term that grows with the nucleus, a surface term that shrinks it, a Coulomb repulsion between protons, and an asymmetry term that punishes imbalance. The formula is empirical, fitted to thousands of measured masses, and it works well enough to guide reactor design and astrophysics.

In Recognition Science, the framework's core object is the cost, a number that measures how far a ratio between two quantities is from unity. The framework proves that any cost function satisfying five plain conditions must equal J(x) = (x + 1/x)/2 - 1. The nuclear module defines its domainCost as J applied to the ratio m/e, where m and e are two real numbers standing for masses or energies. The module then proves three general facts about this cost: it vanishes when the two inputs are equal, it is never negative for positive inputs, and the constant phi - 3/2 is positive. These are true for any positive real inputs, because they follow from the universal properties of J itself.

The module does not prove anything specific to nuclear physics. Its own docstring says so plainly: the definition of domainCost never references protons, neutrons, or binding energies. The file is a template, shared verbatim with 2383 sibling modules, each one hoping to plug in a subject-specific definition of m and e. The Bethe-Weizsäcker formula appears only in a research note attached to the file, where the intended connection is sketched: the volume coefficient aV might equal a power of phi times a coherence energy. That note records where the idea was meant to go, not a result.

What the module does establish is a certificate: a machine-checked structure that bundles the three proved facts together. This certificate is inhabited, meaning the template is consistent and ready to use. The honest summary is that the framework has built the scaffold, and the physics remains open.

def domainCost (m e : ℝ) : ℝ := Jcost (m / e)

theorem domainCost_at_eq (r : ℝ) (h : r ≠ 0) : domainCost r r = 0 := by
  unfold domainCost; rw [div_self h]; exact Jcost_unit0

theorem domainCost_nonneg (m e : ℝ) (hm : 0 < m) (he : 0 < e) : 0 ≤ domainCost m e := by
  unfold domainCost; exact Jcost_nonneg (div_pos hm he)

theorem canonicalThreshold_pos : 0 < canonicalThreshold := by
  unfold canonicalThreshold; linarith [phi_gt_onePointFive]

def domainCost (m e : ℝ) : ℝ := Jcost (m / e)

def domainCost (m e : ℝ) : ℝ := Jcost (m / e)

What this page does not claim

No claim that the Bethe-Weizsäcker formula is derived from the framework. No claim that the module proves anything about actual nuclear masses or binding energies. No claim that the research note's numerical sketch (aV ~ 1.02 MeV) is a result.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Nuclear/Nuclear.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: