action_ratio
plain-language theorem explainer
The theorem shows that consecutive tunneling actions on the phi-ladder satisfy a constant ratio equal to phi. Modelers of vacuum decay channels cite it to confirm self-similar scaling in the five-channel setup. The proof reduces directly to unfolding the power definition followed by algebraic rewriting and ring normalization.
Claim. Let $S(k) := phi^k$ be the tunneling action indexed by natural number $k$. Then $S(k+1)/S(k) = phi$ holds for every $k$.
background
The Vacuum Decay from J-Cost module treats five canonical channels (false-vacuum tunneling, Coleman-de Luccia, sphaleron, instanton, thermal quench) whose actions lie on the phi-ladder. The upstream definition sets tunnelingAction(k) to the real number phi raised to k, where phi is the self-similar fixed point fixed by the Recognition Science forcing chain. This supplies the scaling relation needed for the decay certificate.
proof idea
The term proof unfolds tunnelingAction to expose the powers, introduces the positivity fact for phi^k, rewrites the division via div_eq_iff, replaces the successor exponent, and finishes with ring.
why it matters
The result populates the phi_ratio field inside vacuumDecayCert, which assembles the five-channel certificate. It realizes the constant ratio expected from the phi fixed point (T6) and closes the scaling step in the J-cost vacuum-decay construction.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.