EarthquakeScalingCert
plain-language theorem explainer
The structure certifies that earthquake event rates remain positive at every magnitude and drop by the constant factor phi to the negative two between consecutive magnitudes. Seismologists applying Recognition Science to seismic statistics would cite it to recover the Gutenberg-Richter b-value of one directly from the phi-ladder. The declaration is assembled as a structure that bundles the positivity and ratio properties supplied by the explicit power-law definition of the rate function.
Claim. Let $r(M)$ denote the event rate at natural-number magnitude $M$. The certificate asserts $r(M) > 0$ for every $M$ and $r(M+1)/r(M) = phi^{-2}$ for every $M$.
background
The module re-derives the Gutenberg-Richter frequency-magnitude law from the Recognition Science phi-ladder. Each magnitude increment corresponds to a two-rung descent, so adjacent classes differ in frequency by phi to the negative two, which recovers the empirical b-value near one. The upstream definition fixes the rate at magnitude M as phi raised to the power of negative two times M, supplying the closed-form power law used throughout the module.
proof idea
The structure is defined by packaging the positivity lemma for the rate function and the constant-ratio lemma between successive magnitudes. These two properties are supplied directly by the lemmas eventRate_pos and eventRate_ratio, which follow from algebraic simplification of the explicit phi-power expression.
why it matters
It supplies the certified scaling law that the downstream earthquakeScalingCert packages for the geology module. The construction realizes the self-similar descent required by the phi fixed point, providing a parameter-free account of the b approximately one exponent in the Gutenberg-Richter relation. The module records zero sorry statements and zero axioms for this derivation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.