IndisputableMonolith.Geology.GutenbergRichterFromLedger
The module derives the rung-form Gutenberg-Richter law from the Recognition Science phi-ladder. Its central result states that the natural-log slope between consecutive rungs equals -ln φ, which forces the Richter b-value to equal one. Geophysicists modeling earthquake frequency-magnitude statistics would cite this for its RS-native account of the observed b=1. The module is organized as a chain of elementary lemmas on positivity, bounds, and equality.
claim$N(r)$ denotes event count on rung $r$ of the phi-ladder; the natural-log slope satisfies $ln N(r+1) - ln N(r) = -ln φ$, which implies the Richter b-value $b=1$.
background
The module imports the RS time quantum τ₀ = 1 tick from Constants. It introduces rung_slope as the difference ln N(r+1) - ln N(r) and derives its exact value -ln φ from the self-similar fixed point of the phi-ladder. Supporting definitions include rung_frequency_ratio (the multiplicative scaling factor between rungs) and rungs_per_magnitude (the number of rungs per unit magnitude).
proof idea
This is a definition module, no proofs. The declarations establish the slope via the phi definition, then verify positivity, the bound less than log 2, and the frequency ratio band before equating the b-value to one through direct algebraic relations.
why it matters in Recognition Science
This module supplies the RS-native derivation of the Gutenberg-Richter law with b=1 to the geology domain. It realizes the T6 self-similar fixed point in seismic statistics and feeds any later application of the phi-ladder to event-size distributions. The parent results are the unified forcing chain and the constants module that fix φ.
scope and limits
- Does not model time-dependent clustering or aftershocks.
- Does not derive absolute event rates from first principles.
- Does not address spatial fault geometry.
- Does not explain deviations from power-law scaling at extremes.
depends on (1)
declarations in this module (16)
-
def
rung_slope -
theorem
rung_slope_pos -
theorem
rung_slope_lt_log_two -
def
rung_frequency_ratio -
theorem
rung_frequency_ratio_pos -
theorem
rung_frequency_ratio_lt_one -
theorem
rung_frequency_ratio_band -
def
rungs_per_magnitude -
theorem
rungs_per_magnitude_pos -
theorem
rungs_per_magnitude_times_rung_slope -
def
richter_b_value -
theorem
richter_b_value_eq_one -
theorem
richter_b_value_in_aki_window -
structure
GutenbergRichterCert -
def
gutenbergRichterCert -
theorem
gutenberg_richter_one_statement