freeNeutronMeanLife
plain-language theorem explainer
The declaration supplies the experimental mean lifetime of the free neutron as 881 seconds for use as a reference scale in Recognition Science nuclear calculations. Researchers working on weak decay phase space and neutron lifetime discrepancies would reference this constant when connecting RS mass ladders to observed lifetimes. It enters as a direct numerical definition that anchors subsequent positivity and structure theorems.
Claim. The mean lifetime of the free neutron is defined by the constant value 881 seconds.
background
Module P-015 formalizes the RS structural framework for neutron lifetime, with the experimental bottle/beam discrepancy noted as unresolved. 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. Upstream results supply supporting predicates such as collision-free conditions and algebraic tautologies that underpin the ledger-based decay approach.
proof idea
The definition is introduced by direct assignment of the numerical value 881, serving as a one-line wrapper for the experimental reference scale.
why it matters
This constant feeds the neutron lifetime structure theorems, including neutron_lifetime_from_ledger which requires freeNeutronMeanLife > 0 alongside positive Q, and the positivity theorem neutron_lifetime_positive. It addresses the P-015 question on what determines neutron lifetime within the Recognition Science framework, where lifetime derives from Q^5 phase-space scaling and phi-ladder masses. The open question of the bottle/beam discrepancy remains, as full derivation is blocked.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.