neutron_discrepancy_implies_lifetime_input
plain-language theorem explainer
The result shows that the neutron lifetime discrepancy derived from the ledger directly supplies the neutron lifetime input placeholder. Experimental groups reconciling beam versus bottle neutron lifetime measurements would cite this when mapping observed discrepancies onto Recognition Science ledger conditions. The proof is a one-line term that returns the hypothesis unchanged.
Claim. If the neutron lifetime discrepancy is obtained from the ledger, then the neutron lifetime input from the ledger holds, where the input asserts neutron decay charge $Q > 0$ and positive free neutron mean lifetime.
background
Recognition Science treats neutron lifetime via structural placeholders rather than explicit formulas. The definition neutron_lifetime_from_ledger requires neutronDecayQ > 0 and freeNeutronMeanLife > 0, serving as a minimal ledger condition for decay processes. The companion definition neutron_lifetime_discrepancy_from_ledger is set equal to this same proposition, creating an experimental interface in the NeutronLifetimeDiscrepancyStructure module.
proof idea
The proof is a term-mode identity: the hypothesis h is returned directly. Because neutron_lifetime_discrepancy_from_ledger is definitionally identical to neutron_lifetime_from_ledger, the implication holds by reflexivity with no additional lemmas required.
why it matters
The declaration supplies the minimal bridge that lets experimental neutron lifetime data enter the Recognition Science ledger without extra hypotheses. It sits downstream of the Nuclear.NeutronLifetimeStructure placeholder and upstream of any future reconciliation of the neutron lifetime anomaly with the phi-ladder mass formula. No downstream uses are recorded, leaving its role in full T5-T8 chain applications open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.