pith. machine review for the scientific record. sign in
structure definition def or abbrev high

EruptionRecurrenceCert

show as:
view Lean formalization →

EruptionRecurrenceCert assembles the positivity, band membership, and algebraic identities that certify the phi-squared recurrence ratio between successive VEI classes. A geophysicist testing long-term volcanic statistics against the recognition lattice would cite this structure to assert the predicted interval scaling. The definition simply collects five field assertions taken directly from the cumulative_ratio and vei_step_ratio definitions.

claimThe structure asserts that the VEI step ratio $r = phi^2$ satisfies $0 < r$ and $2.59 < r < 2.63$, that the cumulative ratio $c(k) = phi^{2k}$ obeys $0 < c(k)$ for every natural number $k$, that $c(k) = r^k$ for every $k$, and that $c(1) = r$.

background

Recognition Science predicts volcanic recurrence intervals via the phi-ladder arising from the J-cost spectrum and the eight-tick octave. The module sets vei_step_ratio to phi squared and cumulative_ratio(k) to phi raised to 2k, encoding two phi-steps per octave for long-period geophysical events. The local setting is Track E6 of Plan v6, where the ratio between adjacent VEI classes is phi squared (approximately 2.618) and lies in the band (2.59, 2.63) to match Smithsonian GVP medians for n greater than or equal to 4.

proof idea

This is a structure definition that bundles the required field assertions. It collects the positivity of vei_step_ratio, its membership in the numerical band, the universal positivity of cumulative_ratio, the factorization identity cumulative_ratio(k) equals vei_step_ratio to the k, and the one-step equality, each taken from the upstream definitions and their direct power lemmas.

why it matters in Recognition Science

The certificate supplies the structural prediction that feeds the master certificate eruptionRecurrenceCert. It realizes the phi-rational ladder from the recognition composition law and the T7 eight-tick octave, giving a concrete falsifiable band for VEI ratios. It touches the open question whether the empirical median ratio from the GVP catalog stays inside (2.5, 2.7) with additional data.

scope and limits

formal statement (Lean)

  95structure EruptionRecurrenceCert where
  96  step_ratio_pos : 0 < vei_step_ratio
  97  step_ratio_band : 2.59 < vei_step_ratio ∧ vei_step_ratio < 2.63
  98  cumulative_pos : ∀ k : ℕ, 0 < cumulative_ratio k
  99  cumulative_factors : ∀ k : ℕ,
 100    cumulative_ratio k = vei_step_ratio ^ k
 101  one_step_eq : cumulative_ratio 1 = vei_step_ratio
 102

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (2)

Lean names referenced from this declaration's body.