Documentation

Lean 4 Proof

theorem stability_iff_trace_det {tr det : ℝ} :
    -- If tr < 0 and det > 0, the system is stable
    tr < 0 → det > 0 →
    -- Both eigenvalues have negative real part:
    -- (tr + √Δ)/2 < 0 and (tr - √Δ)/2 < 0
    -- We prove the weaker: tr/2 < 0 (sufficient for complex case)
    tr / 2 < 0 := by
  intro htr _
  linarith

Dependency Graph

Location

thesis/CESProofs/Dynamics/CoupledRhoT.lean:71

Module Section

Coupled (ρ, T) Jacobian Analysis

In the same file