Ricardo's example: at 5/6 to 9/8 wine per cloth, both countries consume at least one unit of each good

Proved

ComparativeAdvantage.ricardo_terms_of_trade

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

comparative-advantageeconomicsinternational-trade

In Ricardo's example let England specialize in cloth (producing $2.2$ units) and Portugal in wine (producing $2.125$ units), and let one unit of cloth trade for $t$ units of wine, where

\frac56\le t\le\frac98.

Then there is an amount $x\ge0$ of cloth that England can export, receiving $tx$ units of wine, such that both countries consume at least one unit of each good:

2.2-x\ge1,\quad tx\ge1\quad\text{(England)},\qquad x\ge1,\quad 2.125-tx\ge1\quad\text{(Portugal)}.

Consequently both England and Portugal can consume at least as much of both goods under free trade as in autarky.

Preamble

import Mathlib
import Definitions.Def_ComparativeAdvantage_Model

Formal statement

namespace ComparativeAdvantage

theorem ricardo_terms_of_trade (t : ℝ) (ht₁ : 5 / 6 ≤ t) (ht₂ : t ≤ 9 / 8) :
    ∃ x : ℝ, 0 ≤ x ∧ 1 ≤ england.L / england.aLC - x ∧ 1 ≤ t * x ∧
      1 ≤ x ∧ 1 ≤ portugal.L / portugal.aLW - t * x := by sorry

end ComparativeAdvantage

Source

Wikipedia, "Comparative advantage" (PDF export supplied with the request); https://en.wikipedia.org/wiki/Comparative_advantage, section "Ricardo's example and Terms of trade"

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 real $t$ with $5/6\le t$ and $t\le 9/8$ , there exists a real $x$ such that

0\le x,\quad 1\le \tfrac{220}{100}-x,\quad 1\le t\,x,\quad 1\le x,\quad 1\le \tfrac{170}{80}-t\,x.

(The numbers $220/100$ and $170/80$ appear as England's $L/a_{LC}$ and Portugal's $L/a_{LW}$ .) The statement does not mention the leftover amounts $0$ to $0.2$ and $0$ to $0.125$ quoted in the source.

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