Nuclear Neutron Lifetime Structure

The neutron's ledger entry

The free neutron, left alone, does not last. Outside a nucleus it decays into a proton, an electron, and an antineutrino, with a mean lifetime near 881 seconds, roughly 15 minutes. The decay is allowed because the reaction releases energy: the Q value, the mass energy left over, is about 0.782 MeV. That positive release of energy is the first fact any theory of the neutron's lifetime must capture.

Two experimental methods measure the lifetime, and they disagree. The bottle method traps neutrons and counts how many remain after a known time; the beam method counts the protons produced by a decaying neutron beam. Bottle results cluster near 879 seconds, beam results near 888 seconds, a gap of about 9 seconds that has persisted for years. The discrepancy is unresolved, and it matters because the neutron's lifetime feeds into predictions of primordial helium abundance and other cosmological quantities.

In Recognition Science, the neutron's decay is treated as an entry in a ledger, a discrete record of recognition events. The framework models the lifetime as fixed by three structural inputs: the weak decay phase space, which scales as the fifth power of the Q value, the matrix-element structure of the interaction, and the rung-determined masses of the particles involved. The machine-checked library of formal theorems establishes only the skeleton of this structure. It proves that the Q value is positive, that the mean lifetime is positive, and that a positive Q value forces a positive fifth-power phase-space factor. It also defines a proposition, neutron_lifetime_from_ledger, that bundles these two positivities together, and proves that this bundled structure implies each of them separately.

The honest summary is that the library proves the signs, not the numbers. The Q value of 0.782 MeV and the mean lifetime of 881 seconds are entered as structural placeholders, not derived from first principles. The full numerical derivation of the lifetime remains blocked, and the experimental bottle-beam discrepancy remains unresolved. What the library does establish is a consistency condition: any complete RS account of the neutron's lifetime must keep the decay kinematically allowed and the lifetime positive, and it must respect the fifth-power phase-space scaling that follows from the positive Q value.

That consistency result is modest, but it is not empty. It gives the framework a fixed target: a future derivation of the lifetime must reproduce the measured value while preserving these positivity and scaling facts, and it must do so in a way that could eventually discriminate between the bottle and beam results. The library does not choose a side in the experimental dispute, but it does set the logical ground rules for any RS attempt to settle it.

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

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

/-- Mean lifetime is positive. -/
theorem neutron_lifetime_positive : freeNeutronMeanLife > 0 := by
  norm_num [freeNeutronMeanLife]

/-- 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 library does not derive the numerical value of the neutron lifetime from first principles. The library does not resolve the experimental bottle-beam discrepancy. The library does not prove that the ledger framework correctly models weak decay phase space beyond the positivity of the Q^5 factor.

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: