impulse_at_saturation
plain-language theorem explainer
The per-octave J-cost impulse vanishes exactly when the VEI ratio reaches unity because that argument sits at the minimum of the J function. Climate modelers using Recognition Science would cite this when fixing the zero point of volcanic forcing against a saturation reference such as Tambora. The proof is a direct algebraic reduction that substitutes the saturation ratio and invokes the known J-cost value at argument one.
Claim. Let $I(r)$ denote the per-octave impulse $I(r) = J(r) · 8$, where $J(r) = (r-1)^2/(2r)$ is the J-cost function and $r$ is the eruption magnitude divided by the saturation reference. Then $I(1) = 0$.
background
In this module volcanic eruptions are treated as instantaneous sources on the eight-tick climate attractor. The J-cost function $J(x) = (x-1)^2/(2x)$ measures the defect of a ratio $x$ and reaches its global minimum of zero at $x=1$. The per-octave impulse multiplies this cost by the octave length 8, which is forced by the minimal complete-cover period at spatial dimension 3 (T7).
proof idea
The proof unfolds the definition of impulse_per_octave, replaces the saturation ratio with 1 via veiRatio_at_saturation, applies the lemma Jcost_unit0 that gives Jcost(1)=0, and finishes by ring simplification.
why it matters
This result supplies the saturation-zero fact required by volcanic_forcing_one_statement, which packages the octave period, the zero impulse at saturation, and the positive impulse for sub-saturation events into one structural theorem. It also populates the certificate volcanicForcingAsJCostImpulseCert. The placement closes the J-cost minimum calibration inside the volcanic forcing model that replaces the v4 skeleton, consistent with the eight-tick octave at D=3.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.