neutron_lifetime_from_ledger
plain-language theorem explainer
The declaration packages the positivity of the neutron beta-decay Q-value together with the positivity of the free-neutron mean lifetime into a single proposition. Nuclear physicists working on the bottle-beam lifetime discrepancy would cite it as the minimal ledger input that makes decay kinematically allowed. It is introduced as a bare definition that simply conjoins the two reference inequalities supplied by its sibling constants.
Claim. Let $Q$ be the free-neutron beta-decay energy release and let $T$ be the free-neutron mean lifetime. The ledger condition is the proposition $Q > 0$ and $T > 0$.
background
In the Recognition Science treatment of nuclear structure the neutron lifetime is fixed by the phase-space volume of the weak decay, which scales as $Q^5$, together with matrix elements determined by rung assignments on the phi-ladder. Module P-015 records that a full first-principles derivation remains blocked while the experimental bottle-beam discrepancy is unresolved; the present definition supplies the minimal structural placeholder that keeps decay allowed and the lifetime finite.
proof idea
This is a definition whose body is the conjunction of the two positivity statements taken directly from the sibling constants neutronDecayQ and freeNeutronMeanLife. No lemmas or tactics are invoked; the declaration simply assembles the pair into a single Prop.
why it matters
The definition is the root proposition required by has_neutron_lifetime_input, by neutron_discrepancy_implies_lifetime_input, and by the three implication theorems that extract $Q > 0$, $T > 0$, and $Q^5 > 0$. It therefore anchors the P-015 registry item, which ultimately aims to replace the numerical ledger entries with mass inputs derived from the forcing chain and the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.