With finite relative demand, the world relative price lies between the autarky prices

Proved

ComparativeAdvantage.relative_price_bounds

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 $P_C,P_W>0$ . Let $(Q_C,Q_W)$ be a competitive output of Home and $(Q'_C,Q'_W)$ a competitive output of Foreign at these prices, and suppose the world supplies of both goods are strictly positive,

Q_C+Q'_C>0,\qquad Q_W+Q'_W>0,

as market clearing requires when world relative demand is finite and positive. Then

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

The equilibrium relative price is therefore always bounded by the two autarky relative prices.

Formalization Note Relative demand is not modelled as a function; "finite relative demand" is encoded by the requirement that world output of both goods be positive.

Preamble

import Mathlib
import Definitions.Def_ComparativeAdvantage_Model

Formal statement

namespace ComparativeAdvantage

theorem relative_price_bounds (h f : Country) (hCA : HasComparativeAdvantageInCloth h f)
    (PC PW : ℝ) (hPC : 0 < PC) (hPW : 0 < PW) (qH qF : ℝ × ℝ)
    (hqH : IsCompetitiveOutput h PC PW qH) (hqF : IsCompetitiveOutput f PC PW qF)
    (hcloth : 0 < qH.1 + qF.1) (hwine : 0 < qH.2 + qF.2) :
    h.aLC / h.aLW ≤ PC / PW ∧ PC / PW ≤ f.aLC / f.aLW := 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})$ , $f=(L',a'_{LC},a'_{LW})$ be countries with $a_{LC}/a_{LW}<a'_{LC}/a'_{LW}$ ; let $P_C>0$ , $P_W>0$ ; let $(x_H,y_H)$ and $(x_F,y_F)$ be pairs of reals such that $(x_H,y_H)$ is competitive for $h$ and $(x_F,y_F)$ is competitive for $f$ at $(P_C,P_W)$ — that is, for each country: both coordinates $\ge0$ , $a_{LC}x+a_{LW}y=L$ , $x>0\Rightarrow P_W/a_{LW}\le P_C/a_{LC}$ , $y>0\Rightarrow P_C/a_{LC}\le P_W/a_{LW}$ . Assume further $x_H+x_F>0$ and $y_H+y_F>0$ . Then

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

No demand side appears in the statement.

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