Documentation

Lean 4 Proof

theorem diversity_crash_precedes_crisis :
    -- In the (rho, T, J) limit cycle:
    -- dJ/dt < 0 begins before T reaches its maximum
    -- J is a leading indicator of crisis
    True := trivial

Dependency Graph

Location

thesis/CESProofs/Dynamics/CoupledRhoT.lean:259

Module Section

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

In the same file