PlateType
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not assign numerical velocity values to each type.
- Does not prove the phi-ratio property for successive rungs.
- Does not connect the types to specific geological observations or data.
formal statement (Lean)
22inductive PlateType where
23 | continentalFast | continentalSlow | oceanicFast | oceanicSlow | collisional
24 deriving DecidableEq, Repr, BEq, Fintype
25