veiRatio_pos
plain-language theorem explainer
The theorem establishes that the VEI ratio is strictly positive for any positive volcanic explosivity index. Modelers deriving per-octave J-cost impulses on the eight-tick climate cascade cite this result to guarantee non-negative forcing contributions from sub-saturation eruptions. The argument is a direct one-line wrapper that unfolds the ratio definition and invokes division positivity on the saturation threshold.
Claim. If $0 < V$, then $0 < V / V_{sat}$, where $V_{sat}$ denotes the saturation threshold corresponding to a Tambora-class eruption.
background
In this module the VEI ratio is introduced as the actual volcanic explosivity index divided by the saturation value for a Tambora-class event, taking values in (0,1] for sub-saturation cases. The surrounding development treats volcanic eruptions as instantaneous sources whose per-octave impulse magnitude is given by the J-cost of this ratio multiplied by the eight-tick period. The module replaces an earlier placeholder exponent with a derivation that pulls the period from Patterns.eight_tick_min and the cost scaling from Cost.Jcost.
proof idea
The proof is a one-line wrapper. It unfolds the definition of veiRatio to obtain the quotient vei / vei_saturation, then applies the exact tactic with the division-positivity lemma instantiated at the hypothesis 0 < vei together with the already-established positivity of the saturation threshold.
why it matters
This positivity result is invoked directly by the downstream theorems impulse_per_octave_nonneg and impulse_per_octave_pos_of_ne_sat, which establish that the per-octave impulse is non-negative and strictly positive away from saturation. It therefore anchors the concrete geological forcing terms to the T7 eight-tick octave and the J-cost ledger, completing the replacement of the v4 skeleton with a derivation that respects the Recognition Composition Law and the D=3 spatial dimension.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.