neutron_lifetime_positive
plain-language theorem explainer
The free neutron mean lifetime is positive by direct evaluation of its constant definition. Nuclear theorists assembling the RS neutron lifetime ledger cite this when confirming kinematic allowance for decay. The proof is a one-line norm_num reduction that unfolds the definition 881 and checks the inequality.
Claim. Let $τ_n$ denote the free-neutron mean lifetime. Then $τ_n > 0$.
background
The module formalizes the RS structural framework for neutron lifetime under P-015. Neutron lifetime is fixed by weak decay phase space ($Q^5$ scaling), matrix-element structure, and rung-determined mass inputs, though full numerical derivation remains blocked. freeNeutronMeanLife is the constant 881 (seconds) serving as the experimental reference scale. The upstream result freeNeutronMeanLife states: Free-neutron decay is kinematically allowed ($Q > 0$).
proof idea
The proof is a term-mode one-line wrapper that applies norm_num to the definition freeNeutronMeanLife. This reduces the goal to the numerical fact 881 > 0.
why it matters
This theorem supplies one conjunct of neutron_lifetime_structure, which packages neutron_decay_allowed together with neutron_lifetime_positive to establish the ledger neutron-lifetime structure. It fills the positivity half of P-015. The module notes that the experimental bottle/beam discrepancy remains unresolved and that full derivation is blocked pending phase-space and mass-ladder inputs.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.