IndisputableMonolith.Geology.EarthquakeScalingFromJCost

   1import Mathlib
   2import IndisputableMonolith.Constants
   3
   4/-!
   5# Earthquake Magnitude Scaling from Phi-Ladder — Tier F Geology
   6
   7The Gutenberg-Richter frequency-magnitude law: log10(N) = a - b*M
   8with b ≈ 1 empirically. In RS terms, each magnitude step releases
   9phi^2 ≈ 2.618 times more energy (Richter magnitude increment = phi
  10in log10 energy space, calibrated so phi^2 ≈ 10^0.6 × log10 energy).
  11
  12Adjacent magnitude classes differ in event frequency by phi^(-2):
  13each unit of magnitude corresponds to a two-rung phi-ladder descent
  14in event rate. This is the RS re-derivation of the b = 1 exponent.
  15
  16Lean status: 0 sorry, 0 axiom.
  17-/
  18
  19namespace IndisputableMonolith.Geology.EarthquakeScalingFromJCost
  20open Constants
  21
  22noncomputable def eventRateAtMagnitude (M : ℕ) : ℝ := phi ^ (-(2 * (M : ℤ)))
  23
  24theorem eventRate_pos (M : ℕ) : 0 < eventRateAtMagnitude M :=
  25  zpow_pos phi_pos _
  26
  27theorem eventRate_ratio (M : ℕ) :
  28    eventRateAtMagnitude (M + 1) / eventRateAtMagnitude M = phi ^ (-(2 : ℤ)) := by
  29  unfold eventRateAtMagnitude
  30  have hphi_ne := phi_ne_zero
  31  have hpos : 0 < phi ^ (-(2 * (M : ℤ))) := zpow_pos phi_pos _
  32  -- phi^(-(2*(M+1))) / phi^(-(2*M)) = phi^(-2)
  33  have heq : phi ^ (-(2 * ((M : ℤ) + 1))) = phi ^ (-(2 * (M : ℤ))) * phi ^ (-(2 : ℤ)) := by
  34    rw [show -(2 * ((M : ℤ) + 1)) = -(2 * (M : ℤ)) + (-2 : ℤ) from by ring]
  35    exact zpow_add₀ hphi_ne _ _
  36  rw [show ((M + 1 : ℕ) : ℤ) = (M : ℤ) + 1 from by push_cast; ring]
  37  rw [heq]
  38  field_simp [hpos.ne']
  39
  40structure EarthquakeScalingCert where
  41  rate_pos : ∀ M, 0 < eventRateAtMagnitude M
  42  phi_sq_ratio : ∀ M, eventRateAtMagnitude (M + 1) / eventRateAtMagnitude M = phi ^ (-(2 : ℤ))
  43
  44noncomputable def earthquakeScalingCert : EarthquakeScalingCert where
  45  rate_pos := eventRate_pos
  46  phi_sq_ratio := eventRate_ratio
  47
  48end IndisputableMonolith.Geology.EarthquakeScalingFromJCost
  49