Only the zero orbit of $x_{t+1}=Mx_t$ is bounded iff all eigenvalues satisfy $|\mu|>1$

Proved

DSGE.bounded_orbits_zero_iff_eigenvalues_outside

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

difference-equationslinear-algebrastability

Let $M$ be a real $n \times n$ matrix. The following are equivalent:

the only bounded solution $(x_t)_{t \ge 0}$ , $x_t \in \mathbb R^n$ , of the linear recursion $x_{t+1} = M x_t$ is $x \equiv 0$ ;
every complex eigenvalue $\mu$ of $M$ (every complex root of its characteristic polynomial) satisfies

|\mu| > 1 .

This is the linear-algebra core of the Blanchard–Kahn approach to determinacy: in a model with no predetermined variables, the zero steady state is the unique bounded solution exactly when all eigenvalues of the forward transition matrix are explosive.

Formalization Note. Boundedness means a single constant $C$ bounds every coordinate $|x_t^{(j)}|$ for all $t$ . Eigenvalues are the complex roots of the characteristic polynomial of $M$ viewed as a complex matrix. The case $n = 0$ is included (both sides are trivially true).

Preamble

import Mathlib

Formal statement

namespace DSGE
theorem bounded_orbits_zero_iff_eigenvalues_outside (n : ℕ) (M : Matrix (Fin n) (Fin n) ℝ) :
    (∀ x : ℕ → Fin n → ℝ, (∀ t : ℕ, x (t + 1) = M.mulVec (x t)) →
        (∃ C : ℝ, ∀ t : ℕ, ∀ j : Fin n, |x t j| ≤ C) → ∀ t : ℕ, x t = 0) ↔
      ∀ μ : ℂ, (M.map (algebraMap ℝ ℂ)).charpoly.IsRoot μ → 1 < ‖μ‖ := by sorry
end DSGE

Source

Linear-algebra lemma behind O. Blanchard and C. Kahn, The Solution of Linear Difference Models under Rational Expectations, Econometrica 48 (1980) 1305-1311; as used in 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 every natural number $n$ and every real $n\times n$ matrix $M$ (rows and columns indexed by $\{0,\dots,n-1\}$ ), the following two statements are equivalent:

(A) For every sequence of vectors $x : \mathbb N \to \mathbb R^n$ : if $x_{t+1} = M x_t$ for all $t$ , and there is a real $C$ with $|x_t^{(j)}| \le C$ for all $t$ and all coordinates $j$ , then $x_t = 0$ for all $t$ .
(B) For every complex number $\mu$ : if $\mu$ is a root of the characteristic polynomial $\det(\lambda I - M_{\mathbb C})$ of the complexification $M_{\mathbb C}$ of $M$ (entries mapped into $\mathbb C$ ), then $|\mu| > 1$ .

For $n = 0$ both statements hold trivially ( $\mathbb R^0$ has only the zero vector; the characteristic polynomial is $1$ , which has no roots).

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

Only the zero orbit of xt+1=Mxtx_{t+1}=Mx_txt+1​=Mxt​ is bounded iff all eigenvalues satisfy ∣μ∣>1|\mu|>1∣μ∣>1

Only the zero orbit of $x_{t+1}=Mx_t$ is bounded iff all eigenvalues satisfy $|\mu|>1$