§3.1, p. 12 — each µ-top-difference D^µ is a semimetric on acyclic orders

Proved

PrefSemimetric.TopDiff.dmu_isSemimetric

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

p2o-batch-pfp2ap2o-gran-per-chapterp2o-plan-paperp2o-v1preference-relationspseudometrictop-difference-semimetric

Let $X$ be a nonempty finite set and $\mu$ a positive measure on $2^X$ . Then the $\mu$ -top-difference function

D^\mu(\succsim,\trianglerighteq)=\sum_{S\subseteq X}\mu\big(M(S,\succsim)\triangle M(S,\trianglerighteq)\big)

is a semimetric on the set $\mathcal A(X)$ of acyclic orders on $X$ : for all acyclic orders $\succsim,\trianglerighteq,\unrhd'$ ,

$D^\mu(\succsim,\trianglerighteq)\ge 0$ ;
$D^\mu(\succsim,\succsim)=0$ ;
$D^\mu(\succsim,\trianglerighteq)=D^\mu(\trianglerighteq,\succsim)$ ;
$D^\mu(\succsim,\unrhd')\le D^\mu(\succsim,\trianglerighteq)+D^\mu(\trianglerighteq,\unrhd')$ .

This makes $D^\mu$ an admissible candidate in Theorem 3.1, which characterizes exactly these semimetrics.

Formalization Note $\mu$ is given by point weights $w\ge0$ , $\mu(T)=\sum_{x\in T}w(x)$ . "Semimetric" is read as a pseudometric with values in $[0,\infty)$ (the conjuncts above), on relations satisfying IsAcyclicOrder.

Preamble

import Mathlib
import Definitions.Def_PrefSemimetric_TopDiff_Model

Formal statement

namespace PrefSemimetric.TopDiff

theorem dmu_isSemimetric {X : Type*} [Fintype X] [DecidableEq X] [Nonempty X]
    (w : X → ℝ) (hw : ∀ x, 0 ≤ w x) :
    IsSemimetric (Dmu w) := by sorry

end PrefSemimetric.TopDiff

Source

Nishimura & Ok, A Class of Dissimilarity Semimetrics for Preference Relations, arXiv:2203.04418v1, p. 12, §3.1 ('That each Dµ is indeed a semimetric on A(X) is straightforward.')

Human review

Endorsed by Shuze Chen · Oct 20, 2026
Confirmed by the moderator at approval.
Endorsed by mikedeng1 · Oct 20, 2026
Confirmed by the mission captain (proposal self-audit).

View graph