neutron_decay_phase_space_positive
plain-language theorem explainer
The theorem establishes that the fifth power of the neutron beta-decay Q-value is strictly positive. Nuclear modelers working on beta-decay kinematics within the Recognition Science framework would cite it when confirming that phase-space factors remain positive for allowed decays. The proof is a one-line application of the general positivity lemma for natural-number powers applied to the kinematic allowance theorem.
Claim. Let $Q$ be the free-neutron beta-decay energy release. Then $Q^5 > 0$.
background
The module P-015 formalizes the Recognition Science structural framework for neutron lifetime, noting that the derivation is STARTED with the experimental bottle/beam discrepancy unresolved. Neutron lifetime is fixed by weak decay phase space with $Q^5$ scaling, matrix-element structure, and rung-determined mass inputs; full numerical derivation remains BLOCKED. The definition neutronDecayQ supplies the structural placeholder value 0.782 MeV for the free-neutron beta-decay Q-value. The upstream theorem neutron_decay_allowed states that free-neutron decay is kinematically allowed because $Q > 0$. The imported lifetime definition from the phi-ladder supplies the general form lifetime(k) = phi^k.
proof idea
The proof is a one-line wrapper that applies the lemma pow_pos to the theorem neutron_decay_allowed at exponent 5.
why it matters
This result supplies the positivity step required for phase-space factors in the P-015 neutron-lifetime registry item. It supports the claim that neutron lifetime is fixed by weak decay phase space ($Q^5$ scaling) inside the RS framework. The module records that full numerical lifetime derivation remains BLOCKED pending resolution of the experimental discrepancy; the declaration closes one structural prerequisite without addressing that open question.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.