Equation (46), p. 42 — the break-even residual decreases in demand

Proved

TokenFinance.Statics.eq_46

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

comparative-staticsderivativesp2o-batch-pfp2ap2o-gran-per-chapterp2o-plan-paperp2o-v1token-financing

Fix marginal cost $c>0$ , pre-sale size $t>0$ , and set-up cost $C_0$ . When $c+2t<\theta$ , the partial derivative of the break-even residual with respect to the demand upper endpoint is

\frac{\partial F}{\partial\theta}=\frac{c}{3}\frac{((\theta-c)/2-t)^2(2\theta+c+2t)}{(c+t)\theta^2}-\frac{(\theta-c)^2(2\theta+c)}{12\theta^2}<0.

This is the demand-direction sign used in Proposition 4.

Formalization Note The condition $c+2t<\theta$ places the pre-sale below the maximal monopoly quantity and ensures $\theta>0$ .

Preamble

import Mathlib
import Definitions.Def_TokenFinance_Debt_Setting

Formal statement

namespace TokenFinance.Statics

theorem eq_46 (c C0 θ t : ℝ) (hc : 0 < c) (ht : 0 < t)
    (hregion : c + 2 * t < θ) :
    HasDerivAt
        (fun T : ℝ => c / (c + t) * (2 / (3 * T)) * ((T - c) / 2 - t) ^ 3 -
          (T - c) ^ 3 / (12 * T) + C0)
        (c / 3 * ((θ - c) / 2 - t) ^ 2 * (2 * θ + c + 2 * t) /
            ((c + t) * θ ^ 2) -
          (θ - c) ^ 2 * (2 * θ + c) / (12 * θ ^ 2)) θ ∧
      (c / 3 * ((θ - c) / 2 - t) ^ 2 * (2 * θ + c + 2 * t) /
            ((c + t) * θ ^ 2) -
          (θ - c) ^ 2 * (2 * θ + c) / (12 * θ ^ 2)) < 0 := by sorry

end TokenFinance.Statics

Source

Malinova & Park, Tokenomics: When Tokens Beat Equity, SSRN 3286825 (version of June 1, 2023), p. 42 (PDF p. 43), Appendix A, proof of Proposition 4, (46)

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