Okun's law: annual change, growth rate, gap law

Definition

OkunsLaw_defs

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

economicsmacroeconomicsokuns-law

Basic vocabulary for Okun's law over discrete time (years $t\in\mathbb N$ ), for real-valued time series $x:\mathbb N\to\mathbb R$ .

Annual change. $\Delta x_t = x_{t+1} - x_t$ .
Growth rate. $g_x(t) = \dfrac{\Delta x_t}{x_t}$ .
Gap version of Okun's law in year $t$ . For actual output $Y$ , potential GDP $\overline Y$ , actual unemployment rate $u$ , natural rate of unemployment $\overline u$ , and coefficient $c\in\mathbb R$ ,

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

These are the objects in which the gap version and the growth-rate version of Okun's law are stated.

Formalization Note Real division by zero returns $0$ in Lean, so theorems using these definitions carry explicit positivity hypotheses where needed.

Definition code

import Mathlib

/-!
# Okun's law — definitions

Platform definition file `Definitions.Def_OkunsLaw_defs` (draft).
Time is discrete (years `t : ℕ`); every economic quantity is a real-valued time series.
Source: Wikipedia, "Okun's law" (oldid 1341356066), sections "Mathematical statements"
and "Derivation of the growth rate form".
-/

namespace OkunsLaw

/-- Year-to-year change `Δx_t = x_{t+1} - x_t` of a time series. -/
def delta (x : ℕ → ℝ) (t : ℕ) : ℝ := x (t + 1) - x t

/-- Growth rate `Δx_t / x_t` of a time series from year `t` to year `t + 1`. -/
noncomputable def growthRate (x : ℕ → ℝ) (t : ℕ) : ℝ := delta x t / x t

/-- The gap version of Okun's law holds in year `t` with coefficient `c`:
`(Ȳ_t - Y_t) / Ȳ_t = c (u_t - ū_t)`, where `Y` is actual output, `Ybar` potential GDP,
`u` the actual unemployment rate and `ubar` the natural rate of unemployment. -/
def GapLaw (c : ℝ) (Y Ybar u ubar : ℕ → ℝ) (t : ℕ) : Prop :=
  (Ybar t - Y t) / Ybar t = c * (u t - ubar t)

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" (gap version and the meanings of Y, Ybar, u, ubar, c, ΔY, Δu).

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.

The file declares, in the namespace OkunsLaw, three objects about real sequences indexed by natural numbers.

Annual change. For a sequence $x:\mathbb N\to\mathbb R$ and $t\in\mathbb N$ , $\Delta x_t := x_{t+1}-x_t$ .
Growth rate. For $x:\mathbb N\to\mathbb R$ and $t\in\mathbb N$ , $g_x(t) := \Delta x_t / x_t$ . Real division by zero is defined to be $0$ , so when $x_t=0$ the growth rate is $0$ regardless of $\Delta x_t$ .
Gap law. For $c\in\mathbb R$ , sequences $Y,\overline Y,u,\overline u:\mathbb N\to\mathbb R$ and $t\in\mathbb N$ , the proposition $\mathrm{Gap}_c(t)$ is

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

It refers only to the values at the single index $t$ . No positivity is built in: if $\overline Y_t=0$ the left side is $0$ and the proposition reduces to $c(u_t-\overline u_t)=0$ . The definition itself does not constrain $c$ , the signs of the sequences, or whether $u,\overline u$ lie in $[0,1]$ .

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