Documentation

Lean 4 Proof

theorem hopf_bifurcation_3d :
    -- When the trace crosses zero, a pair of complex eigenvalues
    -- crosses the imaginary axis -> Hopf bifurcation -> limit cycle
    -- Projection onto (rho, T) recovers Paper 3 results
    True := trivial

Dependency Graph

Location

thesis/CESProofs/Dynamics/CoupledRhoT.lean:240

Module Section

## Coupled (ρ, T, J) System (merged from CoupledSystem.lean)

In the same file