§4, p. 6 — outcome monotonic policy induces a non-worsening response

Proved

StrategicPolicy.MonotoneBinary.remark_after_prop_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

Fix the finite strategic decision model, an outcome monotonic cost, and a policy $\pi\in[0,1]^m$ that is outcome monotonic. If $r_\pi(i)$ is the best response of an individual initially at $x_i$ , then

q_i\le q_{r_\pi(i)}\qquad\text{for every }i.

This is the observation following Proposition 2: a monotonic policy never makes a lower-outcome destination the selected best response.

Formalization Note The cost assumption includes the paper's two §4 equivalences for distinct indices. The standing model assumes free staying, strictly ordered outcomes, and the tie rule in (5).

Preamble

import Mathlib
import Definitions.Def_StrategicPolicy_MonotoneBinary_Setting

Formal statement

namespace StrategicPolicy.MonotoneBinary

variable {m : ℕ}

theorem remark_after_prop_2 [NeZero m]
    (p q : Fin m → ℝ) (γ : ℝ) (c : Fin m → Fin m → ℝ)
    (hstanding : Standing p q γ c) (hcost : OMCost q c)
    (π : Fin m → ℝ) (hπ : π ∈ Policies m) (hmono : OMPolicy q π) :
    ∀ i, q i ≤ q (br c q π i) := by sorry

end StrategicPolicy.MonotoneBinary

Source

Tsirtsis et al., Optimal Decision Making Under Strategic Behavior, arXiv:1905.09239v5, p. 6, §4, remark after Proposition 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