Prove2Me

Exchange economy: bundle values, excess demand, Say's budget, general glut, monetary budget

Definition
SaysLaw_Model

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

economicsgeneral-equilibriummacroeconomicssays-law

This file fixes the vocabulary of a minimal exchange economy in which Say's law can be stated.

Let ι\iota be a finite set of agents and GG a finite set of goods. A price vector is p∈RGp\in\mathbb R^G; agent ii brings the bundle si∈RGs_i\in\mathbb R^G to market (his supply) and plans to buy the bundle di∈RGd_i\in\mathbb R^G (his demand).

  1. Bundle value. ⟨p,x⟩=∑g∈Gpg xg\langle p,x\rangle=\sum_{g\in G}p_g\,x_g.
  2. Aggregate excess demand. zg=∑i∈ι(di,g−si,g)z_g=\sum_{i\in\iota}(d_{i,g}-s_{i,g}) for each good gg.
  3. Say's budget principle ("products are paid for with products"): for every agent ii,
⟨p,di⟩=⟨p,si⟩,\langle p,d_i\rangle=\langle p,s_i\rangle,

i.e. the proceeds of what is sold are spent in full on other products. 4. General glut. A vector z∈RGz\in\mathbb R^G is a general glut when zg<0z_g<0 for every g∈Gg\in G (every good is in excess supply). 5. Monetary budget. With initial money balances mim_i and planned money balances mi′m'_i,

⟨p,di⟩+mi′=⟨p,si⟩+mifor every i.\langle p,d_i\rangle+m'_i=\langle p,s_i\rangle+m_i\quad\text{for every }i.
  1. Aggregate excess demand for money. ∑i∈ι(mi′−mi)\sum_{i\in\iota}(m'_i-m_i); it is positive when agents in aggregate hoard money.

These notions formalize the article's sections "Formulation", "Keynesian", "Role of money" and J. S. Mill's treatment of money as a commodity (section "Immediate reception").

Formalization Note Quantities are real numbers with no sign restriction, so si,dis_i,d_i may be read as gross supplies and demands or as net trades. No sign restriction is placed on prices in the definitions; theorems that need positive prices assume them explicitly.

Definition code
import Mathlib

namespace SaysLaw

/-- Market value `∑ g, p g * x g` of a bundle of goods `x` at the price vector `p`. -/
def bundleValue {G : Type*} [Fintype G] (p x : G → ℝ) : ℝ :=
  ∑ g, p g * x g

/-- Aggregate excess demand for each good: the total quantity of good `g` that the agents
plan to buy, minus the total quantity of `g` that they bring to market (their supply). -/
def excessDemand {ι G : Type*} [Fintype ι] (supply demand : ι → G → ℝ) : G → ℝ :=
  fun g => ∑ i, (demand i g - supply i g)

/-- Say's budget principle ("products are paid for with products"): at prices `p`, every
agent plans to buy goods of exactly the market value of the goods he supplies, so that no
proceeds of a sale remain unspent. -/
def SaysBudget {ι G : Type*} [Fintype G] (p : G → ℝ) (supply demand : ι → G → ℝ) : Prop :=
  ∀ i, bundleValue p (demand i) = bundleValue p (supply i)

/-- A *general glut*: every good is in excess supply, i.e. aggregate excess demand is
strictly negative for every good. -/
def GeneralGlut {G : Type*} (z : G → ℝ) : Prop :=
  ∀ g, z g < 0

/-- Budget constraint of a monetary economy: agent `i` enters with money balance `m i` and
plans to end with money balance `m' i`; spending on goods plus planned money holdings
equals the value of goods supplied plus initial money holdings. -/
def MonetaryBudget {ι G : Type*} [Fintype G] (p : G → ℝ) (supply demand : ι → G → ℝ)
    (m m' : ι → ℝ) : Prop :=
  ∀ i, bundleValue p (demand i) + m' i = bundleValue p (supply i) + m i

/-- Aggregate excess demand for money: planned money holdings minus initial money
holdings, summed over all agents (positive when agents in aggregate hoard money). -/
def excessMoneyDemand {ι : Type*} [Fintype ι] (m m' : ι → ℝ) : ℝ :=
  ∑ i, (m' i - m i)

end SaysLaw
Source
Wikipedia, "Say's law" (PDF export supplied with the request); https://en.wikipedia.org/wiki/Say%27s_law, sections "Formulation", "Keynesian", "Role of money", "Immediate reception"
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.

The file introduces, in a namespace SaysLaw, six notions over a finite type of goods GG and (where needed) a finite type of agents ι\iota, all quantities and prices being arbitrary real numbers (no positivity is built in).

  1. For p,x:G→Rp,x:G\to\mathbb R, the bundle value is
⟨p,x⟩=∑g∈Gpg xg.\langle p,x\rangle=\sum_{g\in G}p_g\,x_g .
  1. For s,d:ι→G→Rs,d:\iota\to G\to\mathbb R (named supply and demand), the excess demand is the function g↦zg=∑i∈ι(di,g−si,g)g\mapsto z_g=\sum_{i\in\iota}(d_{i,g}-s_{i,g}). If ι\iota is empty, zg=0z_g=0 for all gg.
  2. SaysBudget p s d is the proposition that for every agent ii, ⟨p,di⟩=⟨p,si⟩\langle p,d_i\rangle=\langle p,s_i\rangle (an exact equality, not an inequality). It holds trivially, for example, when d=sd=s, or when p=0p=0.
  3. GeneralGlut z, for any z:G→Rz:G\to\mathbb R, is the proposition zg<0z_g<0 for every g∈Gg\in G (strict inequality). If GG is empty this holds vacuously.
  4. MonetaryBudget p s d m m', for m,m′:ι→Rm,m':\iota\to\mathbb R, is the proposition that for every agent ii,
⟨p,di⟩+mi′=⟨p,si⟩+mi.\langle p,d_i\rangle+m'_i=\langle p,s_i\rangle+m_i .

No sign condition is put on m,m′m,m'. 6. The excess money demand is ∑i∈ι(mi′−mi)\sum_{i\in\iota}(m'_i-m_i) (zero if ι\iota is empty).

No axioms, hypotheses or proofs appear in the file; it consists of these six definitions only.

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