Pith. sign in
module module moderate

IndisputableMonolith.Nuclear.NeutronLifetimeStructure

show as:
view Lean formalization →

The module Nuclear.NeutronLifetimeStructure supplies structural placeholder definitions for free-neutron beta-decay quantities in Recognition Science. It defines the Q-value, mean lifetime, and basic allowance/positivity conditions that feed the experimental discrepancy analysis. The module contains only definitions and implication wrappers with no deep theorems.

claimThe module defines the free-neutron beta-decay Q-value $Q_n$ (in MeV) as a structural placeholder together with the mean lifetime $\tau_n$ and the predicates decay-allowed, lifetime-positive, and phase-space-positive.

background

The module sits in the Nuclear domain and imports only Mathlib. It introduces the neutron decay Q-value as a structural placeholder and the free neutron mean life, along with the three predicates neutron_decay_allowed, neutron_lifetime_positive, and neutron_decay_phase_space_positive. These objects are the direct siblings listed in the module and serve as the interface between the Recognition Science mass formula and nuclear decay observables.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module feeds IndisputableMonolith.Experimental.NeutronLifetimeDiscrepancyStructure, supplying the structural basis for comparing Recognition Science lifetime expressions against measured neutron lifetime data. It fills the nuclear-scale application of the phi-ladder mass formula and the eight-tick octave structure.

scope and limits

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

declarations in this module (10)