Nuclear Radioactive Halflife3 From Jcost

What the module proves

The Geiger-Nuttall rule is a classical empirical law of nuclear physics. It states that the logarithm of a radioactive isotope's half-life is a linear function of the atomic number divided by the square root of the decay energy: log(t_1/2) = a * Z / sqrt(Q) - b, where a and b are constants fitted to data. The rule works well for alpha decay across many isotopes, and it is one of the oldest quantitative patterns in nuclear physics, dating to 1911.

In Recognition Science, a ledger (a discrete record of events) is central, and the framework's cost function J(x) = (x + 1/x)/2 - 1 measures the forced price of recognition. The module named RadioactiveHalflife3FromJCost attempts to connect this cost to the Geiger-Nuttall intercept, but the actual Lean file proves something much narrower. It defines a function domainCost(m, e) = Jcost(m / e) and proves three general facts about it: the cost is zero when m equals e, the cost is nonnegative for positive inputs, and the constant phi - 3/2 is positive. These are properties of the cost function itself, not of any radioactive decay process.

The file's own docstring is explicit about this gap. It says the Lean code proves nothing specific to the subject, because domainCost is defined without reference to any physical quantity. The research note records where the idea was meant to go: a dimensional prediction for the Geiger-Nuttall intercept using b = J(phi)^(-1) * (a / sqrt(Q_max)) * Z = 8.47 * a * Z / sqrt(Q_max). But that is a note, not a theorem. The module is one of 2383 siblings that share the same body, universally quantified in a template file.

What the module does establish, in plain language, is that the cost function J has three properties that any reasonable cost should have: it vanishes when the two inputs are equal, it never goes negative, and a particular threshold constant is positive. These are true, machine-checked facts, but they are general facts about J, not facts about radioactivity. The connection to half-lives remains a research aspiration, not a proved result.

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)

What this page does not claim

This module proves no specific fact about radioactive half-lives or the Geiger-Nuttall rule. The dimensional prediction for the intercept is a research note, not a proved result. The cost function J is not shown to be connected to nuclear physics by this file.

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/RadioactiveHalflife3FromJCost.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: