Equation (45), p. 42 — the break-even residual increases in marginal cost

Proved

TokenFinance.Statics.eq_45

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

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

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

\frac{\partial F}{\partial c}=\frac{2t}{3}\frac{((\theta-c)/2-t)^3}{(c+t)^2\theta}+\left(\frac{(\theta-c)^2}{4\theta}-\frac{c((\theta-c)/2-t)^2}{(c+t)\theta}\right)>0.

This gives the cost-direction sign used in Proposition 4.

Formalization Note The final denominator is $(c+t)\theta$ , correcting the printed $(c+t)^2\theta$ . The printed claim that the parenthesized expression vanishes at $t=0$ confirms this correction.

Preamble

import Mathlib
import Definitions.Def_TokenFinance_Debt_Setting

Formal statement

namespace TokenFinance.Statics

theorem eq_45 (c C0 θ t : ℝ) (hc : 0 < c) (hθ : 0 < θ) (ht : 0 < t)
    (hregion : c < θ - 2 * t) :
    HasDerivAt
        (fun d : ℝ => d / (d + t) * (2 / (3 * θ)) * ((θ - d) / 2 - t) ^ 3 -
          (θ - d) ^ 3 / (12 * θ) + C0)
        (2 * t / 3 * ((θ - c) / 2 - t) ^ 3 / ((c + t) ^ 2 * θ) +
          ((θ - c) ^ 2 / (4 * θ) -
            c * ((θ - c) / 2 - t) ^ 2 / ((c + t) * θ))) c ∧
      0 < (2 * t / 3 * ((θ - c) / 2 - t) ^ 3 / ((c + t) ^ 2 * θ) +
          ((θ - c) ^ 2 / (4 * θ) -
            c * ((θ - c) / 2 - t) ^ 2 / ((c + t) * θ))) := 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, (45), corrected final denominator

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