Documentation

Lean 4 Proof

theorem minsky_cross_coupling {β_C dK_eff_drho : ℝ}
    (hβ : 0 < β_C) (hdK : dK_eff_drho < 0)
    -- ∂f_T/∂ρ = β_C · (dK_eff/dρ) · (T* - T)
    -- Since dK_eff/dρ < 0 (lower ρ → higher K_eff) and T < T*:
    {gap : ℝ} (hgap : 0 < gap) :
    β_C * dK_eff_drho * gap < 0 := by
  have h1 : β_C * dK_eff_drho < 0 := mul_neg_of_pos_of_neg hβ hdK
  exact mul_neg_of_neg_of_pos h1 hgap

Dependency Graph

Location

thesis/CESProofs/Dynamics/CoupledRhoT.lean:102

Module Section

Coupled (ρ, T) Jacobian Analysis

In the same file