World relative supply of cloth: the five cases

Proved

ComparativeAdvantage.relative_supply_cases

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

comparative-advantageeconomicsinternational-trade

Let Home have a comparative advantage in cloth, $a_{LC}/a_{LW}<a'_{LC}/a'_{LW}$ , and let world prices satisfy $P_C,P_W>0$ . Write $p=P_C/P_W$ . A competitive output of a country is a full-employment bundle in which labour works only in sectors paying the highest wage ( $P_C/a_{LC}$ in cloth, $P_W/a_{LW}$ in wine). Then:

If $p=a_{LC}/a_{LW}$ : every competitive output of Foreign is $(0,L'/a'_{LW})$ (Foreign specializes in wine), and for every $x$ with $0\le x\le L/a_{LC}$ Home has a competitive output producing exactly $x$ units of cloth (Home workers are indifferent, so cloth supply can take any feasible value).
If $p<a_{LC}/a_{LW}$ : for all competitive outputs of Home and Foreign, world cloth output is $0$ (both specialize in wine).
If $a_{LC}/a_{LW}<p<a'_{LC}/a'_{LW}$ : Home's competitive output is $(L/a_{LC},0)$ , Foreign's is $(0,L'/a'_{LW})$ , and world relative supply is

\frac{Q_C+Q'_C}{Q_W+Q'_W}=\frac{L/a_{LC}}{L'/a'_{LW}}.

If $p>a'_{LC}/a'_{LW}$ : world wine output is $0$ (both specialize in cloth).
If $p=a'_{LC}/a'_{LW}$ : every competitive output of Home is $(L/a_{LC},0)$ , and for every $y$ with $0\le y\le L'/a'_{LW}$ Foreign has a competitive output producing exactly $y$ units of wine.

This is the shape of the step-shaped relative supply curve $RS$ .

Preamble

import Mathlib
import Definitions.Def_ComparativeAdvantage_Model

Formal statement

namespace ComparativeAdvantage

theorem relative_supply_cases (h f : Country) (hCA : HasComparativeAdvantageInCloth h f)
    (PC PW : ℝ) (hPC : 0 < PC) (hPW : 0 < PW) :
    (PC / PW = h.aLC / h.aLW →
      (∀ qF, IsCompetitiveOutput f PC PW qF → qF = (0, f.L / f.aLW)) ∧
      ∀ x ∈ Set.Icc 0 (h.L / h.aLC), ∃ qH, IsCompetitiveOutput h PC PW qH ∧ qH.1 = x) ∧
    (PC / PW < h.aLC / h.aLW →
      ∀ qH qF, IsCompetitiveOutput h PC PW qH → IsCompetitiveOutput f PC PW qF →
        qH.1 + qF.1 = 0) ∧
    (h.aLC / h.aLW < PC / PW → PC / PW < f.aLC / f.aLW →
      ∀ qH qF, IsCompetitiveOutput h PC PW qH → IsCompetitiveOutput f PC PW qF →
        qH = (h.L / h.aLC, 0) ∧ qF = (0, f.L / f.aLW) ∧
        (qH.1 + qF.1) / (qH.2 + qF.2) = (h.L / h.aLC) / (f.L / f.aLW)) ∧
    (f.aLC / f.aLW < PC / PW →
      ∀ qH qF, IsCompetitiveOutput h PC PW qH → IsCompetitiveOutput f PC PW qF →
        qH.2 + qF.2 = 0) ∧
    (PC / PW = f.aLC / f.aLW →
      (∀ qH, IsCompetitiveOutput h PC PW qH → qH = (h.L / h.aLC, 0)) ∧
      ∀ y ∈ Set.Icc 0 (f.L / f.aLW), ∃ qF, IsCompetitiveOutput f PC PW qF ∧ qF.2 = y) := 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,P_W$ be reals with $P_C>0$ , $P_W>0$ . Call $(x,y)\in\mathbb R^2$ competitive for a country $(L,a_{LC},a_{LW})$ when $x\ge0$ , $y\ge0$ , $a_{LC}x+a_{LW}y=L$ , $x>0\Rightarrow P_W/a_{LW}\le P_C/a_{LC}$ , and $y>0\Rightarrow P_C/a_{LC}\le P_W/a_{LW}$ . The statement is the conjunction of five implications:

If $P_C/P_W=a_{LC}/a_{LW}$ , then (a) every pair competitive for $f$ equals $(0,L'/a'_{LW})$ , and (b) for every real $x$ with $0\le x\le L/a_{LC}$ there is a pair competitive for $h$ whose first coordinate is $x$ .
If $P_C/P_W<a_{LC}/a_{LW}$ , then for every $(x_H,y_H)$ competitive for $h$ and every $(x_F,y_F)$ competitive for $f$ : $x_H+x_F=0$ .
If $a_{LC}/a_{LW}<P_C/P_W$ and $P_C/P_W<a'_{LC}/a'_{LW}$ , then for all such competitive pairs: $(x_H,y_H)=(L/a_{LC},0)$ , $(x_F,y_F)=(0,L'/a'_{LW})$ , and $\dfrac{x_H+x_F}{y_H+y_F}=\dfrac{L/a_{LC}}{L'/a'_{LW}}$ (real division).
If $a'_{LC}/a'_{LW}<P_C/P_W$ , then for all such competitive pairs: $y_H+y_F=0$ .
If $P_C/P_W=a'_{LC}/a'_{LW}$ , then (a) every pair competitive for $h$ equals $(L/a_{LC},0)$ , and (b) for every real $y$ with $0\le y\le L'/a'_{LW}$ there is a pair competitive for $f$ whose second coordinate is $y$ .

The fourth bullet of the source (relative supply tending to infinity) is rendered only as world wine output being zero; no limit statement is made.

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