VEICategory
plain-language theorem explainer
The VEICategory inductive type enumerates the five standard volcanic explosivity index bins used in Recognition Science geology models. Geologists and RS theorists cite it when mapping eruption volumes to the phi-ladder and verifying configDim D equals 5. The definition consists of five constructors with automatic derivation of finite type structure that directly enables the downstream cardinality theorem.
Claim. The volcanic explosivity index is partitioned into five categories: VEI 0-1, 2-3, 4-5, 6-7, and 8 or greater.
background
In the Volcanism from Phi-Ladder module, volcanic eruption intensity follows the phi-ladder: VEI 0-8 with each order of magnitude in ejecta volume approximately φ^k. Five VEI categories are commonly used (VEI 0-1, 2-3, 4-5, 6-7, 8+), stated to equal configDim D = 5. The inductive definition supplies the discrete finite set on which cardinality and ratio properties are later established.
proof idea
The declaration is the inductive definition introducing the five constructors vei01, vei23, vei45, vei67, vei8plus together with derivations for DecidableEq, Repr, BEq, and Fintype.
why it matters
This definition supplies the finite set required by the downstream theorem veiCategoryCount establishing Fintype.card VEICategory = 5 and by the VolcanismCert structure requiring both five_categories and the phi ratio ∀ k, ejectionAtRung (k + 1) / ejectionAtRung k = phi. It realizes the module claim that VEI scale units lie on the phi-ladder with five categories matching configDim D = 5, extending the phi-ladder from fundamental constants to geological observables.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.