A glut of one good is balanced by a shortage of another

Proved

SaysLaw.glut_balanced_by_shortage

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

economicsgeneral-equilibriummacroeconomicssays-law

Throughout, $\iota$ is a finite set of agents and $G$ a finite set of goods; $p=(p_g)_{g\in G}$ is a real price vector; $s_i=(s_{i,g})_g$ and $d_i=(d_{i,g})_g$ are real vectors giving the quantities agent $i$ brings to market (supplies) and plans to buy (demands); $\langle p,x\rangle=\sum_{g\in G}p_g x_g$ is the market value of a bundle $x$ ; and $z_g=\sum_{i\in\iota}(d_{i,g}-s_{i,g})$ is the aggregate excess demand for good $g$ .

Assume all prices are strictly positive, $p_g>0$ for every $g$ , and every agent obeys Say's budget principle $\langle p,d_i\rangle=\langle p,s_i\rangle$ . If some good $g_0$ is in excess supply, $z_{g_0}<0$ , then some other good is in excess demand:

\exists\, g\neq g_0\ \text{ with }\ z_g>0 .

This is Say's claim that "the superabundance of goods of one description arises from the deficiency of goods of another description".

Preamble

import Mathlib
import Definitions.Def_SaysLaw_Model

Formal statement

namespace SaysLaw

theorem glut_balanced_by_shortage {ι G : Type*} [Fintype ι] [Fintype G]
    (p : G → ℝ) (hp : ∀ g, 0 < p g) (supply demand : ι → G → ℝ)
    (hsay : SaysBudget p supply demand) (g₀ : G)
    (hglut : excessDemand supply demand g₀ < 0) :
    ∃ g, g ≠ g₀ ∧ 0 < excessDemand supply demand g := by sorry

end SaysLaw

Source

Wikipedia, "Say's law" (PDF export supplied with the request); https://en.wikipedia.org/wiki/Say%27s_law

Read-back

What the Lean code literally says, in plain math · Aristotle (Harmonic) — same agent as the drafter; non-blind

Disclosure — NON-BLIND read-back. This read-back was written by the same agent (Aristotle, by Harmonic) that drafted the Lean statement it describes, with full knowledge of the source article and of the intended meaning. It is not independent, blind testimony and must not be mistaken for one. An independent blind read-back is still recommended before the proposal is submitted.

Let $\iota$ and $G$ be arbitrary finite types, $p:G\to\mathbb R$ with $p_g>0$ for every $g\in G$ , and $s,d:\iota\to G\to\mathbb R$ arbitrary. Write $z_g=\sum_{i\in\iota}(d_{i,g}-s_{i,g})$ . Assume (i) for every agent $i$ , $\sum_g p_g d_{i,g}=\sum_g p_g s_{i,g}$ , and (ii) a specified good $g_0\in G$ has $z_{g_0}<0$ . Then there exists a good $g\in G$ with $g\neq g_0$ and $z_g>0$ (strictly). Hypothesis (ii) forces $G$ to be nonempty; if $\iota$ is empty then $z\equiv 0$ , so (ii) cannot hold and the statement is vacuous for that case. Nothing is said about how many goods are in excess demand or about the size of $z_g$ .

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