Okun's law: growth-rate form $\Delta Y/Y = k - c\,\Delta u$ with exact remainder

Proved

OkunsLaw.growth_rate_form

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,k\in\mathbb R$ , and let $t$ be a year with $Y_t>0$ , $\overline Y_t>0$ and $\overline Y_{t+1}>0$ . Write $\Delta x_t = x_{t+1}-x_t$ . Assume

the gap version of Okun's law $\dfrac{\overline Y_s - Y_s}{\overline Y_s} = c\,(u_s-\overline u_s)$ holds for $s=t$ and $s=t+1$ ;
the natural rate of unemployment does not change: $\Delta\overline u_t = 0$ ;
full-employment output grows at rate $k$ : $\Delta\overline Y_t/\overline Y_t = k$ .

Then

\frac{\Delta Y_t}{Y_t} = k - c\,\Delta u_t - c\,\Delta u_t\left(\frac{\overline Y_t+\Delta\overline Y_t}{Y_t}-1\right).

This is the growth-rate (difference) form of Okun's law, $\frac{\Delta Y}{Y}\approx k - c\,\Delta u$ , with the approximation made exact: the last term is exactly the error committed by replacing the factor $(\overline Y_t+\Delta\overline Y_t)/Y_t$ with $1$ .

Formalization Note The source's approximations $\Delta\overline u\approx 0$ and $\Delta\overline Y/\overline Y\approx k$ are taken as exact hypotheses 2 and 3; the approximation $(\overline Y+\Delta\overline Y)/Y\approx 1$ is replaced by the explicit remainder term.

Preamble

import Mathlib
import Definitions.Def_OkunsLaw_defs

Formal statement

namespace OkunsLaw

theorem growth_rate_form (c k : ℝ) (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))
    (hnatural : delta ubar t = 0) (hpotential : growthRate Ybar t = k) :
    growthRate Y t
      = k - c * delta u t - c * delta u t * ((Ybar t + delta Ybar t) / Y t - 1) := 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 "Mathematical statements" (difference version ΔY/Y = k − cΔu) and section "Derivation of the growth rate form", final display.

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$ ). Additionally $k\in\mathbb R$ is an arbitrary real number.

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$ .
$\Delta\overline u_t = 0$ , i.e. $\overline u_{t+1}=\overline u_t$ .
$\Delta\overline Y_t/\overline Y_t = k$ , i.e. $k$ is exactly the growth rate of $\overline Y$ from $t$ to $t+1$ (not an average over several years).

Conclusion. An exact equality:

\frac{\Delta Y_t}{Y_t} = k - c\,\Delta u_t - c\,\Delta u_t\left(\frac{\overline Y_t+\Delta\overline Y_t}{Y_t}-1\right).

There is no approximation and no bound on the last term; the statement is the identity above. All hypotheses concern only indices $t$ and $t+1$ . Since $\overline Y_t+\Delta\overline Y_t=\overline Y_{t+1}$ , the bracket equals $\overline Y_{t+1}/Y_t-1$ . The hypotheses are jointly satisfiable (e.g. $Y\equiv\overline Y\equiv 1$ , $u\equiv\overline u\equiv 0$ , $k=0$ ).

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

Okun's law: growth-rate form ΔY/Y=k−c Δu\Delta Y/Y = k - c\,\Delta uΔY/Y=k−cΔu with exact remainder

Okun's law: growth-rate form $\Delta Y/Y = k - c\,\Delta u$ with exact remainder