Prove2Me

Okun's gap law as Y/Y‾−1=c(u‾−u)Y/\overline Y - 1 = c(\overline u - u)

Proved
OkunsLaw.gapLaw_iff_ratio

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

economicsokuns-law

Let YtY_t be actual output, Y‾t\overline Y_t potential GDP, utu_t the actual unemployment rate and u‾t\overline u_t the natural rate of unemployment in year tt, and let c∈Rc\in\mathbb R. If Y‾t>0\overline Y_t>0, then the gap version of Okun's law

Y‾t−YtY‾t=c (ut−u‾t)\frac{\overline Y_t - Y_t}{\overline Y_t} = c\,(u_t-\overline u_t)

holds if and only if

YtY‾t−1=c (u‾t−ut).\frac{Y_t}{\overline Y_t} - 1 = c\,(\overline u_t - u_t).

This is the first rewriting in the derivation of the growth-rate form of Okun's law.

Preamble
import Mathlib
import Definitions.Def_OkunsLaw_defs
Formal statement
namespace OkunsLaw

theorem gapLaw_iff_ratio (c : ℝ) (Y Ybar u ubar : ℕ → ℝ) (t : ℕ) (hYbar : 0 < Ybar t) :
    GapLaw c Y Ybar u ubar t ↔ Y t / Ybar t - 1 = c * (ubar t - 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", first display (lines 1-2).
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∈Rc\in\mathbb R is a real number; Y,Y‾,u,u‾:N→RY,\overline Y,u,\overline u:\mathbb N\to\mathbb R are arbitrary real sequences (indexed by years t∈Nt\in\mathbb N), with no sign, boundedness or other assumptions beyond those listed; and t∈Nt\in\mathbb N is an arbitrary year. Δxt\Delta x_t denotes xt+1−xtx_{t+1}-x_t, and Gapc(t)\mathrm{Gap}_c(t) denotes the proposition

Y‾t−YtY‾t=c (ut−u‾t)\frac{\overline Y_t - Y_t}{\overline Y_t} = c\,(u_t-\overline u_t)

(with the convention that a real number divided by 00 is 00).

Statement. Assume Y‾t>0\overline Y_t>0. Then

Gapc(t)  ⟺  YtY‾t−1=c (u‾t−ut).\mathrm{Gap}_c(t)\iff \frac{Y_t}{\overline Y_t}-1 = c\,(\overline u_t-u_t).

Only the values at the single index tt are involved. YtY_t, utu_t, u‾t\overline u_t and cc may be any reals (including negative ones). The only hypothesis is Y‾t>0\overline Y_t>0; it rules out the degenerate case of division by zero.

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