Optimal payments: every paid coin is worth no more than every retained coin

Proved

GreshamLaw.optimal_payment_iff_exchange

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. For a debt $d$ and a set $P$ of coins, $P$ is an optimal payment of $d$ from $s$ if and only if

$P$ is a legal payment of $d$ ( $P\subseteq s$ and the face values of $P$ add up to $d$ ), and
every paid coin is intrinsically worth at most every retained coin:

m_i\le m_j\qquad\text{for all } i\in P,\ j\in s\setminus P .

Under legal tender at equal value, a payer who keeps the more valuable money therefore always pays with the intrinsically least valuable coins available.

Preamble

import Mathlib
import Definitions.Def_GreshamLaw_Model

Formal statement

namespace GreshamLaw

theorem optimal_payment_iff_exchange {ι : Type*} [DecidableEq ι] (coin : ι → Coin)
    (s P : Finset ι) (d : ℝ)
    (hlegal : EqualLegalTender coin s) (hpos : ∀ i ∈ s, 0 < (coin i).face) :
    IsOptimalPayment coin s P d ↔
      IsLegalPayment coin s P d ∧ ∀ i ∈ P, ∀ j ∈ s \ P, (coin i).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 $c:\iota\to\mathrm{Coin}$ (face values $f_i$ , melt values $m_i$ , arbitrary reals), all finite sets $s,P\subseteq\iota$ and every real $d$ , assume:

$f_i=f_j$ for all $i,j\in s$ ;
$f_i>0$ for all $i\in s$ .

Then $P$ is an optimal payment of $d$ from $s$ — that is, $P\subseteq s$ , $\sum_{i\in P}f_i=d$ , and every finite $Q\subseteq s$ with $\sum_{i\in Q}f_i=d$ satisfies $\sum_{i\in s\setminus Q}m_i\le\sum_{i\in s\setminus P}m_i$ — if and only if $P\subseteq s$ , $\sum_{i\in P}f_i=d$ , and $m_i\le m_j$ for every $i\in P$ and every $j\in s\setminus P$ .

Edge cases: $P=\varnothing$ is allowed (then $d=0$ ); $P=s$ is allowed (the second condition is then vacuous); $d$ is arbitrary, and if no subset of $s$ has face total $d$ both sides are false for every $P$ .

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