wilson_cycle_lower_pos
plain-language theorem explainer
The theorem establishes positivity of the dimensionless Wilson cycle lower bound 45 phi to the ninth. Researchers applying Recognition Science to geology and plate tectonics would cite it to confirm the phi-ladder timescale starts above zero. The proof is a short tactic sequence that unfolds the definition then invokes power positivity followed by the positivity tactic.
Claim. The lower bound on the dimensionless Wilson cycle period satisfies $0 < 45 phi^9$.
background
The module develops plate boundary velocities from the phi-ladder. Subduction speed equals seismic velocity over phi to the seventh, ridge spreading equals seismic velocity over phi to the ninth, and their ratio equals phi squared. The Wilson cycle lower bound is placed at 45 times phi to the ninth in dimensionless units, with the full period interval given as (phi^9, phi^10) times 45 Myr, approximately 137 to 222 Myr before geologic uncertainty adjustments.
proof idea
Unfolds wilson_cycle_lower_dimensionless to expose 45 times phi to the ninth. Asserts 0 less than phi to the ninth via the power positivity lemma applied to the known positivity of phi. Closes with the positivity tactic.
why it matters
Supplies the wilson_pos field inside the master certificate plateBoundaryDynamicsCert. It realizes the lower end of the Wilson cycle interval on the phi-ladder as stated in the module documentation for the geology row. The exponent 9 aligns with the self-similar scaling structure of the eight-tick octave in the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.