§3.3, p. 17 — every D^µ satisfies Axiom 4

Proved

PrefSemimetric.TopDiff.dmu_axiom4

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

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

Let $X$ be a finite set and $\mu$ a positive measure on $2^X$ . If $\succsim$ and $\trianglerighteq$ are acyclic orders with the same asymmetric part ( $\succ=\vartriangleright$ ), then

D^\mu(\succsim,\trianglerighteq)=0.

Maximal elements depend only on the strict part of a relation, so $D^\mu$ cannot distinguish orders that differ only in their symmetric parts.

Formalization Note $\mu$ is given by point weights $w\ge0$ .

Preamble

import Mathlib
import Definitions.Def_PrefSemimetric_TopDiff_Model

Formal statement

namespace PrefSemimetric.TopDiff

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

end PrefSemimetric.TopDiff

Source

Nishimura & Ok, A Class of Dissimilarity Semimetrics for Preference Relations, arXiv:2203.04418v1, p. 17, §3.3 ('Finally, it is plain that Dµ satisfies Axiom 4.'); Axiom 4, p. 15

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