IndisputableMonolith.Nuclear.NeutronLifetimeStructure
The NeutronLifetimeStructure module supplies structural placeholders for the free neutron beta-decay Q-value in MeV and the associated mean lifetime within the Recognition Science nuclear layer. It also encodes basic allowance, positivity, and phase-space conditions that follow from those placeholders. Experimental physicists comparing neutron lifetime data to theory would cite these definitions. The module consists entirely of definitions and direct implications with no non-trivial proofs.
claimThe module defines the free-neutron beta-decay Q-value $Q_n$ (in MeV) as a structural placeholder, the free neutron mean lifetime $t_n$, and the derived statements that decay is allowed, $t_n > 0$, and the phase-space factor is positive.
background
This module sits in the Nuclear domain and imports only Mathlib. It introduces neutronDecayQ as the Q-value for free neutron beta decay, freeNeutronMeanLife as the mean lifetime, and a collection of simple implications (neutron_decay_allowed, neutron_lifetime_positive, neutron_decay_phase_space_positive, and the three implication lemmas). These objects serve as the interface between the Recognition Science forcing chain and nuclear observables.
proof idea
This is a definition module, no proofs. All content consists of direct definitions of the Q-value and lifetime together with one-line implications that follow immediately from the definitions.
why it matters in Recognition Science
The module supplies the nuclear-physics placeholders required by the downstream NeutronLifetimeDiscrepancyStructure in the Experimental domain. It therefore closes the structural gap between the Recognition Science constants (phi-ladder, T5–T8) and the free-neutron lifetime observable.
scope and limits
- Does not compute a numerical value for the neutron lifetime.
- Does not derive the lifetime from the phi-ladder mass formula.
- Does not incorporate experimental data or discrepancy analysis.
- Does not treat neutron decay inside nuclei or bound states.
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