IndisputableMonolith.Geophysics.MantelConvectionFromJCost

   1import Mathlib
   2import IndisputableMonolith.Constants
   3
   4/-!
   5# Mantle Convection from J-Cost — Tier F Geophysics
   6
   7Mantle convection drives plate tectonics. The Rayleigh number Ra ≈ 10^7
   8governs convection vigor. In RS terms, the heat flux ratio r =
   9(convective flux)/(conductive flux limit) follows the phi-ladder:
  10adjacent convection regimes (sluggish, transitional, vigorous) ratio by phi.
  11
  12Five canonical mantle convection modes (whole-mantle, layered,
  13episodic, plume-driven, plate-driven) = configDim D = 5.
  14
  15RS prediction: convection regime transitions at phi-ladder critical Ra.
  16
  17Lean status: 0 sorry, 0 axiom.
  18-/
  19
  20namespace IndisputableMonolith.Geophysics.MantelConvectionFromJCost
  21open Constants
  22
  23inductive ConvectionMode where
  24  | wholeMantle | layered | episodic | plumeDriven | plateDriven
  25  deriving DecidableEq, Repr, BEq, Fintype
  26
  27theorem convectionModeCount : Fintype.card ConvectionMode = 5 := by decide
  28
  29noncomputable def rayleighAtRung (k : ℕ) : ℝ := phi ^ k
  30
  31theorem rayleighRatio (k : ℕ) :
  32    rayleighAtRung (k + 1) / rayleighAtRung k = phi := by
  33  unfold rayleighAtRung
  34  have hpos := pow_pos phi_pos k
  35  rw [pow_succ]; field_simp [hpos.ne']
  36
  37structure MantelConvectionCert where
  38  five_modes : Fintype.card ConvectionMode = 5
  39  rayleigh_ratio : ∀ k, rayleighAtRung (k + 1) / rayleighAtRung k = phi
  40
  41noncomputable def mantelConvectionCert : MantelConvectionCert where
  42  five_modes := convectionModeCount
  43  rayleigh_ratio := rayleighRatio
  44
  45end IndisputableMonolith.Geophysics.MantelConvectionFromJCost
  46