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
ProvedTokenFinance.Debt.proposition_2Proposition 2 (Debt Financing). An entrepreneur pays a set-up cost and becomes a monopolist with marginal cost , facing inverse demand with , . Her monopoly profit at demand is for and otherwise. Under debt with promised repayment , investors receive and the entrepreneur keeps . Suppose the project has positive NPV, . Then
- there is exactly one repayment at which investors break even in expectation,
- that repayment satisfies , and the entrepreneur earns the project's expected 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 , which implies the paper's uniqueness in . is the paper's standing "positive marginal cost" assumption, kept for uniformity of the series.
import Mathlib import Definitions.Def_TokenFinance_Debt_Setting
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
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.