def reducedOrderParam (T Tstar : ℝ) : ℝ := max 0 (1 - T / Tstar)

theorem keff_at_critical (J : ℕ) (ρ Tstar : ℝ) (hTs : 0 < Tstar) :
    effectiveCurvatureKeff J ρ Tstar Tstar = 0 :=
  effectiveCurvatureKeff_above_critical J ρ Tstar Tstar hTs (le_refl _)

theorem keff_continuous (J : ℕ) (ρ Tstar : ℝ) :
    Continuous (fun T => effectiveCurvatureKeff J ρ T Tstar) := by
  unfold effectiveCurvatureKeff
  exact continuous_const.mul
    (continuous_const.max (continuous_const.sub (continuous_id.div_const _)))

theorem susceptibility_exponent_one (sigma0_sq T Tstar : ℝ)
    (hTs : 0 < Tstar) (hT : T < Tstar) :
    varianceAtFriction sigma0_sq T Tstar =
      sigma0_sq * (1 - T / Tstar)⁻¹ := by
  rw [intensification_rate (by linarith) (by linarith)]
  rw [one_div]

def landauPotential (t m : ℝ) : ℝ := t * m + m ^ 2 / 2

theorem universality {J₁ J₂ : ℕ} {ρ₁ ρ₂ : ℝ}
    {T₁ Tstar₁ T₂ Tstar₂ : ℝ}
    (hK1 : curvatureK J₁ ρ₁ ≠ 0)
    (hK2 : curvatureK J₂ ρ₂ ≠ 0)
    (hratio : T₁ / Tstar₁ = T₂ / Tstar₂) :
    effectiveCurvatureKeff J₁ ρ₁ T₁ Tstar₁ / curvatureK J₁ ρ₁ =
    effectiveCurvatureKeff J₂ ρ₂ T₂ Tstar₂ / curvatureK J₂ ρ₂ := by
  rw [keff_reduced_universal J₁ ρ₁ T₁ Tstar₁ hK1,
      keff_reduced_universal J₂ ρ₂ T₂ Tstar₂ hK2]
  unfold reducedOrderParam
  rw [hratio]