module module

`IndisputableMonolith.Geology.PlateBoundaryDynamics`

show as: view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import

declarations in this module (9)

def c_seismic L39
def subduction_speed L42
def ridge_spreading L45
theorem subduction_to_ridge_ratio L48
theorem subduction_faster_than_ridge L61
def wilson_cycle_lower_dimensionless L83
theorem wilson_cycle_lower_pos L85
structure PlateBoundaryDynamicsCert L94
def plateBoundaryDynamicsCert L102