subduction_to_ridge_ratio
plain-language theorem explainer
Subduction speed exceeds ridge spreading by the exact factor φ² on the Recognition Science φ-ladder for geological velocities. Plate tectonics researchers calibrating mantle convection timescales in dimensionless units would cite this equality when bounding Wilson cycle periods. The proof is a direct algebraic reduction that unfolds the two velocity definitions, expands φ⁹ = φ⁷ · φ², and simplifies the resulting fraction.
Claim. $v_ {sub}/v_ {ridge}=φ^2$ where $v_ {sub}=c_ {seismic}/φ^7$, $v_ {ridge}=c_ {seismic}/φ^9$, and $c_ {seismic}=1$ in RS-native units.
background
The module derives plate boundary velocities from the φ-ladder of geological timescales. The reference seismic velocity scale c_seismic is defined as the dimensionless constant 1. Subduction speed is then c_seismic divided by φ to the seventh power and ridge spreading is c_seismic divided by φ to the ninth power, so their ratio is φ squared by direct cancellation.
proof idea
The proof unfolds the three local definitions, introduces positivity of φ and its powers via phi_pos and pow_pos, expands φ^9 = φ^7 * φ^2 with the ring tactic, rewrites the numerator, and finishes with field_simp to obtain the exact power φ^2.
why it matters
This supplies the ratio_eq_phi_sq field of the master certificate plateBoundaryDynamicsCert. It realizes the φ² step on the φ-ladder velocities inside the geology section, consistent with the self-similar fixed point φ and the eight-tick octave structure. The result anchors the lower bound on Wilson cycle periods in the interval (φ^9, φ^10) times 45 Myr.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.