Nuclear Neutron Lifetime Structure Neutron Lifetime Implies Phase Space Positive

What the theorem proves

The neutron, a particle inside every atomic nucleus except hydrogen, is unstable when free. It decays into a proton, an electron, and an antineutrino. Whether this decay can happen at all depends on the Q-value: the energy released in the reaction. If the Q-value is positive, the decay is energetically possible; if it were negative, the neutron would be stable. The measured Q-value for free-neutron beta decay is about 0.782 MeV, a positive number.

In the Recognition Science framework, the neutron's lifetime is tied to the phase space of its decay products. Phase space counts how many ways the decay can arrange its particles' momenta. For beta decay, this phase-space factor scales as the fifth power of the Q-value, written Q^5. A positive Q-value therefore guarantees a positive phase-space factor: if the decay is allowed by energy, it has room to happen.

The declaration neutron_lifetime_implies_phase_space_positive is a theorem in the framework's machine-checked library of formal theorems. It proves: from the ledger structure of neutron lifetime, which asserts both a positive Q-value and a positive mean lifetime, it follows that Q^5 is positive. The proof is one line: it applies the general fact that a positive number raised to a positive power stays positive. This is not a physical measurement; it is a logical consequence of the structural assumptions.

What this theorem does not claim is just as important. It does not compute the neutron's lifetime. The full numerical derivation remains blocked, as the experimental bottle and beam methods still disagree by several seconds. The theorem does not say the Q^5 factor equals the measured lifetime, nor does it identify the matrix-element structure that also enters the decay rate. It establishes only a consistency condition: any valid RS model of neutron decay must have positive phase space, because the decay is energetically allowed.

This matters because it separates what is logically forced from what is empirically fitted. The positivity of Q^5 is a theorem; the value of the lifetime is a target. A reader can trust the first without waiting for the second.

/-- Neutron-lifetime structure implies positive `Q^5` phase-space scaling factor. -/
theorem neutron_lifetime_implies_phase_space_positive (h : neutron_lifetime_from_ledger) :
    neutronDecayQ ^ (5 : ℕ) > 0 :=
  pow_pos h.1 5

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

What this page does not claim

The theorem does not compute the numerical value of the neutron lifetime. The theorem does not state that Q^5 equals the measured lifetime. The theorem does not address the matrix-element structure of the decay.

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: