Documentation

Lean 4 Proof

theorem oscillation_vs_gdp :
    -- Oscillation energy L measures cycle amplitude, not GDP level
    -- Welfare = level - friction cost
    -- Instability = amplitude of oscillation
    True := trivial

Dependency Graph

Location

thesis/CESProofs/Dynamics/PhillipsCycles.lean:178

Module Section

Results 63-69: Phillips Curve, Endogenous Cycles, and Oscillation Energy

In the same file