pith. sign in
module module moderate

IndisputableMonolith.Experimental.NeutronLifetimeDiscrepancyStructure

show as:
view Lean formalization →

This module shows that a neutron-lifetime-discrepancy structure implies a neutron-lifetime input in the Recognition Science framework. Researchers examining neutron decay anomalies under RS would cite it. It imports the core NeutronLifetimeStructure module and organizes the implication through sibling definitions and theorems.

claimNeutron-lifetime-discrepancy structure implies neutron-lifetime input: $\text{discrepancy structure} \implies \text{has neutron lifetime input}$.

background

The module sits in the experimental domain and extends the RS structural framework for neutron lifetime. Upstream P-015 formalizes that framework. Sibling declarations introduce has_neutron_lifetime_input, neutron_lifetime_discrepancy_from_ledger, and the implication neutron_discrepancy_implies_lifetime_input.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

The module feeds experimental analysis of neutron lifetime under P-015. It supplies the discrepancy structure that links observed anomalies to the RS input ledger.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (4)