Gresham's law: under equal legal tender, bad money is spent before good

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,\mathrm{good},\mathrm{bad}\subseteq\iota$, every real $d$ and every finite set $P\subseteq\iota$, assume:

1. $\mathrm{good}\cup\mathrm{bad}=s$;
2. $f_i=f_j$ for all $i,j\in s$ (face values are not assumed positive);
3. $m_b<m_g$ for every $g\in\mathrm{good}$ and every $b\in\mathrm{bad}$ (this forces $\mathrm{good}\cap\mathrm{bad}=\varnothing$);
4. $P$ is an optimal payment of $d$ from $s$: $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$.

Then: if some element of $P$ lies in $\mathrm{good}$, every element of $\mathrm{bad}$ lies in $P$. If $\mathrm{good}$ or $\mathrm{bad}$ is empty the conclusion holds trivially.