impulse_after_octaves_zero
plain-language theorem explainer
The theorem states that the volcanic impulse after zero octaves equals the per-octave J-cost impulse for any VEI. Climate modelers initializing the geometric decay series on the eight-tick cascade would cite it to anchor the relaxation at the initial forcing step. The proof is a one-line wrapper that unfolds the decay definition and simplifies the n=0 case directly.
Claim. For any real number $v$ representing VEI, the impulse after zero octaves of relaxation equals the per-octave J-cost impulse: $I(v,0)=J(v)$, where $I(v,n)$ is the impulse after $n$ octaves decaying at rate $1/φ$ and $J(v)$ is the J-cost of the VEI ratio times the octave period 8.
background
The module frames volcanic eruptions as instantaneous σ-sources on the eight-tick climate attractor, with impulse magnitude derived from Cost.Jcost applied to the VEI ratio and scaled by the octave period from Patterns.eight_tick_min. The upstream definition states that the per-octave impulse decays geometrically over n octaves with rate 1/φ, so impulse_after_octaves(vei,n) equals impulse_per_octave(vei) divided by φ^n. The per-octave impulse itself is the J-cost of the VEI ratio multiplied by the octave period 8, which is 2^D from T7 at D=3.
proof idea
The proof is a one-line wrapper that unfolds the definition of impulse_after_octaves and applies simp to reduce the n=0 case, where φ^0 evaluates to 1 and the division drops out.
why it matters
This result initializes the geometric decay series for volcanic impulses, ensuring the n=0 term matches the J-cost construction that replaces the v4 placeholder VEI^8. It grounds the exponent 8 in the eight-tick minimal cover from T7 and supports consistency checks at the saturation point veiRatio=1. The declaration sits at the base of the module's forcing derivations, directly feeding any downstream relaxation calculations that apply the phi-ladder decay.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.