Prove2Me

Proof of Proposition 2, p.28 — the payoff formulas for α∗<1\alpha^*<1 and α∗=1\alpha^*=1

Proved
StrategicObfuscation.payoff_formulas

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

game-theoryinformation-economicsp2o-gran-per-chapterp2o-plan-paperp2o-strengthenedp2o-v1patent-examinationperfect-bayesian-equilibrium

Let (e,α,Q)(e,\alpha,Q) be an equilibrium at σ∈[0,1]\sigma\in[0,1].

  1. If α∈(0,1)\alpha\in(0,1), then QV=cQV=c and (1−π(σ,0))p(V−c)=(1−p)(1−π(σ,e))c(1-\pi(\sigma,0))p(V-c)=(1-p)(1-\pi(\sigma,e))c.
  2. If α<1\alpha<1, then uS=p(V−c)π(σ,0)u_S=p(V-c)\pi(\sigma,0).
  3. If α=1\alpha=1, then uS=pV−c+(1−p)π(σ,e)cu_S=pV-c+(1-p)\pi(\sigma,e)c, where e=e(1,σ)e=e(1,\sigma).

So the sponsor's payoff depends on effort only when uncertified proposals are funded for sure.

Differences from the source:

  • generalization: Assumption 1 with ∂²π/∂σ∂e < 0 for a twice differentiable π → IsDetection: monotonicity plus decreasing differences in σ, strict whenever π(σ,·) separates the two efforts; reason: the C² class satisfies it by integrating the mixed partial, and the paper's own example on p.14, which the strict form excludes, also satisfies it
  • encoding: e(α, σ) written as a function → a fixed selection E with IsEffort π g E; reason: the argmax in (1) may not be a singleton; every selection is covered and existence of a maximizer stays part of the hypothesis, as in (1)
  • encoding: Bayes' rule (2) as a quotient → (2) cross-multiplied in IsEquilibrium; reason: the same equation whenever the denominator is nonzero; at σ = 1, e = 0 the report is off path and a PBE leaves Q free, where Lean's 0/0 = 0 would pin it
Preamble
import Mathlib
import Definitions.Def_StrategicObfuscation_IsDetection
import Definitions.Def_StrategicObfuscation_IsEffort
import Definitions.Def_StrategicObfuscation_IsEquilibrium
import Definitions.Def_StrategicObfuscation_sponsorPayoff

open Set
Formal statement
namespace StrategicObfuscation

/-- **The sponsor's payoff in equilibrium.**
Figueroa & Lemus, *The Benefit of the Doubt: Decision Making under Strategic Obfuscation*,
SSRN 3840423 (version of April 4, 2022), proof of Proposition 2, p.28 (PDF p.28).

In an equilibrium at `σ`: mixing `α ∈ (0, 1)` occurs only with `Q V = c`, equivalently
`(1 - π(σ, 0)) p (V - c) = (1 - p)(1 - π(σ, e)) c`; if `α < 1` then `u_S = p (V - c) π(σ, 0)`; and if
`α = 1` then `u_S = pV - c + (1 - p) π(σ, e) c`, where `e = e(1, σ)`. -/
theorem payoff_formulas {V c g p : ℝ} {π : ℝ → ℝ → ℝ} {E : ℝ → ℝ → ℝ}
    (hc : 0 < c) (hcV : c < V) (hg : 0 < g) (hp0 : 0 ≤ p) (hp1 : p ≤ 1)
    (hπ : IsDetection π) (hE : IsEffort π g E)
    {σ e α Q : ℝ} (hσ : σ ∈ Icc (0 : ℝ) 1) (heq : IsEquilibrium π V c p E σ e α Q) :
    (0 < α → α < 1 →
      Q * V = c ∧ (1 - π σ 0) * p * (V - c) = (1 - p) * (1 - π σ e) * c) ∧
    (α < 1 → sponsorPayoff π V c p σ α e = p * (V - c) * π σ 0) ∧
    (α = 1 → sponsorPayoff π V c p σ α e = p * V - c + (1 - p) * π σ e * c) := by sorry

end StrategicObfuscation
Source
Figueroa & Lemus, The Benefit of the Doubt: Decision Making under Strategic Obfuscation, SSRN 3840423 (version of April 4, 2022), proof of Proposition 2, p.28
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