The source's example curves have the expected slopes

Proved

SupplyDemand.example_curves_slopes

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

economicsmicroeconomicssupply-and-demand

The four example curves of the source have the slopes the model requires:

the linear supply curve $Q(P)=3P-6$ is strictly increasing on $\mathbb R$ ;
the linear demand curve $Q(P)=32-2P$ is strictly decreasing on $\mathbb R$ ;
the constant-elasticity supply curve $Q(P)=5P^{0.5}$ is strictly increasing on $P>0$ ;
the constant-elasticity demand curve $Q(P)=3P^{-2}$ is strictly decreasing on $P>0$ .

This connects the article's examples with the slope hypotheses of the comparative-statics results.

Preamble

import Mathlib
import Definitions.Def_SupplyDemand_Model

Formal statement

namespace SupplyDemand

theorem example_curves_slopes :
    StrictMono linearSupply ∧ StrictAnti linearDemand ∧
    StrictMonoOn isoelasticSupply (Set.Ioi 0) ∧
    StrictAntiOn isoelasticDemand (Set.Ioi 0) := by sorry

end SupplyDemand

Source

Wikipedia, "Supply and demand", revision 1378800284, https://en.wikipedia.org/w/index.php?title=Supply_and_demand&oldid=1378800284, section "Supply schedule" and "Demand schedule" (example specifications)

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.

The statement asserts four facts simultaneously: (1) $P\mapsto3P-6$ is strictly increasing on all of $\mathbb R$ ; (2) $P\mapsto32-2P$ is strictly decreasing on all of $\mathbb R$ ; (3) $P\mapsto5P^{0.5}$ (real power) is strictly increasing on the open interval $(0,\infty)$ ; (4) $P\mapsto3P^{-2}$ (real power) is strictly decreasing on $(0,\infty)$ . Nothing is claimed for $P\le0$ in (3) and (4).

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