lifetime_ratio
Consecutive lifetimes on the phi-ladder satisfy a constant ratio of phi. Researchers modeling exotic decays would cite this result to confirm geometric progression across the five channels. The proof is a direct algebraic reduction that substitutes the power definition and cancels via exponent arithmetic.
claimFor every natural number $k$, if the lifetime at rung $k$ is defined by $L(k) = phi^k$, then $L(k+1)/L(k) = phi$.
background
The module assigns each of the five exotic decay channels (alpha, beta-minus, beta-plus, electron-capture, spontaneous-fission) a lifetime one rung higher on the phi-ladder. The lifetime function is introduced explicitly as the power $phi^k$. This construction sits inside the Recognition Science setting where phi arises as the self-similar fixed point forced by the J-uniqueness relation.
proof idea
Unfold the lifetime definition to obtain powers of phi. Apply positivity of phi to the k power, rewrite the division via the equality condition, substitute the successor exponent rule, and finish with ring simplification.
why it matters in Recognition Science
The theorem supplies the phi_ratio field inside the decaySpectrumCert definition that certifies the full spectrum for the five channels. It directly instantiates the phi-ladder step of the unified forcing chain (T6) and closes the exact scaling relation without additional hypotheses.
scope and limits
- Does not assign particular channels to specific rungs.
- Does not derive phi from the underlying J-cost equation.
- Does not treat absolute lifetime values or particle masses.
- Does not extend the ratio to non-exotic decay processes.
formal statement (Lean)
30theorem lifetime_ratio (k : ℕ) : lifetime (k + 1) / lifetime k = phi := by
proof body
Term-mode proof.
31 unfold lifetime
32 have hpos : (0 : ℝ) < phi ^ k := pow_pos phi_pos k
33 rw [div_eq_iff hpos.ne', pow_succ]
34 ring
35