Physics Nuclear Binding3 From Jcost

What the module actually proves

Nuclear binding energy is the energy that holds a nucleus together, usually quoted per nucleon, and it peaks at about 8.8 MeV for iron. A module in the Recognition Science library, named nuclear binding3 from jcost, was written with the ambition of deriving that binding curve from the framework's cost function, a measure of recognition effort. The file's own research note records attempts to match the iron peak using powers of the golden ratio, but the machine-checked content does not get there.

What the Lean code actually establishes is three general facts about the expression Jcost(m/e), where m and e are real numbers. First, when m equals e, the cost is zero. Second, for positive inputs, the cost is never negative. Third, the constant phi minus 3/2, called the canonical threshold, is positive. These are all true for any positive ratio, so they say nothing specific to nuclear physics. The definition of the cost is just Jcost(m/e), with no link to proton number, neutron number, or any measured binding energy.

The module assembles these three facts into a certificate structure, a formal package that records them as a unit. The certificate is inhabited, meaning the facts are consistent and provable. But the certificate would describe any subject that assigns a positive ratio to the cost function. What would make this a theorem about nuclear binding is a definition of m and e in nuclear terms, such as mass number and charge, and the file does not provide one.

In plain language: the module proves a small, true, and entirely generic lemma about the cost function. It does not prove the binding energy curve, does not derive the iron peak, and does not connect the golden ratio to measured nuclear data. The research note is a plan, not a result. The gap between the note's ambition and the code's content is the honest takeaway: the framework's library currently offers a template, and the physics would require a separate definitional step that has not been formalized.

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)

theorem cert_inhabited : Nonempty NucBind3Cert := ⟨cert⟩

What this page does not claim

The module does not derive the nuclear binding energy curve. The module does not prove the iron peak value of 8.8 MeV. The module does not establish any connection between the golden ratio and measured nuclear data.

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/Physics/Nuclear_Binding3_FromJCost.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: