lifetime_pos
plain-language theorem explainer
The theorem states that the lifetime function evaluated at any natural number rung k is strictly positive. It is invoked inside the decay spectrum certificate that assembles the five exotic channels. The proof is a direct one-line application of the positivity of powers to the base phi.
Claim. For every natural number $k$, $0 < lifetime(k)$, where $lifetime(k) := phi^k$ and $phi > 0$.
background
The module constructs decay spectra by assigning each of the five canonical exotic channels (alpha, beta-minus, beta-plus, electron-capture, spontaneous-fission) to a rung on the phi-ladder. The lifetime function is introduced as the noncomputable definition lifetime(k) = phi^k. This theorem depends only on that definition together with the elementary fact that phi is positive.
proof idea
One-line wrapper that applies the lemma pow_pos to the positivity of phi and the exponent k.
why it matters
The result supplies the lifetime_always_pos field required by decaySpectrumCert, which certifies the five-channel spectrum together with the phi-ratio. It therefore anchors the phi-ladder construction used for decay rates in the Recognition Science framework, consistent with the self-similar fixed point and the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.