Prove2Me

Lemma 3 — two monotone consistent rules that agree on two-competitor competitions agree everywhere

Proved
PrizeAlloc.Interval.lemma_3

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

axiomatic-characterizationconsistencyp2o-batch-pfp2ap2o-gran-per-chapterp2o-plan-paperp2o-v1prize-allocation

Let φ\varphi and φ′\varphi' be prize allocation rules that both satisfy endowment monotonicity and consistency. If

φ(N,R,E)=φ′(N,R,E)for every competition with ∣N∣=2,\varphi(N, \mathcal R, E) = \varphi'(N, \mathcal R, E) \quad \text{for every competition with } |N| = 2,

then φ(N,R,E)=φ′(N,R,E)\varphi(N, \mathcal R, E) = \varphi'(N, \mathcal R, E) for every competition (N,R,E)(N, \mathcal R, E), with any number of competitors.

A consistent, monotone rule is therefore determined by its two-competitor part; in the proof of Theorem 1 this reduces the characterization to competitions with two competitors.

Formalization Note Agreement is stated competitor by competitor, over rankings and endowments E≥0E \ge 0 only.

Preamble
import Mathlib
import Definitions.Def_PrizeAlloc_Interval_Setting
Formal statement
namespace PrizeAlloc.Interval

theorem lemma_3 {U : Type*} [DecidableEq U] (φ ψ : List U → ℝ → U → ℝ)
    (hφ : IsPrizeRule φ) (hψ : IsPrizeRule ψ)
    (hφEM : EndowmentMonotone φ) (hφCons : Consistent φ)
    (hψEM : EndowmentMonotone ψ) (hψCons : Consistent ψ)
    (h2 : ∀ (l : List U) (E : ℝ), IsRanking l → l.length = 2 → 0 ≤ E →
      ∀ i ∈ l, φ l E i = ψ l E i) :
    ∀ (l : List U) (E : ℝ), IsRanking l → 0 ≤ E → ∀ i ∈ l, φ l E i = ψ l E i := by sorry

end PrizeAlloc.Interval
Source
Dietzenbacher and Kondratev, Fair and Consistent Prize Allocation in Competitions, arXiv:2008.08985v2, p. 11, Lemma 3 (proof p. 27)
Human review

  • Endorsed by Shuze Chen · Oct 15, 2026

    Confirmed by the moderator at approval.

  • Endorsed by mikedeng1 · Oct 15, 2026

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

View graph