Equation (42), p. 41 — the break-even residual decreases in the pre-sale size

Proved

TokenFinance.Statics.eq_42

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$ , demand upper endpoint $\theta>0$ , and set-up cost $C_0$ . Let $F(c,C_0,\theta,t)$ be the difference between the two sides of (16). For $0\le t<(\theta-c)/2$ , its derivative with respect to $t$ is

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

This strict sign supplies local monotonicity of the break-even residual at the economically relevant root.

Formalization Note The displayed second term corrects a factor error in printed equation (42). The domain also states $-c<t$ so division by $c+t$ is valid; $0\le t$ already implies it when $c>0$ .

Preamble

import Mathlib
import Definitions.Def_TokenFinance_Debt_Setting

Formal statement

namespace TokenFinance.Statics

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

end TokenFinance.Statics

Source

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

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