IndisputableMonolith.Experimental.NeutronLifetimeDiscrepancyStructure
The module defines the neutron-lifetime-discrepancy structure and derives its implication to the neutron-lifetime input. Experimental researchers comparing RS predictions to beam versus bottle lifetime data would cite this module. It consists of predicate definitions and a direct implication built atop the imported NeutronLifetimeStructure framework.
claimNeutron lifetime discrepancy structure implies neutron lifetime input: if a discrepancy structure is present then the lifetime input predicate holds.
background
The module sits in the experimental domain and imports the core framework from Nuclear.NeutronLifetimeStructure (P-015: What Determines the Lifetime of the Neutron?). That upstream module formalizes the RS structural framework for neutron lifetime. The present module adds predicates has_neutron_lifetime_input, neutron_lifetime_discrepancy_from_ledger, neutron_lifetime_discrepancy_structure and the implication neutron_discrepancy_implies_lifetime_input.
proof idea
This is a definition module, no proofs. It introduces the discrepancy predicates and states the implication to the lifetime input via the imported structural framework.
why it matters in Recognition Science
The module supplies the experimental implication step for P-015 on neutron lifetime. It connects observed discrepancies to the required RS input parameters and prepares the structure for downstream experimental checks. No used_by edges are recorded yet.
scope and limits
- Does not compute numerical neutron lifetime values.
- Does not resolve the experimental beam-bottle discrepancy.
- Does not address lifetimes of other particles.
- Limits scope to the structural implication only.