The free-trade consumption possibility frontier lies above the autarky frontier

Proved

ComparativeAdvantage.trade_frontier

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

comparative-advantageeconomicsinternational-trade

Let a country specialize in cloth and trade at world prices $P_C,P_W>0$ with $a_{LC}/a_{LW}\le P_C/P_W$ , so that its consumption satisfies $a_{LC}Q_C+a_{LC}(P_W/P_C)Q_W\le L$ . Then

a bundle $(Q_C,Q_W)$ is in its consumption possibility set if and only if $Q_C,Q_W\ge0$ and

Q_C\le\frac{L}{a_{LC}}-\frac{P_W}{P_C}Q_W;

for every $Q_W\ge0$ ,

\frac{L}{a_{LC}}-\frac{a_{LW}}{a_{LC}}Q_W\le\frac{L}{a_{LC}}-\frac{P_W}{P_C}Q_W.

The consumption possibility frontier with trade lies on or above the autarky production possibility frontier.

Preamble

import Mathlib
import Definitions.Def_ComparativeAdvantage_Model

Formal statement

namespace ComparativeAdvantage

theorem trade_frontier (c : Country) (PC PW : ℝ) (hPC : 0 < PC) (hPW : 0 < PW)
    (hp : c.aLC / c.aLW ≤ PC / PW) :
    (∀ q : ℝ × ℝ, q ∈ tradeSetCloth c PC PW ↔
      0 ≤ q.1 ∧ 0 ≤ q.2 ∧ q.1 ≤ c.L / c.aLC - (PW / PC) * q.2) ∧
    ∀ QW : ℝ, 0 ≤ QW →
      c.L / c.aLC - (c.aLW / c.aLC) * QW ≤ c.L / c.aLC - (PW / PC) * QW := 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 $c=(L,a_{LC},a_{LW})$ be a country and $P_C>0$ , $P_W>0$ reals with $a_{LC}/a_{LW}\le P_C/P_W$ . The statement asserts both:

for every pair $(x,y)$ : [ $x\ge0$ , $y\ge0$ and $a_{LC}x+a_{LC}(P_W/P_C)y\le L$ ] holds if and only if [ $x\ge0$ , $y\ge0$ and $x\le L/a_{LC}-(P_W/P_C)y$ ];
for every real $y\ge0$ : $L/a_{LC}-(a_{LW}/a_{LC})y\le L/a_{LC}-(P_W/P_C)y$ .

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