lifetime
plain-language theorem explainer
lifetime defines the mean lifetime at rung k on the phi-ladder as phi raised to k in RS-native units. Nuclear physicists analyzing neutron decay or exotic channels cite this when scaling lifetimes from the ladder to experimental Q-values. The declaration is a direct one-line definition that encodes the rung scaling without further computation.
Claim. The mean lifetime at rung $k$ on the phi-ladder is given by $l(k) = phi^k$.
background
The module treats five canonical exotic decay channels (alpha, beta-minus, beta-plus, electron-capture, spontaneous-fission) with configDim D = 5. Each channel lifetime occupies one rung on the phi-ladder, the sequence of values scaled by successive powers of phi. Phi itself enters as the self-similar fixed point forced in the upstream UnifiedForcingChain at T6.
proof idea
One-line definition that directly sets lifetime k to phi^k, implementing the rung scaling on the phi-ladder.
why it matters
This definition supplies the lifetime input to downstream results including neutron_lifetime_discrepancy_structure, neutron_decay_allowed, and neutron_lifetime_structure. It fills the rung-scaling step required by the phi-ladder construction in the Decay Spectrum module, linking to T6 (phi forced) and the mass formula yardstick * phi^(rung - 8 + gap(Z)).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.