subduction_faster_than_ridge
plain-language theorem explainer
Subduction velocity exceeds ridge spreading velocity by the factor phi squared in the Recognition Science phi-ladder model of plate boundaries. Researchers working on geological timescales derived from the forcing chain would cite this result when establishing lower bounds on Wilson cycle durations. The proof proceeds by unfolding the definitions of the two speeds in terms of seismic velocity and phi powers, then invoking the positivity and ordering properties of phi to compare the reciprocals.
Claim. Let $v_{sub} := c_{seismic}/phi^7$ and $v_{ridge} := c_{seismic}/phi^9$. Then $v_{ridge} < v_{sub}$.
background
The module sets plate-boundary velocities on the phi-ladder with subduction speed defined as $c_{seismic}/phi^7$ and ridge spreading as $c_{seismic}/phi^9$. The local setting is the Recognition Science derivation of mantle convection rates, where seismic velocity supplies the dimensional scale and all geological periods sit at integer powers of phi. Upstream, phi_gt_onePointFive supplies the strict lower bound phi > 1.5 that drives the ordering of powers.
proof idea
The tactic proof unfolds the three definitions, obtains positivity of phi and its seventh and ninth powers, invokes phi_gt_onePointFive to reach phi > 1, applies pow_lt_pow_right₀ to obtain phi^7 < phi^9, and finishes with one_div_lt_one_div_of_lt on the reciprocals.
why it matters
The theorem supplies the ridge_slower field of plateBoundaryDynamicsCert, the master certificate for the geology module. It realizes the phi-ladder assignment for subduction versus ridge speeds that follows from T5 J-uniqueness and T6 phi forcing, and it directly supports the Wilson-cycle lower bound 45 · phi^9. The result closes one link in the chain from the eight-tick octave to observable geological periods.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.