PlateMotionCert
PlateMotionCert records that the plate type set has cardinality five and that velocities on the phi-ladder scale by the golden ratio between consecutive rungs. Earth scientists applying Recognition Science to tectonics would cite the certificate when checking ladder consistency with observed speeds from 1 cm/year to 17 cm/year. It is supplied as a bare structure definition with no proof obligations or lemmas.
claimA structure whose fields assert that the set of plate types has cardinality 5 and that for every natural number $k$ the ratio of the velocity at rung $k+1$ to the velocity at rung $k$ equals the golden ratio $phi$, where the velocity at rung $k$ is defined to be $phi^k$.
background
The module treats plate velocities as instances of the phi-ladder. Observed speeds range from roughly 1 cm/year (Eurasian) to 17 cm/year (Pacific) with fastest-to-slowest ratio near 17, comparable to $phi^5$. The central prediction is that velocities occupy rungs of the ladder with adjacent rungs scaled by $phi$, and that five canonical plate types arise as the configuration dimension in the Recognition framework.
proof idea
Direct structure definition. The two fields are declared as propositions with no lemmas applied and no tactics used.
why it matters in Recognition Science
The structure is instantiated by the downstream plateMotionCert, which supplies the concrete values plateTypeCount and plateVelocityRatio. It thereby embeds the phi-ladder into the geology tier, realizing the self-similar fixed point for velocities and connecting to the five-type count that matches configDim D = 5.
scope and limits
- Does not derive the five plate types from the spatial dimension three.
- Does not match the velocity function to measured cm/year values.
- Does not prove stability of the classification under plate interactions.
- Does not address time-dependent evolution of plate boundaries.
formal statement (Lean)
37structure PlateMotionCert where
38 five_types : Fintype.card PlateType = 5
39 phi_ratio : ∀ k, plateVelocityAtRung (k + 1) / plateVelocityAtRung k = phi
40