Terms of trade: specialization pays exactly when the world price beats the opportunity cost

Proved

ComparativeAdvantage.terms_of_trade_iff

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

comparative-advantageeconomicsinternational-trade

Let a country have unit labour requirements $a_{LC},a_{LW}>0$ and labour force $L>0$ , and let world prices be $P_C,P_W>0$ .

Its autarky set is contained in its consumption set when it specializes in cloth if and only if

\frac{a_{LC}}{a_{LW}}\le\frac{P_C}{P_W}.

Its autarky set is contained in its consumption set when it specializes in wine if and only if

\frac{P_C}{P_W}\le\frac{a_{LC}}{a_{LW}}.

Hence terms of trade that benefit both a cloth exporter and a wine exporter lie between the two countries' opportunity costs.

Preamble

import Mathlib
import Definitions.Def_ComparativeAdvantage_Model

Formal statement

namespace ComparativeAdvantage

theorem terms_of_trade_iff (c : Country) (PC PW : ℝ) (hPC : 0 < PC) (hPW : 0 < PW) :
    (autarkySet c ⊆ tradeSetCloth c PC PW ↔ c.aLC / c.aLW ≤ PC / PW) ∧
    (autarkySet c ⊆ tradeSetWine c PC PW ↔ PC / PW ≤ c.aLC / c.aLW) := by sorry

end ComparativeAdvantage

Source

Wikipedia, "Comparative advantage" (PDF export supplied with the request); https://en.wikipedia.org/wiki/Comparative_advantage, section "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.

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 $c=(L,a_{LC},a_{LW})$ be a country and $P_C>0$ , $P_W>0$ . The statement asserts both equivalences:

[every $(x,y)$ with $x,y\ge0$ and $a_{LC}x+a_{LW}y\le L$ also satisfies $a_{LC}x+a_{LC}(P_W/P_C)y\le L$ ] $\iff a_{LC}/a_{LW}\le P_C/P_W$ ;
[every $(x,y)$ with $x,y\ge0$ and $a_{LC}x+a_{LW}y\le L$ also satisfies $a_{LW}(P_C/P_W)x+a_{LW}y\le L$ ] $\iff P_C/P_W\le a_{LC}/a_{LW}$ .

Only one country appears; the statement about two trading partners is obtained by applying it to each.

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