VolcanicForcingAsJCostImpulseCert
plain-language theorem explainer
VolcanicForcingAsJCostImpulseCert bundles six properties that certify volcanic eruptions produce nonnegative J-cost impulses on the eight-tick octave, vanishing at saturation and decaying geometrically thereafter. Climate researchers extending the Recognition Science forcing chain to geology would cite it when linking VEI ratios to the T7 octave. The structure is assembled directly from lemmas on octavePeriod and impulse_per_octave.
Claim. Let $P$ denote the octave period and $I(v)$ the per-octave impulse for VEI ratio $v$. Then $P=8$, any surjective map from a finite set of size $T$ onto the 3-dimensional pattern space satisfies $8≤T$, $I(v)≥0$ for $v>0$, $I(1)=0$, $I(6/7)>0$, and for $v>0$ with $I(v)>0$ the sequence $I(v)/φ^n$ is nonincreasing in $n$.
background
The module replaces an earlier placeholder exponent with a derivation from Patterns.eight_tick_min and Cost.Jcost. An eruption supplies an instantaneous σ-source to the eight-tick attractor; the resulting impulse after one octave is Jcost(veiRatio vei) multiplied by the period. Upstream, octavePeriod is defined as 8*tick and impulse_per_octave(vei) as Jcost(veiRatio vei)*octavePeriod. The saturation reference vei_saturation marks the J-cost minimum. impulse_after_octaves then applies geometric decay at rate 1/φ per additional octave.
proof idea
This is a structure definition that packages six component results. It directly inserts octavePeriod_eq_eight, the surjectivity lemma octavePeriod_is_minimal_cover, impulse_per_octave_nonneg, impulse_at_saturation, impulse_pinatubo_pos, and the monotonicity statement for impulse_after_octaves. No new tactics are required beyond the referenced lemmas.
why it matters
The certificate supplies the structural backing for the §XXIII.C geology depth extension. It embeds the T7 eight-tick octave (period 2^D at D=3) and the Recognition Composition Law symmetry of Jcost into a concrete forcing term. The downstream volcanicForcingAsJCostImpulseCert uses it to expose the full certificate to climate-cascade applications. It closes the placeholder gap left by the v4 skeleton.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.