Okun's law: exact growth-rate identity

Proved

OkunsLaw.exact_growth_identity

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

economicsokuns-law

Let $Y$ , $\overline Y$ , $u$ , $\overline u$ be the series of actual output, potential GDP, actual unemployment rate and natural rate of unemployment, let $c\in\mathbb R$ , and let $t$ be a year with $Y_t>0$ , $\overline Y_t>0$ and $\overline Y_{t+1}>0$ . If the gap version of Okun's law holds with coefficient $c$ in both years $t$ and $t+1$ , then, writing $\Delta x_t = x_{t+1}-x_t$ ,

\frac{\Delta Y_t}{Y_t} - \frac{\Delta\overline Y_t}{\overline Y_t} = c\,(\Delta\overline u_t-\Delta u_t)\cdot\frac{\overline Y_t+\Delta\overline Y_t}{Y_t}.

This is the exact form of the step "multiplying the left hand side by $(\overline Y+\Delta\overline Y)/Y$ , which is approximately equal to 1": the source then drops the factor $(\overline Y_t+\Delta\overline Y_t)/Y_t$ , obtaining $\frac{\Delta Y}{Y} \approx \frac{\Delta\overline Y}{\overline Y} + c(\Delta\overline u-\Delta u)$ .

Preamble

import Mathlib
import Definitions.Def_OkunsLaw_defs

Formal statement

namespace OkunsLaw

theorem exact_growth_identity (c : ℝ) (Y Ybar u ubar : ℕ → ℝ) (t : ℕ)
    (hY : 0 < Y t) (hYbar₀ : 0 < Ybar t) (hYbar₁ : 0 < Ybar (t + 1))
    (h₀ : GapLaw c Y Ybar u ubar t) (h₁ : GapLaw c Y Ybar u ubar (t + 1)) :
    growthRate Y t - growthRate Ybar t
      = c * (delta ubar t - delta u t) * ((Ybar t + delta Ybar t) / Y t) := by
  sorry

end OkunsLaw

Source

Wikipedia, "Okun's law", revision oldid=1341356066 (https://en.wikipedia.org/w/index.php?title=Okun%27s_law&oldid=1341356066), section "Derivation of the growth rate form", fourth and fifth displays ("Multiplying the left hand side by (Ybar+ΔYbar)/Y").

Read-back

What the Lean code literally says, in plain math · Aristotle (Harmonic) — same agent that drafted the statements (non-blind)

Non-blind read-back — not independent testimony. This read-back was written by the same agent that drafted the Lean statements, at the account owner's explicit request. It was not produced by a blind, independent auditor, and the author knew the intended meaning when writing it. Reviewers should not treat it as independent evidence of faithfulness.

Throughout, $c\in\mathbb R$ is a real number; $Y,\overline Y,u,\overline u:\mathbb N\to\mathbb R$ are arbitrary real sequences (indexed by years $t\in\mathbb N$ ), with no sign, boundedness or other assumptions beyond those listed; and $t\in\mathbb N$ is an arbitrary year. $\Delta x_t$ denotes $x_{t+1}-x_t$ , and $\mathrm{Gap}_c(t)$ denotes the proposition

\frac{\overline Y_t - Y_t}{\overline Y_t} = c\,(u_t-\overline u_t)

(with the convention that a real number divided by $0$ is $0$ ). The growth rate of a sequence $x$ in year $t$ is $\Delta x_t/x_t$ .

Hypotheses.

$Y_t>0$ , $\overline Y_t>0$ and $\overline Y_{t+1}>0$ .
$\mathrm{Gap}_c(t)$ and $\mathrm{Gap}_c(t+1)$ both hold, with the same $c$ .

Conclusion. An exact equality (no approximation):

\frac{\Delta Y_t}{Y_t}-\frac{\Delta\overline Y_t}{\overline Y_t} = c\,\big(\Delta\overline u_t-\Delta u_t\big)\cdot\frac{\overline Y_t+\Delta\overline Y_t}{Y_t}.

Nothing is assumed about $\Delta\overline u_t$ (the natural rate may change) or about the size of $\Delta\overline Y_t/\overline Y_t$ . Only indices $t$ and $t+1$ are involved.

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