Okun's law: common-denominator form

Proved

OkunsLaw.common_denominator_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\in\mathbb R$ , and let $t$ be a year with $\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{\overline Y_t\,\Delta Y_t - Y_t\,\Delta\overline Y_t}{\overline Y_t\,(\overline Y_t+\Delta\overline Y_t)} = c\,(\Delta\overline u_t-\Delta u_t).

This is the step "putting both numerators over a common denominator" in the derivation of the growth-rate form.

Preamble

import Mathlib
import Definitions.Def_OkunsLaw_defs

Formal statement

namespace OkunsLaw

theorem common_denominator_form (c : ℝ) (Y Ybar u ubar : ℕ → ℝ) (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)) :
    (Ybar t * delta Y t - Y t * delta Ybar t) / (Ybar t * (Ybar t + delta Ybar t))
      = c * (delta ubar t - delta u 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", third display ("Putting both numerators over a common denominator").

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$ ).

Hypotheses.

$\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.

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

The denominator equals $\overline Y_t\,\overline Y_{t+1}$ , which is positive under hypothesis 1. Only indices $t$ and $t+1$ are involved; $Y_t$ may have any sign.

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