neutron_lifetime_structure
plain-language theorem explainer
The declaration establishes that the neutron lifetime ledger structure holds by confirming both a positive decay Q-value and a positive mean lifetime. Nuclear modelers working inside the Recognition Science framework cite this when assembling kinematic inputs for neutron decay calculations. The proof is a one-line term that directly pairs the two upstream positivity results into the required conjunction.
Claim. The neutron lifetime ledger structure holds: the free neutron decay Q-value satisfies $Q > 0$ and the mean lifetime satisfies $t > 0$.
background
Module P-015 formalizes the Recognition Science structural framework for neutron lifetime. The ledger is defined as the conjunction of positive decay Q-value and positive free neutron mean lifetime. Upstream results establish the kinematic allowance by direct numerical check on the Q-value and confirm lifetime positivity by the same method.
proof idea
The proof is a one-line term that constructs the pair from the kinematic allowance theorem and the lifetime positivity theorem to witness the conjunction required by the ledger definition.
why it matters
This supplies the structural input required by the neutron lifetime discrepancy analysis. It advances P-015 by confirming the basic positivity conditions that underpin Q^5 phase-space scaling in the Recognition Science derivation. The experimental bottle-beam discrepancy remains unresolved and blocks full numerical lifetime derivation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.