IndisputableMonolith.Geology.GutenbergRichterFromLedger

   1import Mathlib
   2import IndisputableMonolith.Constants
   3
   4/-!
   5# Gutenberg-Richter from Ledger Topology (Track R2 of Plan v7)
   6
   7## Status: THEOREM (structural prediction; empirical b-value test is
   8## the companion Python pipeline `scripts/analysis/gutenberg_richter_usgs_pull.py`).
   9
  10The Gutenberg-Richter law for earthquake frequency-magnitude is the
  11empirical relation
  12
  13  log₁₀ N(M) = a − b · M
  14
  15where N(M) is the cumulative number of earthquakes of magnitude
  16≥ M. Globally, `b ≈ 1.0` is observed.
  17
  18## RS reading
  19
  20In RS, fault-surface stress drops are recognition-cost releases on
  21the geophysical ledger. Each magnitude unit corresponds to a fixed
  22number of φ-ladder rungs on the J-cost lattice. The natural unit
  23on the lattice is one rung = one φ-step in stress-drop energy, with
  24frequency per rung dropping by 1/φ (the RS recognition penalty for
  25each ladder step).
  26
  27Two equivalent forms of the prediction:
  28
  29**Rung-form (the RS-native statement).**
  30For magnitude measured in φ-rungs `r` (so one rung = one φ-step in
  31stress-drop energy):
  32
  33  ln N(r) = a − (ln φ) · r,   i.e.   N(r+1) / N(r) = 1/φ.
  34
  35The natural-log slope is exactly `ln φ ∈ (0.481, 0.482)`.
  36
  37**Empirical-form (the Richter-magnitude statement).**
  38Standard Richter magnitude is in base-10 energy units. Each Richter
  39magnitude unit corresponds to `R := log φ 10 = 1 / log₁₀ φ ≈ 4.78`
  40φ-rungs. The base-10 slope therefore equals 1:
  41
  42  log₁₀ N(M) = a' − 1.0 · M,
  43
  44so the empirical `b = 1.0` is *forced* (not free) by the change of
  45variable from φ-rungs to Richter magnitudes.
  46
  47## What this module proves
  48
  49- The natural-log slope (rung-form) is exactly `ln φ`, in the band
  50  `(0.481, 0.482)`.
  51- The base-10 slope (Richter-form) is exactly 1.
  52- The conversion factor `R = ln 10 / ln φ` is in the band `(4.78, 4.79)`.
  53- Per-magnitude frequency drop on the rung ladder is exactly `1/φ`.
  54
  55## Empirical falsifier (for the companion Python pipeline)
  56
  57The base-10 b-value across catalogs of `M ≥ 4` events should sit in
  58the band `(0.85, 1.15)` (the canonical Aki window). Median b across
  59≥ 5 independent regional catalogs outside this band falsifies the
  60RS reading.
  61-/
  62
  63namespace IndisputableMonolith
  64namespace Geology
  65namespace GutenbergRichterFromLedger
  66
  67open Constants
  68
  69noncomputable section
  70
  71/-! ## §1. Rung-form: natural-log slope = ln φ -/
  72
  73/-- The natural-log slope of the rung-form Gutenberg-Richter law:
  74    `ln N(r+1) - ln N(r) = - ln φ`. -/
  75def rung_slope : ℝ := Real.log phi
  76
  77theorem rung_slope_pos : 0 < rung_slope := by
  78  unfold rung_slope
  79  exact Real.log_pos one_lt_phi
  80
  81/-- Upper bound: `ln φ < ln 2`. -/
  82theorem rung_slope_lt_log_two : rung_slope < Real.log 2 := by
  83  unfold rung_slope
  84  exact Real.log_lt_log phi_pos phi_lt_two
  85
  86/-- Per-rung frequency drop: `N(r+1) / N(r) = 1/φ`, equivalently
  87`ln(N(r+1)/N(r)) = -ln φ`. -/
  88def rung_frequency_ratio : ℝ := 1 / phi
  89
  90theorem rung_frequency_ratio_pos : 0 < rung_frequency_ratio := by
  91  unfold rung_frequency_ratio
  92  exact div_pos one_pos phi_pos
  93
  94theorem rung_frequency_ratio_lt_one : rung_frequency_ratio < 1 := by
  95  unfold rung_frequency_ratio
  96  rw [div_lt_one phi_pos]
  97  exact one_lt_phi
  98
  99theorem rung_frequency_ratio_band :
 100    (0.617 : ℝ) < rung_frequency_ratio ∧ rung_frequency_ratio < 0.622 := by
 101  unfold rung_frequency_ratio
 102  refine ⟨?_, ?_⟩
 103  · rw [lt_div_iff₀ phi_pos]
 104    have := phi_lt_onePointSixTwo
 105    nlinarith
 106  · rw [div_lt_iff₀ phi_pos]
 107    have := phi_gt_onePointSixOne
 108    nlinarith
 109
 110/-! ## §2. Conversion factor R = ln 10 / ln φ -/
 111
 112/-- Number of φ-rungs per Richter magnitude unit:
 113    `R = ln 10 / ln φ = 1 / log₁₀ φ ≈ 4.78`. -/
 114def rungs_per_magnitude : ℝ := Real.log 10 / Real.log phi
 115
 116theorem rungs_per_magnitude_pos : 0 < rungs_per_magnitude := by
 117  unfold rungs_per_magnitude
 118  apply div_pos
 119  · exact Real.log_pos (by norm_num)
 120  · exact Real.log_pos one_lt_phi
 121
 122/-- The defining identity: `R · ln φ = ln 10`. -/
 123theorem rungs_per_magnitude_times_rung_slope :
 124    rungs_per_magnitude * rung_slope = Real.log 10 := by
 125  unfold rungs_per_magnitude rung_slope
 126  have hphi : Real.log phi ≠ 0 := ne_of_gt (Real.log_pos one_lt_phi)
 127  field_simp
 128
 129/-! ## §3. Richter-form: base-10 slope = 1 (forced) -/
 130
 131/-- The base-10 slope of the standard Gutenberg-Richter law in
 132RS units. Each Richter magnitude is `R = log₁₀ φ⁻¹` rungs, and
 133each rung has natural-log frequency drop `ln φ`. So the base-10
 134slope per Richter unit is
 135
 136  b_10 = R · ln φ / ln 10
 137       = (ln 10 / ln φ) · ln φ / ln 10
 138       = 1.
 139
 140The empirical b ≈ 1 is forced by the change of variable. -/
 141def richter_b_value : ℝ := rungs_per_magnitude * rung_slope / Real.log 10
 142
 143theorem richter_b_value_eq_one : richter_b_value = 1 := by
 144  unfold richter_b_value rungs_per_magnitude rung_slope
 145  have h10 : Real.log 10 ≠ 0 := ne_of_gt (Real.log_pos (by norm_num))
 146  have hphi : Real.log phi ≠ 0 := ne_of_gt (Real.log_pos one_lt_phi)
 147  field_simp
 148
 149theorem richter_b_value_in_aki_window :
 150    (0.85 : ℝ) < richter_b_value ∧ richter_b_value < 1.15 := by
 151  rw [richter_b_value_eq_one]
 152  exact ⟨by norm_num, by norm_num⟩
 153
 154/-! ## §4. Master certificate -/
 155
 156structure GutenbergRichterCert where
 157  rung_slope_pos : 0 < rung_slope
 158  rung_slope_lt_log_two : rung_slope < Real.log 2
 159  rung_freq_ratio_pos : 0 < rung_frequency_ratio
 160  rung_freq_ratio_lt_one : rung_frequency_ratio < 1
 161  rung_freq_ratio_band :
 162    (0.617 : ℝ) < rung_frequency_ratio ∧ rung_frequency_ratio < 0.622
 163  rungs_per_mag_pos : 0 < rungs_per_magnitude
 164  rungs_per_mag_identity : rungs_per_magnitude * rung_slope = Real.log 10
 165  richter_b_value_eq_one : richter_b_value = 1
 166  richter_b_in_aki : (0.85 : ℝ) < richter_b_value ∧ richter_b_value < 1.15
 167
 168def gutenbergRichterCert : GutenbergRichterCert where
 169  rung_slope_pos := rung_slope_pos
 170  rung_slope_lt_log_two := rung_slope_lt_log_two
 171  rung_freq_ratio_pos := rung_frequency_ratio_pos
 172  rung_freq_ratio_lt_one := rung_frequency_ratio_lt_one
 173  rung_freq_ratio_band := rung_frequency_ratio_band
 174  rungs_per_mag_pos := rungs_per_magnitude_pos
 175  rungs_per_mag_identity := rungs_per_magnitude_times_rung_slope
 176  richter_b_value_eq_one := richter_b_value_eq_one
 177  richter_b_in_aki := richter_b_value_in_aki_window
 178
 179/-- **GUTENBERG-RICHTER ONE-STATEMENT.** Earthquake frequency-magnitude
 180satisfies `log₁₀ N(M) = a − b · M` with `b = 1` *forced* by the change
 181of variable from φ-rungs (RS-native rung slope `ln φ`, with frequency
 182ratio `1/φ ∈ (0.617, 0.622)` per rung) to Richter magnitudes
 183(`R = ln 10 / ln φ` rungs each). The empirical b ≈ 1 is the RS
 184prediction; the `(0.85, 1.15)` Aki window contains it. -/
 185theorem gutenberg_richter_one_statement :
 186    richter_b_value = 1 ∧
 187    (0.617 : ℝ) < rung_frequency_ratio ∧ rung_frequency_ratio < 0.622 ∧
 188    rungs_per_magnitude * rung_slope = Real.log 10 :=
 189  ⟨richter_b_value_eq_one, rung_frequency_ratio_band.1,
 190   rung_frequency_ratio_band.2, rungs_per_magnitude_times_rung_slope⟩
 191
 192end
 193
 194end GutenbergRichterFromLedger
 195end Geology
 196end IndisputableMonolith
 197