Paying with one coin: the most debased coin is handed over

Proved

GreshamLaw.sixpence_single_coin

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

economicsgreshams-lawmonetary-economics

Let $s$ be a finite wallet of coins, all of the same positive face value $f$ (legal tender at equal value). For a coin $c$ , paying the debt $f$ with the single coin $c$ is optimal for the payer (no other legal payment of $f$ from $s$ lets the payer keep more intrinsic value) if and only if

c\in s\quad\text{and}\quad m_c\le m_j\ \text{ for every } j\in s .

This is the article's sixpence example: the customer hands over the most debased coin, and the shopkeeper, giving one penny in change, has every reason to give the most debased penny.

Preamble

import Mathlib
import Definitions.Def_GreshamLaw_Model

Formal statement

namespace GreshamLaw

theorem sixpence_single_coin {ι : Type*} [DecidableEq ι] (coin : ι → Coin) (s : Finset ι)
    (hlegal : EqualLegalTender coin s) (hpos : ∀ i ∈ s, 0 < (coin i).face) (c : ι) :
    IsOptimalPayment coin s {c} (coin c).face ↔
      c ∈ s ∧ ∀ j ∈ s, (coin c).melt ≤ (coin j).melt := 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 assignment $c:\iota\to\mathrm{Coin}$ of a face value $f_i$ and a melt value $m_i$ (arbitrary reals) to each index, every finite set $s\subseteq\iota$ and every index $c_0\in\iota$ (not assumed to lie in $s$ ), assume:

all coins of $s$ have equal face value: $f_i=f_j$ for $i,j\in s$ ;
every coin of $s$ has positive face value: $f_i>0$ for $i\in s$ .

Then the following are equivalent:

(a) $\{c_0\}$ is an optimal payment of the debt $d=f_{c_0}$ from $s$ : $\{c_0\}\subseteq s$ , $\sum_{i\in\{c_0\}} f_i=f_{c_0}$ , and for every finite $Q\subseteq s$ with $\sum_{i\in Q}f_i=f_{c_0}$ ,

\sum_{i\in s\setminus Q} m_i\le\sum_{i\in s\setminus\{c_0\}} m_i;

(b) $c_0\in s$ and $m_{c_0}\le m_j$ for every $j\in s$ .

If $s=\varnothing$ both sides are false. Melt values are unrestricted reals.

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