neutron_decay_allowed
plain-language theorem explainer
The free-neutron beta-decay Q-value is positive, establishing kinematic allowance for decay. Nuclear physicists using the Recognition Science framework cite this when deriving Q^5 phase-space factors for lifetime calculations. The proof is a one-line term-mode normalization that evaluates the constant definition 0.782 directly to a positive real.
Claim. The free-neutron beta-decay energy release satisfies $Q > 0$, where $Q = 0.782$ MeV.
background
Module P-015 formalizes the Recognition Science structural framework for neutron lifetime, noting that the experimental bottle-beam discrepancy remains unresolved. Neutron lifetime is fixed by weak-decay phase space with $Q^5$ scaling, matrix-element structure, and rung-determined mass inputs from the phi-ladder. The definition neutronDecayQ supplies the structural placeholder value 0.782 MeV. Upstream, the lifetime function is defined as lifetime k := phi^k.
proof idea
The proof is a term-mode one-liner that applies norm_num to the constant definition neutronDecayQ := 0.782, which evaluates immediately to a positive real number.
why it matters
This theorem supplies the positivity hypothesis required by neutron_decay_phase_space_positive (which shows the fifth-power phase-space factor is positive) and by neutron_lifetime_structure. It advances the RS derivation under P-015, where lifetime depends on Q^5 scaling together with phi-ladder inputs, though the full numerical derivation remains blocked.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.