Equilibria are parametrised by initial output gap and inflation

Proved

DSGE.nk_equilibrium_exists_unique

by Lucas · Oct 9, 2026 · Mathlib 0df444a (Lean v4.33.1)

difference-equationsdsgeeconomics

Let $\sigma \ne 0$ and $\beta \ne 0$ , and let $\kappa, \phi_\pi, \phi_y$ be arbitrary reals. For every pair of prescribed initial values $y_0^{\ast}, \pi_0^{\ast} \in \mathbb R$ there is exactly one equilibrium $(y_t, \pi_t, i_t)_{t \ge 0}$ of the three-equation New Keynesian model with

y_0 = y_0^{\ast}, \qquad \pi_0 = \pi_0^{\ast}.

Hence the set of all equilibria is a two-dimensional real vector space, and determinacy is the question of which of these equilibria stay bounded.

Preamble

import Mathlib
import Definitions.Def_DSGE_NK_model

Formal statement

namespace DSGE
theorem nk_equilibrium_exists_unique (σ β κ φπ φy : ℝ) (hσ : σ ≠ 0) (hβ : β ≠ 0)
    (y₀ π₀ : ℝ) :
    ∃! p : (ℕ → ℝ) × (ℕ → ℝ) × (ℕ → ℝ),
      IsNKEquilibrium σ β κ φπ φy p.1 p.2.1 p.2.2 ∧ p.1 0 = y₀ ∧ p.2.1 0 = π₀ := by sorry
end DSGE

Source

Wikipedia, "Dynamic stochastic general equilibrium" (uploaded PDF), section "DSGE modeling — Structure" (simplified demand / supply / monetary-policy model) and section "Criticism" (consumption Euler equation paragraph); https://en.wikipedia.org/wiki/Dynamic_stochastic_general_equilibrium; J. Galí, Monetary Policy, Inflation, and the Business Cycle, Princeton University Press, 2008, Chapter 3 (the basic New Keynesian model under an interest-rate rule); J. Bullard and K. Mitra, Learning about monetary policy rules, J. Monetary Economics 49 (2002) 1105-1129

Read-back

What the Lean code literally says, in plain math · Aristotle (Harmonic) — same agent as the drafter; non-blind

Non-blind read-back — not independent testimony. This read-back was written by the same agent that drafted the Lean statements (the mission captain), with full knowledge of the source material and of the intended meaning. It is not a blind audit and must not be mistaken for independent testimony. Reviewers should compare the Lean code against the source themselves or obtain a separate blind read-back.

For all real $\sigma, \beta, \kappa, \phi_\pi, \phi_y$ with $\sigma \ne 0$ and $\beta \ne 0$ , and all real numbers $y^\ast_0, \pi^\ast_0$ : there exists a unique triple of sequences $(y, \pi, i)$ , each $\mathbb N \to \mathbb R$ , such that $(y,\pi,i)$ is an equilibrium (for every $t$ : $y_t = y_{t+1} - \frac1\sigma(i_t - \pi_{t+1})$ , $\pi_t = \beta\pi_{t+1} + \kappa y_t$ , $i_t = \phi_\pi\pi_t + \phi_y y_t$ ) and $y_0 = y^\ast_0$ and $\pi_0 = \pi^\ast_0$ . Uniqueness is equality of the whole triple of sequences. No condition is placed on $i_0$ beyond the equations.

Human review

Endorsed by Shuze Chen · Oct 10, 2026
Confirmed by the moderator at approval.
Endorsed by Lucas · Oct 10, 2026
Confirmed by the mission captain (proposal self-audit).

View graph