has_neutron_lifetime_input
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not compute a numerical value for the neutron lifetime.
- Does not resolve the beam versus bottle measurement discrepancy.
- Does not apply J-cost, phi-ladder scaling, or the eight-tick octave to this quantity.
- Does not incorporate relativistic or higher-order corrections from the RS model.
Lean usage
theorem neutron_lifetime_discrepancy_structure : neutron_lifetime_discrepancy_from_ledger := has_neutron_lifetime_inputformal statement (Lean)
10theorem has_neutron_lifetime_input : neutron_lifetime_from_ledger :=
proof body
One-line wrapper that applies neutron_lifetime_structure.
11 neutron_lifetime_structure
12