Both roots of $z^2 - Tz + D$ lie outside the unit circle iff $D>1$ and $|T|<1+D$

Proved

DSGE.quadratic_roots_outside_unit_disk_iff

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

linear-algebrapolynomialsstability

Let $T, D$ be real numbers with $D > 0$ . Then every complex root $z$ of $z^2 - T z + D$ satisfies $|z| > 1$ if and only if

D > 1 \quad\text{and}\quad |T| < 1 + D .

This is the two-dimensional Schur–Cohn (Jury) stability test, applied in the outward direction. Applied to the trace $T$ and determinant $D$ of the transition matrix $M$ of the forward form, it turns "both eigenvalues of $M$ are explosive" into explicit parameter inequalities.

Formalization Note. The hypothesis $D > 0$ is needed: e.g. $T = 0$ , $D = -4$ has roots $\pm 2$ outside the unit circle while $D > 1$ fails. In the application, $D = \det M > 0$ .

Preamble

import Mathlib

Formal statement

namespace DSGE
theorem quadratic_roots_outside_unit_disk_iff (T D : ℝ) (hD : 0 < D) :
    (∀ z : ℂ, z ^ 2 - (T : ℂ) * z + (D : ℂ) = 0 → 1 < ‖z‖) ↔ 1 < D ∧ |T| < 1 + D := by sorry
end DSGE

Source

Standard Schur–Cohn / Jury criterion for real quadratics, as used in the determinacy analysis of 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 $T$ and $D$ with $D > 0$ : the statement "for every complex number $z$ , if $z^2 - T z + D = 0$ then $|z| > 1$ " holds if and only if both $D > 1$ and $|T| < 1 + D$ . Here $T, D$ are viewed as complex numbers in the polynomial, $|z|$ is the complex modulus, and $|T|$ the real absolute value. Repeated roots are covered (the condition quantifies over all roots, not over distinct ones). The case $D \le 0$ is excluded by hypothesis.

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

Both roots of z2−Tz+Dz^2 - Tz + Dz2−Tz+D lie outside the unit circle iff D>1D>1D>1 and ∣T∣<1+D|T|<1+D∣T∣<1+D

Both roots of $z^2 - Tz + D$ lie outside the unit circle iff $D>1$ and $|T|<1+D$