Paper
A Simplified Stability Criterion for Linear Discrete Systems, 1962. Proceedings of the IRE 50(6), pp. 1493–1500. Read a later research application, Lemma 2.
Connection to the paper
The original full text could not be retrieved. The quadratic conditions were checked against Khalsaraei, Shokri and Ramos, “Efficient Numerical Solutions to a SIR Epidemic Model” (2022), Lemma 2, using A = −a and B = b. Our proof treats roots directly; it is not a transcription of the general Jury determinant test.
The result
For the real-coefficient polynomial z² + az + b, the three strict Jury inequalities are sufficient to place every complex root strictly inside the unit circle.
|b| < 1, 1 + a + b > 0, 1 − a + b > 0 z² + az + b = 0 ⇒ |z| < 1
Proof in plain English
- Handle real roots. The signs at 1 and −1 rule out roots outside the interval.
- Handle nonreal roots. The imaginary equation forces 2 Re(z) + a = 0; the real equation gives |z|² = b.
- Read the modulus. The strict bound on b puts both cases in the open disk.
Scope & assumptions
5 checked theorems. Real-root bounds, real/imaginary root equations, the modulus of nonreal roots, and sufficiency of the degree-two test. Necessity and the higher-order Jury table are not formalized. No claim about a particular simulated system follows without connecting its characteristic polynomial.
Real a and b, any complex root z, and strict coefficient inequalities. Repeated and real roots are included. The conclusion uses the standard complex norm. The |b| < 1 assumption includes b < 1; the lower bound is compatible with the other two inequalities.
Notation in Lean
| Meaning | Lean |
|---|---|
| Real-root interval | real_root_inside |
| Complex root equations | root_parts |
| Nonreal modulus | nonreal_modulus |
| Stability test | quadratic_sufficient |
Prior work
No matching named formalization was located in the bounded search of two Mathlib revisions and indexed web results on 2026-09-10. Related library ingredients already exist. First-formalization status is unconfirmed; this does not establish priority.
Read the search recordLean proof
import Mathlib.Analysis.Complex.Basic
import Mathlib.Tactic.Ring
import Mathlib.Tactic.Linarith
import Mathlib.Tactic.NormNum
import Mathlib.Tactic.Positivity
/-! Jury (1962): sufficiency of the second-order unit-disk test.
All complex roots of z² + a z + b are handled, including repeated roots.
This is not a formalization of the higher-order Jury table or necessity. -/
namespace PaperToLean.Jury
noncomputable section
theorem real_root_upper (a b x : ℝ) (hb : b < 1) (hp : 0 < 1 + a + b)
(hx : x ^ 2 + a * x + b = 0) : x < 1 := by
by_contra h
have hx1 : 1 ≤ x := le_of_not_gt h
have hy : 1 < -a - x := by
by_contra hy
have hfactor : 0 ≤ 1 + a + x := by linarith
have hprod := mul_nonneg (sub_nonneg.mpr hx1) hfactor
nlinarith
have hprod := mul_nonneg (sub_nonneg.mpr hx1) (show 0 ≤ -a - x by linarith)
nlinarith
theorem real_root_inside (a b x : ℝ) (hb : b < 1)
(hp : 0 < 1 + a + b) (hm : 0 < 1 - a + b)
(hx : x ^ 2 + a * x + b = 0) : -1 < x ∧ x < 1 := by
have hu := real_root_upper a b x hb hp hx
have hl := real_root_upper (-a) b (-x) hb (by linarith) (by nlinarith)
exact ⟨by linarith, hu⟩
theorem root_parts (a b : ℝ) (z : ℂ) (hz : z ^ 2 + (a : ℂ) * z + b = 0) :
z.re ^ 2 - z.im ^ 2 + a * z.re + b = 0 ∧ z.im * (2 * z.re + a) = 0 := by
have hr := congrArg Complex.re hz
have hi := congrArg Complex.im hz
simp [pow_two] at hr hi
constructor <;> nlinarith
theorem nonreal_modulus (a b : ℝ) (z : ℂ)
(hz : z ^ 2 + (a : ℂ) * z + b = 0) (hi : z.im ≠ 0) : Complex.normSq z = b := by
obtain ⟨hr, him⟩ := root_parts a b z hz
have ha := (mul_eq_zero.mp him).resolve_left hi
rw [Complex.normSq_apply]
nlinarith [congrArg (fun t : ℝ => t * z.re) ha]
/-- The usual three strict inequalities put every root in the open disk. -/
theorem quadratic_sufficient (a b : ℝ) (hb : |b| < 1)
(hp : 0 < 1 + a + b) (hm : 0 < 1 - a + b) (z : ℂ)
(hz : z ^ 2 + (a : ℂ) * z + b = 0) : ‖z‖ < 1 := by
have hb1 : b < 1 := (abs_lt.mp hb).2
have hnorm : Complex.normSq z < 1 := by
by_cases hi : z.im = 0
· have hr := (root_parts a b z hz).1
rw [hi] at hr
have h := real_root_inside a b z.re hb1 hp hm (by nlinarith)
rw [Complex.normSq_apply, hi]
nlinarith [mul_pos (show 0 < 1 - z.re by linarith) (show 0 < 1 + z.re by linarith)]
· rw [nonreal_modulus a b z hz hi]
exact hb1
rw [Complex.normSq_eq_norm_sq] at hnorm
nlinarith [norm_nonneg z]
#print axioms real_root_upper
#print axioms real_root_inside
#print axioms root_parts
#print axioms nonreal_modulus
#print axioms quadratic_sufficient
end
end PaperToLean.Jury
Inspect the verification record
Every listed theorem is audited individually. These proofs use only propext, Classical.choice, Quot.sound. No custom axioms, sorry placeholders, or native_decide proofs.
Lean 4.33.1
Dependencies: Mathlib 4.33.1 (see bundled lake-manifest.json)
File: Jury.lean
SHA-256: 1b030b7fc9f699726cc0146ff4229890b695948e3fd64447bdbed62c91e3e57a
Result: passed
'PaperToLean.Jury.real_root_upper' depends on axioms: [propext, Classical.choice, Quot.sound]
'PaperToLean.Jury.real_root_inside' depends on axioms: [propext, Classical.choice, Quot.sound]
'PaperToLean.Jury.root_parts' depends on axioms: [propext, Classical.choice, Quot.sound]
'PaperToLean.Jury.nonreal_modulus' depends on axioms: [propext, Classical.choice, Quot.sound]
'PaperToLean.Jury.quadratic_sufficient' depends on axioms: [propext, Classical.choice, Quot.sound]
SHA-256: 1b030b7fc9f699726cc0146ff4229890b695948e3fd64447bdbed62c91e3e57a
Run it
Install Lean with elan and Git. Download the project ZIP, extract it, and run these commands in that folder. The first command downloads the pinned Mathlib dependencies.
python3 prepare.py
lake env lean -DwarningAsError=true Jury.lean