impulse_pinatubo_pos
plain-language theorem explainer
The declaration establishes that the per-octave J-cost impulse from a VEI-6 eruption is strictly positive. Climate modelers using the Recognition Science derivation of volcanic forcing would cite it to confirm the ordering of transient cooling by eruption magnitude below saturation. The proof is a one-line application of the non-saturation positivity lemma with numerical checks that the input differs from the saturation threshold.
Claim. $0 < I(6)$, where $I(v)$ denotes the J-cost impulse magnitude delivered by an eruption of Volcanic Explosivity Index $v$ after one octave of relaxation on the climate cascade, with $I$ vanishing exactly at the saturation reference $v=7$.
background
In the Recognition Science model of volcanic forcing, an eruption acts as an instantaneous source on the eight-tick climate attractor. The impulse after one octave is given by $I(v) = J(v / v_s) · 8$, where the period 8 is forced by T7 at spatial dimension D=3 via Patterns.eight_tick_min, and $J$ is the cost function induced by the multiplicative recognizer comparator (MultiplicativeRecognizerL4.cost). The module derives all structural properties directly from Cost.Jcost and the minimal-cover property of the eight-tick period. Upstream results establish that the cost of any recognition event is non-negative and that the octave period equals eight ticks exactly.
proof idea
The proof applies the lemma impulse_per_octave_pos_of_ne_sat. It discharges the two hypotheses by norm_num: the input value 6 is positive, and unfolding vei_saturation yields 7 so that 6 differs from saturation.
why it matters
This supplies the third clause of the VolcanicForcingAsJCostImpulseCert structure and is assembled into the compact one-statement theorem volcanic_forcing_one_statement. It confirms that sub-saturation eruptions deliver positive forcing while the saturation reference sits at the J-cost zero point, consistent with T7 and the non-negativity of J-cost. The module notes that empirical calibration may shift the saturation reference, but the structural ordering remains fixed by the derivation from Patterns.eight_tick_min.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.