Prove2Me

Proof of Proposition 2, PDF p. 35 — Num(f,β,δ) = 4N₅² − D² factors as (11) times a second factor

Proved
PlatformEntry.Regimes.prop2_num_factorization

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

p2o-batch-pfp2ap2o-gran-per-chapterp2o-plan-paperp2o-v1platform-entrypolynomial-identity

For all real δ,f,β\delta, f, \beta,

4(4(1+δ)−2β(2−δ+δ2)+β3(1+f)−β2(2+f+δf))2−(8−8δ2f+8βδ(1+f)−2β3δf(1+f)+β4(1+f)2+2β2(−4−3f+δ2(−1+f2)))2=(−β4(1+f)2+8δ(1+δf)+2β3(1+f)(1+δf)−4β(2+δ+δ2+2δf)+β2(−2δf+4(1+f)−2δ2(−1+f2)))×(β4(1+f)2−2β3(1+f)(−1+δf)+8(2+δ−δ2f)−4β(2+δ2−δ(3+2f))+2β2(−6−4f−δf+δ2(−1+f2))).\begin{aligned} &4\big(4(1+\delta) - 2\beta(2-\delta+\delta^2) + \beta^3(1+f) - \beta^2(2+f+\delta f)\big)^2 \\ &\quad - \big(8 - 8\delta^2 f + 8\beta\delta(1+f) - 2\beta^3\delta f(1+f) + \beta^4(1+f)^2 + 2\beta^2(-4-3f+\delta^2(-1+f^2))\big)^2 \\ &= \big(-\beta^4(1+f)^2 + 8\delta(1+\delta f) + 2\beta^3(1+f)(1+\delta f) - 4\beta(2+\delta+\delta^2+2\delta f) + \beta^2(-2\delta f + 4(1+f) - 2\delta^2(-1+f^2))\big) \\ &\quad \times \big(\beta^4(1+f)^2 - 2\beta^3(1+f)(-1+\delta f) + 8(2+\delta-\delta^2 f) - 4\beta(2+\delta^2-\delta(3+2f)) + 2\beta^2(-6-4f-\delta f+\delta^2(-1+f^2))\big). \end{aligned}

The left side is Num(f,β,δ)\mathrm{Num}(f,\beta,\delta), the numerator of H−1/4H - 1/4 over 4D24D^2; the first factor on the right is the function (11) of Lemma 3. The identity turns the condition H>1/4H > 1/4 into a sign condition on (11).

Preamble
import Mathlib
import Definitions.Def_PlatformEntry_Regimes_Model
Formal statement
namespace PlatformEntry.Regimes

theorem prop2_num_factorization (δ f β : ℝ) :
    4 * N5 δ f β ^ 2 - D δ f β ^ 2 = P11 δ f β * S2 δ f β := by sorry

end PlatformEntry.Regimes
Source
Qi, Song & Xiao, Coopetition in Platform-Based Retailing: On the Platform’s Entry, authors' manuscript with Online Supplement (2024-08-03; Management Science DOI 10.1287/mnsc.2023.00260), Online Supplement, Appendix A, proof of Proposition 2, PDF p. 35
Human review

  • Endorsed by Shuze Chen · Oct 14, 2026

    Confirmed by the moderator at approval.

  • Endorsed by mikedeng1 · Oct 14, 2026

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

View graph