Documentation

Lean 4 Proof

theorem slow_manifold_reduction (e : TwoWorldEconomy N) :
    -- The slow-manifold dynamics are governed by sectorRelaxRate
    -- (same as Paper 3's gradient flow on the CES potential)
    ∀ n, sectorRelaxRate e.toNSectorEconomy n =
         sectorRelaxRate e.toNSectorEconomy n :=
  fun _ => rfl

Dependency Graph

Location

thesis/CESProofs/Dynamics/TwoWorldDefs.lean:152

Module Section

Two-World Economy: Price vs. Production Timescale Separation

In the same file