plateBoundaryDynamicsCert
plain-language theorem explainer
The master certificate for plate boundary dynamics is inhabited by direct construction from the module's ratio, inequality, and positivity results. A geophysicist applying φ-ladder scalings to tectonic velocities would cite this to confirm the model satisfies all certificate conditions. The definition proceeds by field-wise assignment using the ratio theorem for the φ² equality, the faster subduction theorem for the inequality, the Wilson positivity theorem, reflexivity for the unit seismic scale, and a short positivity proof for the subduction
Claim. The master certificate is inhabited, satisfying $v_ {sub}/v_{ridge}=φ^2$, $v_{ridge}<v_{sub}$, $0<w$, $c_{seismic}=1$, and $0<v_{sub}$ where $v_{sub}=c_{seismic}/φ^7$ and $v_{ridge}=c_{seismic}/φ^9$.
background
The module places plate boundary velocities on the φ-ladder with subduction speed defined as the reference seismic scale divided by φ^7 and ridge spreading as the same scale divided by φ^9. The reference scale c_seismic is the dimensionless RS-native unit set to 1. This yields the exact ratio φ² and the strict inequality that subduction exceeds ridge speed. The Wilson cycle lower bound is the dimensionless quantity whose positivity is established on the ladder interval (φ^9, φ^10) scaled by 45 Myr.
proof idea
The definition constructs the PlateBoundaryDynamicsCert structure by direct field assignment. The ratio field receives the subduction-to-ridge ratio theorem, the ridge-slower field receives the subduction-faster theorem, the Wilson field receives the Wilson positivity theorem, the seismic constant receives rfl, and the subduction positivity field is discharged by unfolding the speed and scale definitions then applying positivity after the fact that φ^7 is positive.
why it matters
This supplies the inhabited master certificate that closes the §XXIII.C geology row on plate tectonics. It aggregates the φ-ladder velocity results into a single structure whose fields confirm the ratio φ², the speed ordering, Wilson positivity, and unit seismic scale. The construction supports the Wilson cycle interval estimate of roughly 137–222 Myr but records no downstream dependencies yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.