EruptionRecurrenceCert
plain-language theorem explainer
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.
Claim. The 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.