action_pos
plain-language theorem explainer
The theorem establishes that the tunneling action, defined as the golden ratio raised to any natural number k, is strictly positive. Physicists studying vacuum decay in the Recognition Science model cite this positivity to ensure all five decay channels have positive action. The proof is a direct one-line application of the power-positivity lemma to the positivity of the golden ratio.
Claim. For every natural number $k$, $0 < phi^k$, where the tunneling action equals $phi^k$ and $phi > 0$.
background
In the Vacuum Decay from J-Cost module, the tunneling action is defined as phi raised to the power k for each natural number k. This construction supports the five canonical vacuum decay channels: false-vacuum tunneling, Coleman-de Luccia bubble, sphaleron, instanton, and thermal quench. The module reports zero sorry statements and zero axioms, relying on the upstream definition of the tunneling action.
proof idea
The proof is a one-line wrapper applying the lemma pow_pos to the fact phi_pos.
why it matters
This theorem supplies the action_always_pos field in the vacuumDecayCert definition. It anchors positivity for tunneling actions on the phi-ladder, consistent with the Recognition Science forcing chain and the requirement that actions remain positive in decay processes. It completes a basic positivity check for the vacuum decay certification.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.