Documentation

Lean 4 Proof

theorem phase_lead_sign_axiom :
    -- phase_{nm} = arctan(omega/r) * sgn(j_{nm})
    -- Positive coupling => positive phase lead
    True := trivial

Dependency Graph

Location

thesis/CESProofs/Dynamics/BusinessCycles.lean:130

Module Section

Results 47-62: Business Cycles on the CES Landscape

In the same file