Newton's guinea: overvalued gold makes silver-for-gold arbitrage profitable without bound

Proved

GreshamLaw.newton_guinea_arbitrage

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

economicsgreshams-lawmonetary-economics

Let the legal rate at home be $r$ silver shillings per gold guinea, and suppose that abroad the gold of one guinea costs the silver of $m$ shillings, with

0<m<r

(gold is overvalued at home, as after Newton fixed the guinea at 21 shillings in 1717). Starting from $N>0$ shillings, one round of shipping silver abroad, buying gold, coining guineas at home and buying shillings at the legal rate yields $A_{r,m}(N)=\tfrac{N}{m}r$ shillings. Then

one round is strictly profitable: $N<A_{r,m}(N)$ ;
repeating the round makes the holding grow without bound: $A_{r,m}^{\,n}(N)\to\infty$ as $n\to\infty$ .

This is the mechanism by which good silver coin left Britain and Britain moved onto a de facto gold standard.

Formalization Note Transport and minting costs are ignored.

Preamble

import Mathlib
import Definitions.Def_GreshamLaw_Model

Formal statement

namespace GreshamLaw

theorem newton_guinea_arbitrage (r m N : ℝ) (hm : 0 < m) (hmr : m < r) (hN : 0 < N) :
    N < arbitrageRound r m N ∧
      Filter.Tendsto (fun n : ℕ => (arbitrageRound r m)^[n] N) Filter.atTop Filter.atTop := 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 all real numbers $r,m,N$ with $0<m$ , $m<r$ and $0<N$ , write $A(x)=\dfrac{x}{m}\cdot r$ . The statement asserts both:

$N<A(N)$ ;
the sequence $n\mapsto A^{n}(N)$ ( $A$ composed with itself $n$ times and applied to $N$ , with $A^{0}(N)=N$ ), indexed by natural numbers $n$ , tends to $+\infty$ : for every real bound $B$ there is $n_0$ such that $A^{n}(N)\ge B$ for all $n\ge n_0$ .

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