richter_b_value_in_aki_window
plain-language theorem explainer
The RS-derived Gutenberg-Richter b-value lies inside the Aki window 0.85 < b < 1.15. Seismologists comparing ledger-based predictions to global catalogs would cite this result to show consistency with the observed b ≈ 1. The proof reduces the claim to the equality b = 1 and verifies the numerical bounds directly.
Claim. The base-10 slope $b$ of the Gutenberg-Richter frequency-magnitude relation satisfies $0.85 < b < 1.15$, where $b$ equals the product of rungs per magnitude and the natural-log rung slope divided by $ln 10$.
background
In the Recognition Science treatment of geology, earthquake magnitudes correspond to stress-drop events on the phi-ladder of recognition costs. The Gutenberg-Richter law states that the cumulative number of events $N(M)$ with magnitude at least $M$ obeys $log_{10} N(M) = a - b M$. The module derives that each Richter magnitude unit spans $R = log_{10} (phi^{-1})$ rungs, and the frequency ratio per rung is $1/phi$, forcing the slope $b$ to equal 1.
proof idea
The proof applies the equality theorem that sets the b-value to 1, then uses norm_num to confirm that 0.85 is less than 1 and 1 is less than 1.15.
why it matters
This result supplies the numerical bound required by the master certificate gutenbergRichterCert for the Gutenberg-Richter law. It confirms that the forced value b = 1 from the phi-ladder lies inside the empirical Aki window (0.85, 1.15) commonly reported in seismology. The derivation ties to the Recognition Composition Law and the self-similar fixed point phi, ensuring the frequency drop per energy rung matches observations without free parameters.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.