Proposition 2, p. 6 — an outcome monotonic optimum exists

Proved

StrategicPolicy.MonotoneBinary.proposition_2

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

best-responsedecision-policyoutcome-monotonicityp2o-batch-pfp2ap2o-gran-per-chapterp2o-plan-paperp2o-v1strategic-classification

Let $\pi^*$ maximize the utility $u(\pi,\gamma)$ among all policies $\pi\in[0,1]^m$ . If the cost is outcome monotonic, there is an outcome monotonic policy $\pi$ with the same utility:

\pi\in[0,1]^m,\qquad \pi_i<\pi_j\Rightarrow q_i<q_j,\qquad u(\pi,\gamma)=u(\pi^*,\gamma).

This narrows the search for an optimum and is the prerequisite used in Theorem 3.

Formalization Note Optimality of $\pi^*$ is an explicit hypothesis, as in the paper. The finite model assumes distinct outcomes, free staying, and the standing positive cost condition; §4 cost monotonicity uses distinct indices. The policy monotonicity implication is the disclosed reading of (1).

Preamble

import Mathlib
import Definitions.Def_StrategicPolicy_MonotoneBinary_Setting

Formal statement

namespace StrategicPolicy.MonotoneBinary

variable {m : ℕ}

theorem proposition_2 [NeZero m]
    (p q : Fin m → ℝ) (γ : ℝ) (c : Fin m → Fin m → ℝ)
    (hstanding : Standing p q γ c) (hcost : OMCost q c)
    (πstar : Fin m → ℝ) (hopt : Optimal p q γ c πstar) :
    ∃ π ∈ Policies m, OMPolicy q π ∧ u p q γ c π = u p q γ c πstar := by sorry

end StrategicPolicy.MonotoneBinary

Source

Tsirtsis et al., Optimal Decision Making Under Strategic Behavior, arXiv:1905.09239v5, p. 6, Proposition 2; proof p. 18, Appendix A.2

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