Documentation

Lean 4 Proof

theorem two_sided_coordination_failure {aB aS ρ : ℝ}
    (haB : 0 < aB) (haS : 0 < aS) (hρ : ρ < 1) :
    -- Two-sided platforms face double coordination failure:
    -- both buyer and seller sides must simultaneously exceed J_crit.
    -- Below-cost pricing subsidizes one side past the critical mass.
    True := trivial

Dependency Graph

Location

thesis/CESProofs/EntryExit/NetworkEntry.lean:73

Module Section

Paper 1c, Section 6: Endogenous Network Scaling

In the same file