pith. machine review for the scientific record. sign in
theorem proved term proof high

eruption_recurrence_one_statement

show as:
view Lean formalization →

The declaration packages the band (2.59, 2.63) for the VEI-adjacent recurrence ratio together with the power law for cumulative ratios over k steps and the base case at k=1. Geophysicists modeling volcanic recurrence on the phi-ladder would cite it to connect the recognition lattice to Smithsonian GVP statistics. The proof is a one-line term that directly assembles the three upstream results into a single conjunction.

claimLet $r = phi^2$. Then $2.59 < r < 2.63$, and for every natural number $k$ the cumulative recurrence ratio satisfies $C(k) = r^k$, with the base case $C(1) = r$.

background

The module models volcanic eruptions as a phi-rational ladder on the recognition lattice. Each VEI step corresponds to one octave in the J-cost impulse spectrum, so the recurrence-interval ratio between adjacent classes is defined as vei_step_ratio := phi^2. The cumulative ratio across k steps is defined as cumulative_ratio k := phi^(2*k), which is algebraically identical to (phi^2)^k. Upstream results supply the numerical band for the ratio, the factorization identity, and the one-step identity.

proof idea

The proof is a term-mode conjunction that applies vei_step_ratio_band for the interval, cumulative_ratio_factors (which unfolds both definitions and rewrites via pow_mul) for the general power law, and cumulative_ratio_one_step (which reduces to reflexivity) for the base case. No additional tactics are required.

why it matters in Recognition Science

This theorem is the master certificate for Track E6 of the eruption-recurrence prediction. It supplies the concrete phi^2 ratio (approximately 2.618) required by the eight-tick octave plus gap-45 frustration, and it matches the empirical 2.5-2.7 band reported for n >= 4 in the Smithsonian GVP catalog. The result closes the structural link between the self-similar fixed point phi and observable geophysical recurrence intervals.

scope and limits

formal statement (Lean)

 113theorem eruption_recurrence_one_statement :
 114    (2.59 < vei_step_ratio ∧ vei_step_ratio < 2.63) ∧
 115    (∀ k : ℕ, cumulative_ratio k = vei_step_ratio ^ k) ∧
 116    cumulative_ratio 1 = vei_step_ratio :=

proof body

Term-mode proof.

 117  ⟨vei_step_ratio_band, cumulative_ratio_factors, cumulative_ratio_one_step⟩
 118
 119end
 120
 121end EruptionRecurrenceLadder
 122end Geology
 123end IndisputableMonolith

depends on (5)

Lean names referenced from this declaration's body.