neutron_lifetime_implies_positive_lifetime
plain-language theorem explainer
The ledger hypothesis on neutron lifetime structure directly implies that the free neutron mean lifetime is positive. Nuclear modelers using RS-derived decay spectra would cite this result to confirm that the structural assumptions entail kinematic positivity before numerical evaluation. The proof consists of a single term projection selecting the second conjunct from the ledger definition.
Claim. If the neutron-lifetime ledger proposition holds, then the free-neutron mean lifetime is positive.
background
The neutron-lifetime ledger is defined as the conjunction of a positive decay Q-value and a positive free-neutron mean lifetime, with the latter set to the experimental reference scale of 881 seconds. This sits inside the module addressing P-015, which formalizes the RS structural framework for neutron lifetime via weak decay phase space and rung-determined mass inputs. Upstream results supply the eight-tick phase definition for periodicity in decay spectra and the phi-powered lifetime scaling from the DecaySpectrumFromPhiLadder module.
proof idea
The proof is the term h.2, which selects the second conjunct of the defining proposition for the neutron-lifetime ledger. It is a one-line wrapper that applies the ledger definition to extract the positivity assertion on the free-neutron mean lifetime.
why it matters
This theorem secures a basic consistency check inside the neutron-lifetime structure for P-015. It ensures the ledger hypothesis carries the positivity of the mean lifetime as a direct consequence, supporting broader RS work on Q^5 phase-space scaling and matrix-element structure. The parent framework landmarks include the phi-ladder mass inputs and eight-tick periodicity, though the full numerical lifetime derivation remains blocked due to unresolved experimental tensions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.