impulse_per_octave_pos_of_ne_sat
plain-language theorem explainer
Volcanic forcing models in the Recognition Science framework rely on this result to ensure that sub-saturation eruptions produce strictly positive per-octave impulses in the eight-tick climate cascade. Researchers deriving cooling magnitudes from VEI values would invoke it to confirm non-zero J-cost contributions when the ratio deviates from unity. The tactic proof reduces the claim to positivity of the squared J-cost term and the octave period after establishing the ratio is positive and unequal to one.
Claim. For any real number $v > 0$ with $v$ unequal to the saturation value $v_s$, the per-octave impulse satisfies $0 < I(v)$, where $I(v) = J(r) · P$, $r = v / v_s$, $J(r) = (r-1)^2 / (2r)$, and $P = 8$ is the octave period in ticks.
background
The module frames volcanic eruptions as instantaneous σ-sources on the eight-tick climate attractor. Each eruption contributes an impulse magnitude after one octave of relaxation given by impulse_per_octave(VEI) = J(VEI_ratio) · period, with period drawn from the T7 eight-tick octave at D=3. Here veiRatio is the eruption magnitude divided by vei_saturation (Tambora-class VEI=7), and J is the Recognition Science cost function. Upstream, octavePeriod is defined as 8 ticks and Jcost_eq_sq rewrites J(x) = (x-1)^2 / (2x) for x ≠ 0.
proof idea
The tactic proof unfolds impulse_per_octave, obtains 0 < veiRatio vei from veiRatio_pos, proves veiRatio vei ≠ 1 by contradiction via div_eq_one_iff_eq on the definition of veiRatio, invokes Jcost_eq_sq to replace the J-cost with the squared ratio form, shows (veiRatio vei - 1)^2 > 0 by sub_ne_zero, and multiplies the resulting positive factors including the positive octave period.
why it matters
This result feeds the downstream theorem impulse_pinatubo_pos, which applies it directly to obtain a positive impulse for VEI 6. It completes the positivity half of the per-octave J-cost derivation in the volcanic forcing module, confirming that the impulse vanishes exactly at saturation and is monotone below it. The argument rests on the T7 eight-tick period and the algebraic form of J-cost, closing one link in the chain from Patterns.eight_tick_min to concrete geology applications.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.