veiCategoryCount
plain-language theorem explainer
The theorem establishes that the finite type of volcanic eruption intensity categories contains exactly five elements. Geologists applying Recognition Science to eruption data would cite this to confirm the VEI grouping matches the predicted configuration dimension of five. The proof is a one-line decision procedure that enumerates the five constructors of the inductive type.
Claim. The finite type of volcanic eruption intensity categories has cardinality five: $|VEICategory| = 5$.
background
The module develops volcanic eruption intensity as following the phi-ladder, with each order of magnitude in ejecta volume approximating φ^k. Five VEI categories are grouped as 0-1, 2-3, 4-5, 6-7, and 8+, stated to equal configDim D = 5. The upstream inductive definition enumerates these five cases and derives Fintype, DecidableEq, Repr, and BEq instances.
proof idea
The proof is a one-line wrapper that applies the decide tactic. The tactic succeeds because the type is finite and the cardinality equality is decidable by exhaustive enumeration of the five constructors.
why it matters
This supplies the five_categories field inside the VolcanismCert definition. It implements the module claim that five VEI categories correspond to configDim D = 5, connecting phi-ladder predictions to geological observables such as the Tambora/Krakatau ratio approximating φ^5. The result sits inside the Tier C geology development that treats VEI scale units as lying on the phi-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.