plateTypeCount

formal source

  23  | continentalFast | continentalSlow | oceanicFast | oceanicSlow | collisional
  24  deriving DecidableEq, Repr, BEq, Fintype
  25
  26theorem plateTypeCount : Fintype.card PlateType = 5 := by decide
  27
  28noncomputable def plateVelocityAtRung (k : ℕ) : ℝ := phi ^ k
  29
  30theorem plateVelocityRatio (k : ℕ) :
  31    plateVelocityAtRung (k + 1) / plateVelocityAtRung k = phi := by
  32  unfold plateVelocityAtRung
  33  have hpos := pow_pos phi_pos k
  34  rw [pow_succ, div_eq_iff hpos.ne']
  35  ring
  36
  37structure PlateMotionCert where
  38  five_types : Fintype.card PlateType = 5
  39  phi_ratio : ∀ k, plateVelocityAtRung (k + 1) / plateVelocityAtRung k = phi
  40
  41noncomputable def plateMotionCert : PlateMotionCert where
  42  five_types := plateTypeCount
  43  phi_ratio := plateVelocityRatio
  44
  45end IndisputableMonolith.Geology.PlateMotionFromPhiLadder