PlateType
plain-language theorem explainer
PlateType enumerates the five canonical tectonic plate categories in the Recognition Science geology model. Researchers modeling plate velocities on the phi-ladder cite this inductive type to fix the configuration dimension at five. The definition is a direct enumeration that automatically derives finite type and equality instances with no proof obligations.
Claim. The inductive type of plate types consists of five constructors: continental fast, continental slow, oceanic fast, oceanic slow, and collisional, equipped with decidable equality and finite type structure.
background
The module on plate tectonic motion from the phi-ladder predicts that plate velocities lie on the phi-ladder with adjacent plates differing by factor phi. Plate velocities span from approximately 1 cm/year for the Eurasian plate to 17 cm/year for the Pacific plate, yielding a fastest-to-slowest ratio near phi^5. The five canonical plate types (continental fast, continental slow, oceanic fast, oceanic slow, collisional) realize configuration dimension D equals 5.
proof idea
The declaration is a direct inductive definition enumerating the five plate types, with automatic derivation of DecidableEq, Repr, BEq, and Fintype instances.
why it matters
This definition supplies the finite set whose cardinality equals 5 in the downstream PlateMotionCert structure, which also asserts the phi-ratio property for velocities at successive rungs. It anchors the configDim D equals 5 step in the Recognition Science geology tier and supports the phi-ladder velocity predictions stated in the module. The module notes that the observed velocity ratio of approximately 17 lies within a factor of 1.5 of phi^5.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.