Gains from trade: specialization by comparative advantage expands both countries' consumption possibilities

Proved

ComparativeAdvantage.gains_from_trade

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

comparative-advantageeconomicsinternational-trade

Let Home and Foreign be two countries of the Ricardian model, Home with labour force $L$ and unit labour requirements $a_{LC},a_{LW}$ , Foreign with $L',a'_{LC},a'_{LW}$ (all positive), and suppose Home has a comparative advantage in cloth, $a_{LC}/a_{LW}<a'_{LC}/a'_{LW}$ . Let world prices $P_C,P_W>0$ satisfy

\frac{a_{LC}}{a_{LW}}\le\frac{P_C}{P_W}\le\frac{a'_{LC}}{a'_{LW}}.

Then

every bundle Home can produce in autarky, $a_{LC}Q_C+a_{LW}Q_W\le L$ , can be consumed by Home when it produces only cloth and trades, $a_{LC}Q_C+a_{LC}(P_W/P_C)Q_W\le L$ ;
every bundle Foreign can produce in autarky can be consumed by Foreign when it produces only wine and trades, $a'_{LW}(P_C/P_W)Q_C+a'_{LW}Q_W\le L'$ ;
if $a_{LC}/a_{LW}<P_C/P_W$ , Home's inclusion is strict;
if $P_C/P_W<a'_{LC}/a'_{LW}$ , Foreign's inclusion is strict.

By trading and specializing in the good of its comparative advantage, each country can expand its consumption possibilities and choose bundles it could not have produced in a closed economy.

Formalization Note The comparative-advantage hypothesis is the standing assumption of the source section; the two price bounds already imply its non-strict form.

Preamble

import Mathlib
import Definitions.Def_ComparativeAdvantage_Model

Formal statement

namespace ComparativeAdvantage

theorem gains_from_trade (h f : Country) (hCA : HasComparativeAdvantageInCloth h f)
    (PC PW : ℝ) (hPC : 0 < PC) (hPW : 0 < PW)
    (hlow : h.aLC / h.aLW ≤ PC / PW) (hhigh : PC / PW ≤ f.aLC / f.aLW) :
    autarkySet h ⊆ tradeSetCloth h PC PW ∧ autarkySet f ⊆ tradeSetWine f PC PW ∧
    (h.aLC / h.aLW < PC / PW → autarkySet h ⊂ tradeSetCloth h PC PW) ∧
    (PC / PW < f.aLC / f.aLW → autarkySet f ⊂ tradeSetWine f PC PW) := by sorry

end ComparativeAdvantage

Source

Wikipedia, "Comparative advantage" (PDF export supplied with the request); https://en.wikipedia.org/wiki/Comparative_advantage, section "Ricardian model"

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.

Here a country $c$ is a triple of real numbers $(L, a_{LC}, a_{LW})$ , all strictly positive (the structure itself carries the positivity proofs). Let $h=(L,a_{LC},a_{LW})$ and $f=(L',a'_{LC},a'_{LW})$ be countries with $a_{LC}/a_{LW}<a'_{LC}/a'_{LW}$ , and let $P_C>0$ , $P_W>0$ with

\frac{a_{LC}}{a_{LW}}\le\frac{P_C}{P_W}\le\frac{a'_{LC}}{a'_{LW}}.

Write $A_h=\{(x,y):x,y\ge0,\ a_{LC}x+a_{LW}y\le L\}$ , $A_f$ likewise for $f$ , $T_h=\{(x,y):x,y\ge0,\ a_{LC}x+a_{LC}(P_W/P_C)y\le L\}$ , and $T_f=\{(x,y):x,y\ge0,\ a'_{LW}(P_C/P_W)x+a'_{LW}y\le L'\}$ . The statement asserts the conjunction:

$A_h\subseteq T_h$ ;
$A_f\subseteq T_f$ ;
if $a_{LC}/a_{LW}<P_C/P_W$ , then $A_h\subsetneq T_h$ (contained and not equal);
if $P_C/P_W<a'_{LC}/a'_{LW}$ , then $A_f\subsetneq T_f$ .

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