Documentation

Lean 4 Proof

theorem timescale_exponent (τ₀ T Tstar : ℝ) :
    adjustmentTimescale τ₀ T Tstar = τ₀ * (1 - T / Tstar)⁻¹ := by
  simp [adjustmentTimescale, div_eq_mul_inv]

Dependency Graph

Location

thesis/CESProofs/CurvatureRoles/PhaseTransition.lean:167

Module Section

Phase Transition at T* (Gap #8)

In the same file