Physics Beta Decay3 From Jcost

The cost of a decay

In physics, beta decay is the process by which an unstable atomic nucleus changes a neutron into a proton (or the reverse), emitting an electron and an antineutrino. The energy released in such a decay is shared between the daughter nucleus, the electron, and the neutrino. A central question is whether a given decay is energetically possible: the mass of the parent nucleus must exceed the sum of the masses of the products, otherwise the decay cannot proceed.

Within Recognition Science, the framework models this energy balance using its fundamental cost function. The module Beta_Decay3_FromJCost defines a domain cost, a discrete record of the price of a mismatch between two masses, as J(m/e), where J is the framework's unique cost function and m and e are the masses of the parent and the emitted electron. The framework proves three plain facts about this cost. First, when the two masses are equal, the cost is exactly zero. Second, for any positive masses, the cost is never negative. Third, a canonical threshold value, defined as the golden ratio minus 1.5, is always positive.

The module packages these three facts into a certificate structure, a formal object that bundles the proofs together. The certificate is inhabited, meaning the framework can construct an instance of it. In plain language, this establishes that the cost of a beta decay, as defined by the framework, is a well-behaved quantity: it is zero when the masses balance, and it never goes below zero, so it cannot indicate an impossible negative energy release.

This is a small but foundational result. It does not predict any specific decay rate or half-life. Instead, it provides a formal guarantee that the framework's cost function, when applied to beta decay, satisfies the basic sanity conditions one would demand of any energy-like quantity. The golden ratio enters through the threshold, but the module does not claim this threshold corresponds to any measured physical boundary.

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]

What this page does not claim

This module does not predict any specific beta decay rate or half-life. The canonical threshold is not claimed to correspond to any measured physical boundary.

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/Beta_Decay3_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: