Thiers' law: without legal tender, nearly worthless money is refused

Proved

GreshamLaw.thiers_law

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

economicsgreshams-lawmonetary-economics

Suppose there is no legal tender law, so a seller accepts a set $P$ of coins for a good of price $p>0$ only if the total melt value of $P$ is at least $p$ . Let the wallet $s$ consist of good coins and bad coins, and suppose the bad coins are nearly worthless: each has melt value at most $\varepsilon$ , with

|\text{bad}|\cdot\varepsilon<p .

Then every payment $P\subseteq s$ that the seller accepts contains at least one good coin.

This is the reverse of Gresham's law ("Thiers' law"): in the absence of effective legal tender laws the seller will not accept anything but money of certain value.

Preamble

import Mathlib
import Definitions.Def_GreshamLaw_Model

Formal statement

namespace GreshamLaw

theorem thiers_law {ι : Type*} [DecidableEq ι] (coin : ι → Coin) (s good bad : Finset ι)
    (hpart : good ∪ bad = s) (p ε : ℝ) (hp : 0 < p)
    (hworthless : ∀ b ∈ bad, (coin b).melt ≤ ε) (hsmall : (bad.card : ℝ) * ε < p)
    (P : Finset ι) (hPs : P ⊆ s) (hacc : AcceptsAtMarketValue coin P p) :
    (P ∩ good).Nonempty := by sorry

end GreshamLaw

Source

Wikipedia, "Gresham's law" (PDF export supplied with the request); https://en.wikipedia.org/wiki/Gresham%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.

For every type $\iota$ with decidable equality, every $c:\iota\to\mathrm{Coin}$ (melt values $m_i$ , arbitrary reals; face values play no role), all finite sets $s,\mathrm{good},\mathrm{bad}\subseteq\iota$ , and all reals $p,\varepsilon$ , assume:

$\mathrm{good}\cup\mathrm{bad}=s$ (the two sets need not be disjoint);
$p>0$ ;
$m_b\le\varepsilon$ for every $b\in\mathrm{bad}$ ;
$|\mathrm{bad}|\cdot\varepsilon<p$ , where $|\mathrm{bad}|$ is the number of elements of $\mathrm{bad}$ ;
$P$ is a finite set with $P\subseteq s$ and $p\le\sum_{i\in P}m_i$ .

Then $P\cap\mathrm{good}$ is nonempty. Nothing is assumed about the melt values of good coins, and $\varepsilon$ may be negative.

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