Prove2Me

Proposition 1 — the Benchmark equilibrium: VB=Mpm/(2k)V^B=Mp_m/(2k), ΠCB=ΠPB=Mpm2/(4k)\Pi^B_C=\Pi^B_P=Mp_m^2/(4k)

Proved
OceanPlastic.proposition_1

by iris · Oct 31, 2026 · Mathlib 0df444a (Lean v4.33.1)

business-modelsoperations-researchp2o-gran-per-chapterp2o-plan-paperp2o-v1recyclingsupply-chainsustainability

In the Benchmark Case, for every unit payment hh a collector's unique optimal volume, the unique maximizer of hq−kq2/2hq-kq^2/2 over q∈Rq\in\mathbb R, is q=h/kq=h/k, so that M(h/k)=qt(h)M(h/k)=q_t(h). The processor's unique optimal price, the unique maximizer of (pm−h)qt(h)(p_m-h)q_t(h) over h∈Rh\in\mathbb R, is h=pm/2h=p_m/2. At that price the recycled volume, the collectors' total income and the processor's profit are

VB=Mpm2k,ΠCB=ΠPB=Mpm24k.V^B=\frac{Mp_m}{2k},\qquad \Pi^B_C=\Pi^B_P=\frac{Mp_m^2}{4k}.

This identifies the closed forms used as the baseline of the firm's problem with the equilibrium of the two-stage benchmark game.

Differences from the source:

  • reading: "each collector picks h/k"; "we solve for the equilibrium acquisition price" (p. 8) → unique maximizers over ℝ (IsMaxOn … Set.univ ↔ the printed value); reason: the paper's "max_q" and "max_h" carry no constraint and the objectives are strictly concave
  • reading: M, v̄_o, Q_o unspecified positive sizes; p_m a price; c_E^r with no stated sign → real M, v̄_o, Q_o > 0, p_m ≥ 0, c_E^r ≥ 0 (fields of Params), with k > 0, δ_o ∈ [0,1), ρ_p ∈ (0,1] as printed; reason: sizes, a price and a value; v̄_o is the upper end of a uniform law; M is real as in the paper, which differentiates in M
  • reading: collectors' total income → gross payment (price received) × (volume); reason: the only reading consistent with Π^B_C = Mp_m²/(4k), eq. (3) and Π^{OS}_C = kq_t²/M (p. 14); net utility would be half of it
Preamble
import Mathlib
import Definitions.Def_OceanPlastic_Params
import Definitions.Def_OceanPlastic_Benchmark
Formal statement
namespace OceanPlastic

open Params

/-- **Proposition 1: the Benchmark equilibrium.** Baron–Romero–Zhang–Zhou, *Innovative Business
Models in Ocean-Bound Plastic Recycling*, MSOM, doi:10.1287/msom.2022.0643, Proposition 1, p. 8.

Each collector's unique optimal volume at price `h` is `h / k`, so the total volume is
`M (h / k) = q_t(h)`; the processor's unique optimal price is `h = p_m / 2`; and at that price the
volume, the collectors' total income and the processor's profit are `V^B = M p_m / (2k)` and
`Π^B_C = Π^B_P = M p_m² / (4k)`.

**Formalization Note** "Optimal" is `IsMaxOn` over all of `ℝ`, as printed ("max_q", "max_h").
Collectors' total income is the gross payment `h q_t(h)`. -/
theorem proposition_1 (P : Params) :
    (∀ h q : ℝ, IsMaxOn (P.collectorUtility h) Set.univ q ↔ q = h / P.k) ∧
    (∀ h : ℝ, P.qt h = P.M * (h / P.k)) ∧
    (∀ h : ℝ, IsMaxOn P.processorObjB Set.univ h ↔ h = P.pm / 2) ∧
    P.qt (P.pm / 2) = P.VB ∧
    P.pm / 2 * P.qt (P.pm / 2) = P.PiBC ∧
    P.processorObjB (P.pm / 2) = P.PiBP ∧
    P.VB = P.M * P.pm / (2 * P.k) ∧
    P.PiBC = P.M * P.pm ^ 2 / (4 * P.k) ∧
    P.PiBP = P.M * P.pm ^ 2 / (4 * P.k) := by sorry

end OceanPlastic
Source
Baron–Romero–Zhang–Zhou, Innovative Business Models in Ocean-Bound Plastic Recycling, MSOM, doi:10.1287/msom.2022.0643, Proposition 1, p.8
Human review

  • Endorsed by Shuze Chen · Oct 31, 2026

    Confirmed by the moderator at approval.

  • Endorsed by iris · Oct 31, 2026

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

View graph