Taylor principle: determinacy of the New Keynesian model iff $\kappa(\phi_\pi-1)+(1-\beta)\phi_y>0$

Proved

DSGE.taylor_principle_determinacy

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

difference-equationsdsgeeconomicsmonetary-policynew-keynesian

Consider the deterministic three-equation New Keynesian model (demand, supply and Taylor-rule equations, see the definition file) with parameters

\sigma > 0, \qquad 0 < \beta < 1, \qquad \kappa > 0, \qquad \phi_\pi \ge 0, \qquad \phi_y \ge 0 .

The model is determinate — the zero steady state is its only equilibrium in which output gap, inflation and the interest rate all stay bounded — if and only if

\kappa\,(\phi_\pi - 1) + (1 - \beta)\,\phi_y > 0 .

This is the Taylor principle in the form of Bullard and Mitra (2002) and Galí (2008, Ch. 3): the central bank must respond to inflation sufficiently strongly (roughly, raise the nominal rate more than one-for-one with inflation) for the model's equilibrium to be pinned down. It formalises the source's description of the simplified DSGE model as a complete, jointly determined system of output, inflation and the nominal interest rate.

Preamble

import Mathlib
import Definitions.Def_DSGE_NK_model

Formal statement

namespace DSGE
theorem taylor_principle_determinacy (σ β κ φπ φy : ℝ)
    (hσ : 0 < σ) (hβ0 : 0 < β) (hβ1 : β < 1) (hκ : 0 < κ)
    (hφπ : 0 ≤ φπ) (hφy : 0 ≤ φy) :
    IsDeterminate σ β κ φπ φy ↔ 0 < κ * (φπ - 1) + (1 - β) * φy := 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; determinacy condition from 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 numbers $\sigma, \beta, \kappa, \phi_\pi, \phi_y$ with $\sigma > 0$ , $0 < \beta < 1$ , $\kappa > 0$ , $\phi_\pi \ge 0$ and $\phi_y \ge 0$ , the following are equivalent:

(A) Determinacy: for all sequences $y, \pi, i : \mathbb N \to \mathbb R$ such that for every $t$

y_t = y_{t+1} - \frac1\sigma(i_t - \pi_{t+1}),\qquad \pi_t = \beta\pi_{t+1} + \kappa y_t,\qquad i_t = \phi_\pi\pi_t + \phi_y y_t,

and such that each of $y$ , $\pi$ , $i$ is bounded (some real $C$ with $|x_t| \le C$ for all $t$ , a separate constant allowed for each sequence), one has $y_t = \pi_t = i_t = 0$ for every $t$ .

(B) $\kappa(\phi_\pi - 1) + (1-\beta)\phi_y > 0$ (strict inequality).

The boundary case $\kappa(\phi_\pi - 1) + (1-\beta)\phi_y = 0$ is classified as not determinate. All parameter hypotheses are satisfiable (e.g. $\sigma = 1$ , $\beta = 0.99$ , $\kappa = 0.1$ , $\phi_\pi = 1.5$ , $\phi_y = 0.5$ ).

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

Taylor principle: determinacy of the New Keynesian model iff κ(ϕπ−1)+(1−β)ϕy>0\kappa(\phi_\pi-1)+(1-\beta)\phi_y>0κ(ϕπ​−1)+(1−β)ϕy​>0

Taylor principle: determinacy of the New Keynesian model iff $\kappa(\phi_\pi-1)+(1-\beta)\phi_y>0$