VolcanismCert
plain-language theorem explainer
VolcanismCert packages the assertion that volcanic explosivity follows the phi-ladder with exactly five categories and successive ejecta ratios equal to phi. Geophysicists working in the Recognition Science program cite this structure when checking whether observed VEI distributions align with the predicted scaling. The definition consists of two fields that directly encode the cardinality condition on VEICategory and the ratio property on ejectionAtRung.
Claim. Let VEICategory be the inductive type with five constructors for the intervals VEI 0-1, 2-3, 4-5, 6-7, 8+. A VolcanismCert is a structure whose fields assert that the cardinality of VEICategory equals 5 and that the ejecta volume function satisfies $V(k+1)/V(k) = phi$ for all natural numbers $k$, where $V(k) = phi^k$.
background
The module VolcanismFromPhiLadder develops a Tier C geology model in which volcanic eruption intensity follows the phi-ladder. VEI values from 0 to 8 are grouped into five categories: vei01, vei23, vei45, vei67, vei8plus. The function ejectionAtRung maps each natural number rung k to phi raised to k, so that the ratio between consecutive rungs is exactly phi. This setup implements the module's claim that VEI scale units lie on the phi-ladder and that five categories correspond to configDim D = 5.
proof idea
The declaration is a structure definition with no proof body. It simply declares the two fields five_categories and phi_ratio that must hold for any inhabitant of VolcanismCert. No tactics or lemmas are invoked; the content is purely definitional.
why it matters
VolcanismCert supplies the type for the downstream definition volcanismCert, which constructs an explicit inhabitant using veiCategoryCount and ejectionRatio. This declaration realizes the module's prediction that VEI follows the phi-ladder, connecting to the Recognition Science forcing chain where phi is the self-similar fixed point. It addresses the open question of whether geological phenomena exhibit the same phi-scaling as the core physics constants.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.