neutron_lifetime_discrepancy_from_ledger
plain-language theorem explainer
The definition equates neutron_lifetime_discrepancy_from_ledger to the upstream proposition requiring positive neutron decay Q-value and positive free neutron mean life. Experimental modelers working on the neutron lifetime anomaly in Recognition Science cite it to connect ledger inputs to discrepancy structures. It is realized as a direct one-line alias to the placeholder definition in the Nuclear module.
Claim. Define the proposition $P$ to hold precisely when the neutron decay Q-value exceeds zero and the free neutron mean lifetime exceeds zero.
background
The module Experimental.NeutronLifetimeDiscrepancyStructure constructs experimental structures around the neutron lifetime discrepancy. It imports Nuclear.NeutronLifetimeStructure, whose definition neutron_lifetime_from_ledger serves as a structural placeholder for the full RS lifetime formula. The placeholder asserts neutronDecayQ > 0 and freeNeutronMeanLife > 0, supplying the base input proposition for all downstream discrepancy claims.
proof idea
The definition is a one-line alias that directly sets neutron_lifetime_discrepancy_from_ledger to the upstream neutron_lifetime_from_ledger.
why it matters
This definition supplies the hypothesis type for neutron_discrepancy_implies_lifetime_input, which extracts the lifetime input from the discrepancy assumption, and for neutron_lifetime_discrepancy_structure, which asserts the structure via has_neutron_lifetime_input. It anchors the neutron lifetime discrepancy inside the Recognition Science experimental chain, linking to the phi-ladder mass formula and RS-native constants. It leaves open the quantitative reconciliation of measured lifetime values with the predicted phi-ladder rung.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.