Nuclear Neutron Lifetime Structure Neutron Lifetime Implies Positive Lifetime

What the declaration proves

The neutron, a particle inside every atomic nucleus except ordinary hydrogen, does not live forever when free. Left alone, it decays into a proton, an electron, and an antineutrino, with a mean lifetime of about 881 seconds, roughly 15 minutes. The declaration neutron_lifetime_implies_positive_lifetime is a formal statement in the Recognition Science framework's machine-checked library of formal theorems. It proves a modest but exact fact: if the structural conditions for neutron decay hold, then the mean lifetime is greater than zero. That is, the framework's model of the neutron cannot describe a particle that decays and also has a zero or negative lifetime.

The proof is deliberately small. The framework defines a ledger, a discrete record of events, in which the neutron's decay is represented by two quantities: a decay energy Q of 0.782 MeV and a mean lifetime of 881 seconds. A first theorem establishes that Q is positive, meaning the decay is kinematically allowed, the final state has less mass than the initial neutron. A second theorem, the one in question, takes that structure and extracts the positivity of the lifetime. The entire argument is a projection: from the conjunction of two positive facts, it selects the second one. It does not derive the lifetime from first principles; it only confirms that the lifetime, as defined, is a positive real number.

The declaration sits inside a larger effort. The framework's broader goal is to derive the neutron's lifetime from its structural inputs, using a phase-space factor that scales as the fifth power of the decay energy, Q^5, along with matrix-element structure and mass inputs. That full numerical derivation is not complete. The present theorem is a consistency check, a guarantee that the model's basic ingredients are not internally contradictory. It is the kind of small, rigorous step that a proof assistant can verify completely, even when the surrounding physics remains open.

What the declaration does not claim is just as important. It does not say that the neutron's lifetime is 881 seconds as a matter of proof; that value is an experimental reference, not a derived result. It does not resolve the known discrepancy between bottle and beam experiments, which measure slightly different lifetimes. And it does not establish that the framework's structural model is correct. It only says that within that model, a positive lifetime follows from the assumption that decay is possible. The theorem is a floor, not a ceiling: a small certainty on which a larger, unfinished derivation may eventually stand.

/-- The ledger neutron-lifetime structure implies positive mean lifetime. -/
theorem neutron_lifetime_implies_positive_lifetime (h : neutron_lifetime_from_ledger) :
    freeNeutronMeanLife > 0 :=
  h.2

/-- Free-neutron decay is kinematically allowed (`Q > 0`). -/
theorem neutron_decay_allowed : neutronDecayQ > 0 := by
  norm_num [neutronDecayQ]

/-- Positive decay Q-value forces positive fifth-power phase-space factor (`Q^5`). -/
theorem neutron_decay_phase_space_positive : neutronDecayQ ^ (5 : ℕ) > 0 := by
  exact pow_pos neutron_decay_allowed 5

What this page does not claim

The declaration does not prove that the neutron's lifetime is 881 seconds; that value is an experimental input. The declaration does not resolve the bottle versus beam discrepancy in neutron lifetime measurements. The declaration does not establish that the framework's structural model of the neutron is physically correct.

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: