neutron_lifetime_implies_phase_space_positive
plain-language theorem explainer
The neutron lifetime ledger assumption forces the beta-decay Q-value to satisfy Q^5 > 0, ensuring positive phase-space volume for weak decay. Nuclear physicists modeling neutron lifetime in structural frameworks would cite this to confirm sign consistency of the scaling factor. The proof is a one-line term application of the positivity lemma for real powers to the first conjunct of the ledger hypothesis.
Claim. Let $Q$ be the free-neutron beta-decay energy release. If $Q > 0$ and the free neutron mean lifetime is positive, then $Q^5 > 0$.
background
The module P-015 formalizes the Recognition Science structural framework for neutron lifetime, which is fixed by weak decay phase space scaling as $Q^5$, matrix-element structure, and rung-determined mass inputs. The definition neutronDecayQ supplies the structural placeholder $Q = 0.782$ MeV for the free-neutron beta-decay energy release. The hypothesis neutron_lifetime_from_ledger is the Prop encoding the conjunction $Q > 0$ and freeNeutronMeanLife > 0, serving as the interface assumption linking lifetime to ledger inputs.
proof idea
This is a term-mode proof consisting of a single application of the lemma pow_pos, which states that a positive real number raised to any natural power remains positive. It is applied directly to the first projection of the hypothesis h, which supplies neutronDecayQ > 0, with exponent 5.
why it matters
This theorem establishes the positivity of the phase-space scaling factor under the ledger assumption, forming a basic consistency check within the neutron lifetime structure for P-015. It supports the broader derivation where lifetime is fixed by $Q^5$ scaling and aligns with Recognition Science emphasis on phase space positivity in decay processes. The full numerical lifetime derivation remains blocked as noted in the module documentation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.