Prove2Me

Okun's law: annual difference of Y/Y‾Y/\overline Y

Proved
OkunsLaw.ratio_annual_difference

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

economicsokuns-law

Let YY, Y‾\overline Y, uu, u‾\overline u be the series of actual output, potential GDP, actual unemployment rate and natural rate of unemployment, let c∈Rc\in\mathbb R, and let tt be a year with Y‾t>0\overline Y_t>0 and Y‾t+1>0\overline Y_{t+1}>0. Suppose the gap version of Okun's law

Y‾s−YsY‾s=c (us−u‾s)\frac{\overline Y_s - Y_s}{\overline Y_s} = c\,(u_s-\overline u_s)

holds for both s=ts=t and s=t+1s=t+1 (with the same cc). Then, writing Δxt=xt+1−xt\Delta x_t = x_{t+1}-x_t,

Δ ⁣(YY‾)t=Yt+ΔYtY‾t+ΔY‾t−YtY‾t=c (Δu‾t−Δut).\Delta\!\left(\frac{Y}{\overline Y}\right)_t = \frac{Y_t+\Delta Y_t}{\overline Y_t+\Delta\overline Y_t} - \frac{Y_t}{\overline Y_t} = c\,(\Delta\overline u_t - \Delta u_t).

This is the step "taking annual differences on both sides" in the derivation of the growth-rate form.

Preamble
import Mathlib
import Definitions.Def_OkunsLaw_defs
Formal statement
namespace OkunsLaw

theorem ratio_annual_difference (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)) :
    delta (fun s => Y s / Ybar s) t
        = (Y t + delta Y t) / (Ybar t + delta Ybar t) - Y t / Ybar t ∧
      delta (fun s => Y s / Ybar s) 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", second display ("Taking annual differences on both sides").
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).

Hypotheses.

  1. Y‾t>0\overline Y_t>0 and Y‾t+1>0\overline Y_{t+1}>0.
  2. Gapc(t)\mathrm{Gap}_c(t) and Gapc(t+1)\mathrm{Gap}_c(t+1) both hold, with the same cc.

Conclusion. Both of the following hold, where Δ(Y/Y‾)t\Delta(Y/\overline Y)_t means Yt+1Y‾t+1−YtY‾t\dfrac{Y_{t+1}}{\overline Y_{t+1}}-\dfrac{Y_t}{\overline Y_t}:

(i)Δ(Y/Y‾)t=Yt+ΔYtY‾t+ΔY‾t−YtY‾t,\text{(i)}\quad \Delta(Y/\overline Y)_t = \frac{Y_t+\Delta Y_t}{\overline Y_t+\Delta\overline Y_t}-\frac{Y_t}{\overline Y_t}, (ii)Δ(Y/Y‾)t=c (Δu‾t−Δut).\text{(ii)}\quad \Delta(Y/\overline Y)_t = c\,\big(\Delta\overline u_t-\Delta u_t\big).

Part (i) is an identity (since xt+Δxt=xt+1x_t+\Delta x_t=x_{t+1}) that holds without any hypothesis. Only indices tt and t+1t+1 are involved; nothing is assumed about other years, about the sign of YY, or about cc.

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