IndisputableMonolith.Nuclear.NeutronLifetimeStructure
The module supplies structural placeholders and basic properties for the free neutron beta-decay Q-value in MeV together with mean lifetime and decay allowances inside the Recognition Science nuclear domain. Experimental analyses of neutron lifetime discrepancies import these objects. The module contains only definitions and one-line implications with no substantive proofs.
claim$Q_n$ denotes the free-neutron beta-decay energy release in MeV as a structural placeholder; companion objects include the mean lifetime $τ_n$ and lemmas asserting decay is allowed, lifetime positive, and phase space positive.
background
The Nuclear.NeutronLifetimeStructure module operates in the nuclear domain and introduces neutronDecayQ as the free-neutron beta-decay Q value in MeV (structural placeholder). It also defines freeNeutronMeanLife along with neutron_decay_allowed, neutron_lifetime_positive, neutron_decay_phase_space_positive and the implication lemmas neutron_lifetime_implies_decay_allowed, neutron_lifetime_implies_positive_lifetime, neutron_lifetime_implies_phase_space_positive. The module imports only Mathlib and supplies the neutron lifetime structure used by downstream experimental discrepancy work.
proof idea
this is a definition module, no proofs
why it matters in Recognition Science
The module feeds IndisputableMonolith.Experimental.NeutronLifetimeDiscrepancyStructure, supplying the neutron lifetime structure required for discrepancy analysis. It fills the nuclear placeholder slot in the Recognition Science chain without deriving numerical values or linking to the phi-ladder.
scope and limits
- Does not assign a numerical value to neutronDecayQ.
- Does not derive lifetime from the phi-ladder or J-cost.
- Does not connect to the eight-tick octave or D=3.
- Does not perform any mass-formula calculation.
used by (1)
declarations in this module (10)
-
def
neutronDecayQ -
def
freeNeutronMeanLife -
theorem
neutron_decay_allowed -
theorem
neutron_lifetime_positive -
theorem
neutron_decay_phase_space_positive -
def
neutron_lifetime_from_ledger -
theorem
neutron_lifetime_structure -
theorem
neutron_lifetime_implies_decay_allowed -
theorem
neutron_lifetime_implies_positive_lifetime -
theorem
neutron_lifetime_implies_phase_space_positive