With money hoarding, a general glut is consistent with every agent's budget

Proved

SaysLaw.hoarding_permits_general_glut

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$ . Each agent holds money $m_i$ initially.

Assume there is at least one agent. For any prices $p$ , any supplies $s$ and any initial money balances $m$ , there exist demands $d$ and planned money balances $m'$ such that every agent satisfies the monetary budget constraint $\langle p,d_i\rangle+m'_i=\langle p,s_i\rangle+m_i$ and yet

z_g<0\quad\text{for every good }g\in G,

i.e. there is a general glut. Once agents may hold on to the proceeds of sales as money instead of spending them, the budget constraints alone no longer rule out a general glut, which is the Keynesian and Marxian objection to Say's law.

Preamble

import Mathlib
import Definitions.Def_SaysLaw_Model

Formal statement

namespace SaysLaw

theorem hoarding_permits_general_glut {ι G : Type*} [Fintype ι] [Nonempty ι] [Fintype G]
    (p : G → ℝ) (supply : ι → G → ℝ) (m : ι → ℝ) :
    ∃ (demand : ι → G → ℝ) (m' : ι → ℝ),
      MonetaryBudget p supply demand m m' ∧ GeneralGlut (excessDemand supply demand) := 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$ be a finite type assumed nonempty, $G$ an arbitrary finite type (possibly empty), $p:G\to\mathbb R$ arbitrary (no sign condition), $s:\iota\to G\to\mathbb R$ and $m:\iota\to\mathbb R$ arbitrary. Then there exist $d:\iota\to G\to\mathbb R$ and $m':\iota\to\mathbb R$ such that (1) for every $i$ , $\sum_g p_g d_{i,g}+m'_i=\sum_g p_g s_{i,g}+m_i$ , and (2) for every $g\in G$ , $\sum_i(d_{i,g}-s_{i,g})<0$ . No sign or nonnegativity condition is imposed on the witnesses $d$ and $m'$ (demands may be negative), and none relating $m'$ to $m$ beyond (1). If $G$ is empty, (2) holds vacuously.

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