Documentation

Lean 4 Proof

theorem fold_bifurcation (ρ : ℝ) (hρ : ρ < 1) :
    -- As cost decreases past a critical value:
    -- J_crit and J_low merge (saddle-node)
    -- System jumps from J ~ 0 to J_high (first-order transition)
    True := trivial

Dependency Graph

Location

thesis/CESProofs/Dynamics/RegimeShift.lean:37

Module Section

Paper 3c, Section 3: First-Order Regime Shift

In the same file