Uniqueness of the equilibrium interest rate

Existence came from the intermediate value theorem. Uniqueness comes from single crossing: capital demand falls in the interest rate, so if capital supply RISES in it the two curves meet at most once. This file proves that skeleton and supplies the demand half.

What the literature says, and why only the skeleton is here

The supply half is the whole difficulty, and it is not a theorem about the model — it is a restriction on the calibration.

Light (2018) proves uniqueness for CRRA utility and Cobb–Douglas production when relative risk aversion γ ≤ 1. The argument is exactly the one below: individual savings rise with the interest rate (his Theorem 1), hence aggregate savings do (Theorem 2), and since the capital-to-wage ratio k(R)/w(R) strictly falls, the curves cross once (Theorem 3). The economics of γ ≤ 1 is that the substitution effect dominates the income effect: a higher rate raises the price of current consumption, but also makes existing wealth worth more, and only when γ ≤ 1 does the first dominate.

For γ > 1 supply need not rise. Açıkgöz (2018) exhibits multiple stationary equilibria at γ = 6.5. Walsh and Young's November 19, 2025 draft uses 24,000 parameter draws, retains 23,673 after numerical screening, and reports 250 cases with three equilibria. They report that they never see multiplicity with risk aversion below about 1.49, depreciation below about 0.19, or income persistence below about 0.47, and only ever with a disaster state for income. Their mechanism is precautionary: with a disaster state, persistent income and high risk aversion, agents facing a low return still amass capital to insure against near-zero income, so capital supply bends back and can cross downward-sloping demand more than once. These findings concern their competitive economies, not counterexamples instantiating this capped household and its prescribed normalized demand.

Kirkby (2018) approaches it computationally and finds both Aiyagari (1994) and Pijoan-Mas (2006) "almost certainly have a unique general equilibrium".

So the honest formal target is CONDITIONAL uniqueness — uniqueness given monotone supply — plus, separately, whatever route establishes monotone supply for a restricted class. That is what is proved here; monotone supply remains an explicit input rather than a claim about every calibration.

theorem LeanEconomics.eq_of_monotoneOn_of_strictAntiOn {S D : ℝ → ℝ} {s : Set ℝ} (hS : MonotoneOn S s) (hD : StrictAntiOn D s) {r₁ r₂ : ℝ} (h₁ : r₁ ∈ s) (h₂ : r₂ ∈ s) (he₁ : S r₁ = D r₁) (he₂ : S r₂ = D r₂) : r₁ = r₂

Single crossing. A non-decreasing supply curve meets a strictly decreasing demand curve at most once. This is the skeleton of Light (2018) Theorem 3.

theorem LeanEconomics.capitalDemand_strictAntiOn {A δ rlo rhi : ℝ} (hA : A ≠ 0) (h : 0 < rlo + δ) : StrictAntiOn (capitalDemand A δ) (Set.Icc rlo rhi)

Capital demand falls STRICTLY in the interest rate, which is the half of single crossing that is a theorem about the technology rather than about the households.

theorem LeanEconomics.equilibriumRate_unique {A δ rlo rhi : ℝ} (hA : A ≠ 0) (hδ : 0 < rlo + δ) {S : ℝ → ℝ} (hS : MonotoneOn S (Set.Icc rlo rhi)) {r₁ r₂ : ℝ} (h₁ : r₁ ∈ Set.Icc rlo rhi) (h₂ : r₂ ∈ Set.Icc rlo rhi) (he₁ : S r₁ = capitalDemand A δ r₁) (he₂ : S r₂ = capitalDemand A δ r₂) : r₁ = r₂

Conditional uniqueness of the equilibrium interest rate. Given that capital supply is non-decreasing in the rate, the equilibrium rate is unique.

The hypothesis hS is the entire economic content, and it is restrictive: it holds for CRRA with γ ≤ 1 (Light 2018) and fails for the calibrations of Açıkgöz (2018) and Walsh and Young (2025). See the module docstring.

theorem LeanEconomics.equilibriumRate_le_of_supply_le {A δ rlo rhi : ℝ} (hA : A ≠ 0) (hδ : 0 < rlo + δ) {S T : ℝ → ℝ} (hS : MonotoneOn S (Set.Icc rlo rhi)) (hle : ∀ r ∈ Set.Icc rlo rhi, S r ≤ T r) {r₁ r₂ : ℝ} (h₁ : r₁ ∈ Set.Icc rlo rhi) (h₂ : r₂ ∈ Set.Icc rlo rhi) (he₁ : S r₁ = capitalDemand A δ r₁) (he₂ : T r₂ = capitalDemand A δ r₂) : r₂ ≤ r₁

A larger capital supply means a lower equilibrium rate. With demand strictly decreasing, two economies whose supply schedules are ordered have their equilibrium rates ordered the other way. This is what uniqueness buys: without it "the" equilibrium rate is not a number to compare.

The hypothesis is only needed at r₂, and only monotonicity of the SMALLER supply is used.