Nuclear Neutron Lifetime Structure Neutron Lifetime Implies Decay Allowed

The decay condition

A free neutron is not a stable particle. Left alone, it decays into a proton, an electron, and an antineutrino, with a mean lifetime of about 881 seconds, roughly fifteen minutes. The decay happens because the reaction is energetically favorable: the mass of the neutron is slightly larger than the combined mass of the decay products, so the process releases energy. In nuclear physics this energy release is measured by the Q value, the difference between the initial and final rest masses. For neutron beta decay, the Q value is about 0.782 MeV, a positive number, and that positivity is the kinematic condition that makes the decay allowed at all.

In the Recognition Science framework, this physical situation is encoded in a machine-checked library of formal theorems. The framework models the neutron's decay as a structural fact about a ledger, a discrete record of recognition events, and it defines a proposition called the ledger neutron-lifetime structure. That proposition bundles two conditions: the decay Q value is positive, and the mean lifetime is positive. The declaration neutron_lifetime_implies_decay_allowed is a theorem in this library, and it proves a deliberately narrow point: if the ledger neutron-lifetime structure holds, then the decay Q value is positive. In plain terms, the theorem says that within the framework's model, the existence of a positive neutron lifetime implies that the decay is kinematically allowed.

The proof is short because the claim is small. The ledger structure is defined as a conjunction of two facts, the positive Q value and the positive lifetime. The theorem simply extracts the first of those facts. It does not derive the Q value from first principles, it does not compute the lifetime, and it does not explain why the neutron decays. It records a logical implication inside the framework's formal system, nothing more.

What the declaration does not claim matters as much as what it proves. It does not claim that the framework has derived the numerical value of the neutron lifetime. The library's own status notes say the full derivation remains blocked, and the experimental bottle and beam measurements of the lifetime still disagree with each other. It does not claim that the Q value of 0.782 MeV is derived from the framework; that number is a structural placeholder, an input chosen for the model. And it does not claim that the positivity of the Q value alone explains the decay rate; the rate depends on the weak interaction's matrix element and on phase space, which the theorem does not touch.

The consequence of this theorem is modest but real. It gives the framework a formal anchor for a fact every nuclear physicist already knows: a neutron can decay because the reaction releases energy. The value of the declaration is not that it surprises anyone, but that it makes the kinematic condition explicit inside a machine-checked system, so that later, larger derivations can build on a verified foundation.

/-- The ledger neutron-lifetime structure implies positive decay Q-value. -/
theorem neutron_lifetime_implies_decay_allowed (h : neutron_lifetime_from_ledger) :
    neutronDecayQ > 0 :=
  h.1

/-- Structural placeholder for full RS lifetime formula. -/
def neutron_lifetime_from_ledger : Prop := neutronDecayQ > 0 ∧ freeNeutronMeanLife > 0

/-- Free-neutron mean lifetime in seconds (experimental reference scale). -/
def freeNeutronMeanLife : ℝ := 881

/-- Free-neutron beta-decay Q value in MeV (structural placeholder). -/
def neutronDecayQ : ℝ := 0.782

What this page does not claim

The framework derives the numerical value of the neutron lifetime. The Q value of 0.782 MeV is derived from the framework rather than chosen as an input. A positive Q value alone determines the decay rate, which also depends on the weak matrix element.

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