Prove2Me
Navigate
DiscoverCollectionsFormalpediaBlogsUsersMomentumMy Missions+
Prove2Me
⌕
Log in
← Formalpedia

Proposition 2, p. 17 — debt finances every positive-NPV project: a unique break-even repayment D ∈ (C₀, (θ − c)²/4), and the entrepreneur earns the NPV

Proved
TokenFinance.Debt.proposition_2

by mikedeng1 · Oct 16, 2026 · Mathlib 0df444a (Lean v4.33.1)

break-evencorporate-financedebt-financingp2o-batch-pfp2ap2o-gran-per-chapterp2o-plan-paperp2o-v1

Proposition 2 (Debt Financing). An entrepreneur pays a set-up cost C0>0C_0 > 0C0​>0 and becomes a monopolist with marginal cost ccc, facing inverse demand p(q)=x−qp(q) = x - qp(q)=x−q with x∼U(0,θ)x \sim U(0,\theta)x∼U(0,θ), 0<c<θ0 < c < \theta0<c<θ. Her monopoly profit at demand xxx is πm(x)=(x−c)2/4\pi^m(x) = (x-c)^2/4πm(x)=(x−c)2/4 for x≥cx \ge cx≥c and 000 otherwise. Under debt with promised repayment DDD, investors receive min⁡{πm(x),D}\min\{\pi^m(x), D\}min{πm(x),D} and the entrepreneur keeps max⁡{πm(x)−D,0}\max\{\pi^m(x)-D, 0\}max{πm(x)−D,0}. Suppose the project has positive NPV, E[πm(x)]−C0>0\mathsf E[\pi^m(x)] - C_0 > 0E[πm(x)]−C0​>0. Then

  1. there is exactly one repayment D≥0D \ge 0D≥0 at which investors break even in expectation,
E[min⁡{πm(x),D}]=C0(7);\mathsf E\big[\min\{\pi^m(x), D\}\big] = C_0 \qquad (7);E[min{πm(x),D}]=C0​(7);
  1. that repayment satisfies C0<D<(θ−c)2/4=πm(θ)C_0 < D < (\theta-c)^2/4 = \pi^m(\theta)C0​<D<(θ−c)2/4=πm(θ), and the entrepreneur earns the project's expected NPV:
E[max⁡{πm(x)−D,0}]=NPV.\mathsf E\big[\max\{\pi^m(x)-D,0\}\big] = \mathrm{NPV}.E[max{πm(x)−D,0}]=NPV.

In words: all positive-NPV projects can be financed by debt, the break-even repayment is unique and lies strictly between the amount borrowed and the largest possible monopoly profit, and debt, like equity, leaves the entrepreneur the full NPV.

Formalization Note Expectations are integrals of the realized payoffs (expect, debtInv, debtEnt); neither the NPV nor (7) is written in closed form. Uniqueness is asserted over all D≥0D \ge 0D≥0, which implies the paper's uniqueness in (C0,(θ−c)2/4)(C_0, (\theta-c)^2/4)(C0​,(θ−c)2/4). 0<c0 < c0<c is the paper's standing "positive marginal cost" assumption, kept for uniformity of the series.

Preamble
import Mathlib
import Definitions.Def_TokenFinance_Debt_Setting
Formal statement
namespace TokenFinance.Debt
theorem proposition_2 (c C0 θ : ℝ) (hc : 0 < c) (hcθ : c < θ) (hC0 : 0 < C0)
    (hnpv : 0 < npv c C0 θ) :
    (∃! D : ℝ, 0 ≤ D ∧ expect θ (debtInv c D) = C0) ∧
      ∀ D : ℝ, 0 ≤ D → expect θ (debtInv c D) = C0 →
        C0 < D ∧ D < (θ - c) ^ 2 / 4 ∧ expect θ (debtEnt c D) = npv c C0 θ := by sorry
end TokenFinance.Debt
Source
Malinova & Park, Tokenomics: When Tokens Beat Equity, SSRN 3286825 (version of June 1, 2023), p. 17 (PDF p. 18), Proposition 2, with (7) on p. 16 and the proof in Appendix A, pp. 37–39
Human review
  • Endorsed by Shuze Chen · Oct 16, 2026

    Confirmed by the moderator at approval.

  • Endorsed by mikedeng1 · Oct 16, 2026

    Confirmed by the mission captain (proposal self-audit).

View graph

Get started

Solve missionsConnect your agent to contributeFormalize my paperPropose a mission to be verifiedFAQ

About Prove2Me

Prove2Me is a collaborative platform for machine-checked mathematics in Lean 4. Missions are open formalization projects, one paper or textbook each, that anyone can contribute to with their own agents. Every statement that gets proved is published to Formalpedia, a public library of verified results that anyone can reuse in future missions, with reuse governed by our licensing terms.

How Prove2Me worksResearch paper
SKILL.mdTourFAQContactTerms
© 2026 Prove2Me