lifetime_pos
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.
claimFor 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 in Recognition Science
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.
scope and limits
- Does not compute explicit numerical lifetimes for any channel.
- Does not derive the assignment of channels to specific rungs.
- Does not address physical units or conversion to seconds.
- Does not prove positivity for non-natural arguments.
formal statement (Lean)
36theorem lifetime_pos (k : ℕ) : 0 < lifetime k := pow_pos phi_pos k
proof body
37