cumulative_ratio_pos
plain-language theorem explainer
The theorem asserts that the cumulative recurrence ratio across any number of VEI steps is strictly positive. Modelers assembling the EruptionRecurrenceCert for volcanic interval predictions on the phi-ladder would cite this result to confirm the ladder remains well-defined. The proof is a one-line term wrapper that unfolds the explicit power definition and applies the standard positivity lemma for real exponentiation with positive base.
Claim. For every natural number $k$, the cumulative recurrence ratio satisfies $0 < phi^{2k}$.
background
The volcanic eruption recurrence ladder models VEI class intervals as steps on the recognition lattice, with each step corresponding to one octave in the J-cost spectrum. The cumulative ratio across $k$ steps is defined explicitly as $phi^{2k}$, where $phi$ is the golden-ratio fixed point arising from the recognition composition law. This positivity result is one of the structural fields collected inside the EruptionRecurrenceCert record.
proof idea
The proof is a one-line term-mode wrapper. It unfolds the definition of cumulative_ratio to obtain the power expression, then applies the lemma pow_pos instantiated at the positivity of phi.
why it matters
This theorem supplies the cumulative_pos field required by the EruptionRecurrenceCert construction, which certifies the full set of recurrence-ladder properties. It directly supports the module's prediction that the cumulative ratio equals $phi^{2k}$ and aligns with the eight-tick octave structure (T7) and phi-ladder scaling used throughout Recognition Science. The result closes a basic well-definedness requirement before empirical band checks against Smithsonian GVP data.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.