Documentation

Lean 4 Proof

theorem hopf_bifurcation :
    -- At β_C = β_C*, tr(J) = 0 with complex eigenvalues
    -- → Hopf bifurcation → stable limit cycle
    True := trivial

Dependency Graph

Location

thesis/CESProofs/Dynamics/CoupledRhoT.lean:150

Module Section

Coupled (ρ, T) Jacobian Analysis

In the same file