§3.3, p. 16 — every D^µ satisfies Axiom 1′ and Axiom 1

Proved

PrefSemimetric.TopDiff.dmu_axiom1

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

additivityp2o-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$ . Then $D^\mu$ satisfies

Axiom 1′: for all acyclic orders $\succsim,\succsim_0,\trianglerighteq$ with $\succsim\to\succsim_0\twoheadrightarrow\trianglerighteq$ ,

D^\mu(\succsim,\trianglerighteq)=D^\mu(\succsim,\succsim_0)+D^\mu(\succsim_0,\trianglerighteq);

Axiom 1: the same identity whenever $\succsim_0$ is in-between $\succsim$ and $\trianglerighteq$ .

This is the additivity half of the "if" direction of Theorem 3.1.

Formalization Note $\mu$ is given by point weights $w\ge0$ . Acyclicity of $\succsim_0$ is part of the one-step relation.

Preamble

import Mathlib
import Definitions.Def_PrefSemimetric_TopDiff_Model

Formal statement

namespace PrefSemimetric.TopDiff

theorem dmu_axiom1 {X : Type*} [Fintype X] [DecidableEq X]
    (w : X → ℝ) (hw : ∀ x, 0 ≤ w x) :
    (∀ R R0 T, IsAcyclicOrder R → IsAcyclicOrder T → OneStepToward R R0 T →
        Dmu w R T = Dmu w R R0 + Dmu w R0 T) ∧
      Axiom1 (Dmu w) := by sorry

end PrefSemimetric.TopDiff

Source

Nishimura & Ok, A Class of Dissimilarity Semimetrics for Preference Relations, arXiv:2203.04418v1, p. 16, §3.3, proof of Theorem 3.1 ('An obvious application of Lemma 3.3 shows that Dµ satisfies Axiom 1’, and by induction, Axiom 1.'); Axioms 1 and 1′, p. 13

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