has_neutron_lifetime_input
plain-language theorem explainer
The declaration establishes that the neutron lifetime ledger holds, with positive decay Q-value and positive free neutron mean lifetime. Experimental physicists analyzing the neutron lifetime anomaly under Recognition Science would cite it to anchor measured inputs to the RS ledger. The proof is a one-line wrapper that directly invokes the neutron lifetime structure theorem.
Claim. The neutron decay Q-value is positive and the free neutron mean lifetime is positive.
background
Recognition Science encodes nuclear decay constraints via ledger propositions that require positivity of energy release and lifetime quantities. The neutron lifetime ledger is the conjunction asserting positive decay Q-value together with positive free neutron mean lifetime. This rests on the upstream neutron lifetime structure theorem, which proves the ledger by exact combination of the allowed decay condition and lifetime positivity.
proof idea
The proof is a one-line wrapper that applies the neutron lifetime structure theorem.
why it matters
This supplies the input condition required by the neutron lifetime discrepancy structure theorem in the same module. It links the RS nuclear ledger to experimental lifetime observables, consistent with the framework's use of positive quantities in decay processes. No open scaffolding questions are addressed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.