PlateBoundaryDynamicsCert
plain-language theorem explainer
The PlateBoundaryDynamicsCert structure records that subduction velocity exceeds ridge spreading by exactly phi squared, with both speeds positive and the Wilson cycle lower bound positive. Modelers working on Recognition Science geology or phi-ladder timescales would cite it to close the plate-boundary velocity row. The structure is populated directly from the module's velocity definitions and positivity facts with no additional lemmas required.
Claim. The master certificate asserts that subduction velocity divided by ridge spreading velocity equals $phi^2$, that ridge spreading velocity is strictly less than subduction velocity, that the dimensionless Wilson cycle lower bound is positive, that the reference seismic velocity scale equals 1, and that subduction velocity is positive.
background
The module places plate-boundary velocities on the phi-ladder of geological timescales. Subduction speed is defined as the reference seismic velocity scale divided by phi to the seventh power; ridge spreading is the same scale divided by phi to the ninth power. Their ratio is therefore phi squared by direct cancellation. The Wilson cycle lower bound is taken in the interval (phi^9, phi^10) scaled by 45 Myr, and the certificate records its positivity together with the positivity of subduction speed and the normalization of the seismic scale to unity.
proof idea
The structure is a definition whose five fields are filled by direct reference to the module's velocity definitions and the already-proved positivity and ratio lemmas (subduction_to_ridge_ratio, subduction_faster_than_ridge, wilson_cycle_lower_pos). No tactics or reductions are performed inside the structure itself.
why it matters
It supplies the inhabited certificate that downstream code (plateBoundaryDynamicsCert) uses to close the geology row of the Recognition Science velocity ladder. The construction anchors subduction and ridge speeds at phi^7 and phi^9 on the c_seismic = 1 scale, consistent with the eight-tick octave periodicity and the phi-ladder mass/velocity formulas used elsewhere in the framework. No open scaffolding remains inside this declaration.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.