EruptionRecurrenceCert
plain-language theorem explainer
EruptionRecurrenceCert packages the positivity, band membership in (2.59, 2.63), and algebraic closure properties of the VEI recurrence ratios under the phi-ladder. Geophysicists matching Smithsonian GVP catalogs to predicted recurrence intervals would cite the certificate when checking the phi-squared step ratio. The structure is introduced directly as a record type whose fields are supplied by the downstream construction that invokes the upstream positivity and equality lemmas on cumulative_ratio and vei_step_ratio.
Claim. Let $r := phi^2$ and let $c(k) := phi^{2k}$ for $k$ a natural number. The certificate asserts $0 < r$, $2.59 < r < 2.63$, $0 < c(k)$ for every natural $k$, $c(k) = r^k$ for every natural $k$, and $c(1) = r$.
background
The module treats volcanic eruption recurrence intervals as lying on a phi-rational ladder derived from the recognition lattice. vei_step_ratio is defined as phi^2; cumulative_ratio k is defined as phi^(2*k). The module doc states: 'Volcanic eruptions in the Smithsonian Global Volcanism Program catalog cluster on a φ-rational recurrence ladder. The recurrence-interval ratio between successive Volcanic Explosivity Index (VEI) classes is T_VEI(n+1) / T_VEI(n) = φ² (approximately 2.618, consistent with the empirical 2.5–2.7 ratio seen in Smithsonian GVP n ≥ 4 classes). Each VEI step represents one octave on the recognition lattice's J-cost impulse spectrum.'
proof idea
The declaration introduces a structure type whose five fields are the listed properties. No proof body is present. The fields are populated by the downstream construction eruptionRecurrenceCert, which applies the upstream theorems cumulative_ratio_pos, cumulative_ratio_factors, cumulative_ratio_one_step together with the corresponding positivity and band results for vei_step_ratio.
why it matters
The certificate supplies the master structural claim for the eruption recurrence model (Track E6). It is consumed by the construction of eruptionRecurrenceCert. The construction realizes the prediction that the recurrence ratio lies in (2.59, 2.63) and that the cumulative ratio equals phi to the power 2k, consistent with the eight-tick octave and phi-ladder of the Recognition framework. The module doc identifies the falsifier as any median ratio outside (2.5, 2.7) for adjacent VEI classes with n ≥ 4.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.