Theorem 4.4 — (EXC) iff every $\operatorname{argmax}(\omega[p])$ is an integral base set

Proved

SteinitzExchange.Extension.exc_iff_argmax_isIntegralBaseSet

by mikedeng1 · Sep 27, 2026 · Mathlib 0df444a (Lean v4.33.1)

integral-base-setm-concavep2o-batch-p100bp2o-gran-per-chapterp2o-plan-paperp2o-v1

Let $B\subseteq\mathbb Z^V$ be a finite integral base set and $\omega:B\to\mathbb R$ . Then $\omega$ satisfies (EXC) if and only if, for every $p:V\to\mathbb R$ ,

\operatorname{argmax}(\omega[p])=\{x\in B\mid \omega(x)+\langle p,x\rangle\ge\omega(y)+\langle p,y\rangle\ \forall y\in B\}

is an integral base set (equivalently, $\overline{\operatorname{argmax}(\omega[p])}$ is an integral base polytope whose integer points are exactly $\operatorname{argmax}(\omega[p])$ ).

This characterizes M-concavity by its maximizers, as concavity of a function is characterized by the convexity of the maximizer sets of all its linear perturbations.

Formalization Note. The page states the condition as " $\overline{\operatorname{argmax}(\omega[p])}$ is an integral base polytope". Read literally (the convex hull of $\operatorname{argmax}(\omega[p])$ equals the convex hull of some integral base set) the "if" direction is false: on $B=\{(2,0),(1,1),(0,2)\}$ with $\omega=0,-1,0$ every $\operatorname{argmax}(\omega[p])$ is $\{(2,0)\}$ , $\{(0,2)\}$ or $\{(2,0),(0,2)\}$ , each with an integral base polytope as convex hull, yet (EXC) fails. The paper's proof uses that $\operatorname{argmax}(\omega[p])$ itself is an integral base set, the reading glossed in Lemma 4.3 and used when Theorem 4.4 is applied on p. 292; that reading is stated here.

Preamble

import Mathlib
import Definitions.Def_SteinitzExchange_Extension_IntegralBaseSet
import Definitions.Def_SteinitzExchange_Extension_Exchange

Formal statement

namespace SteinitzExchange.Extension

/-- Murota 1996, p. 286, Theorem 4.4, in the reading of Lemma 4.3 ("argmax(ω) is an integral base
set, that is, conv(argmax(ω)) is an integral base polytope"): on a finite integral base set `B`,
`ω` satisfies (EXC) iff `argmax(ω[p])` is an integral base set for every `p : V → ℝ`. -/
theorem exc_iff_argmax_isIntegralBaseSet {V : Type*} [Fintype V] [DecidableEq V] [Nonempty V]
    (B : Finset (V → ℤ)) (hB : IsIntegralBaseSet B) (ω : (V → ℤ) → ℝ) :
    SatisfiesEXC B ω ↔ ∀ p : V → ℝ, IsIntegralBaseSet (argmaxB B (perturb ω p)) := by sorry

end SteinitzExchange.Extension

Source

Murota, Convexity and Steinitz's Exchange Property, Adv. Math. 124 (1996), p. 286, Theorem 4.4 (read as in Lemma 4.3, p. 285, and as applied on p. 292)

Read-back

What the Lean code literally says, in plain math · claude-opus-5-5

Setting. $V$ is a finite, nonempty type with decidable equality. $\chi_u$ is the indicator vector of $u$ , and $\langle p, b\rangle = \sum_v p(v)b(v)$ .

Hypotheses.

$B \subseteq \mathbb{Z}^V$ is a finite integral base set. That is, $B$ is nonempty, and for all $x, y\in B$ and every $u$ with $(x-y)(u)>0$ there is some $v$ with $(x-y)(v)<0$ and $x-\chi_u+\chi_v\in B$ .
$\omega : \mathbb{Z}^V \to \mathbb{R}$ is arbitrary.

Conclusion. The following two statements are equivalent.

$\omega$ satisfies (EXC) on $B$ . For all $x, y\in B$ and every $u$ with $(x-y)(u)>0$ , there is some $v$ with $(x-y)(v)<0$ such that $x-\chi_u+\chi_v\in B$ , $y+\chi_u-\chi_v\in B$ and

\omega(x)+\omega(y)\le\omega(x-\chi_u+\chi_v)+\omega(y+\chi_u-\chi_v).

For every $p \in \mathbb{R}^V$ , the argmax of the perturbation is an integral base set. The set in question is

\{x\in B : \omega[p](y)\le\omega[p](x)\ \forall y\in B\}, \qquad \omega[p](x)=\omega(x)+\langle p,\iota(x)\rangle.

Being an integral base set means it is nonempty and has the one-sided exchange property within itself.

Degenerate cases.

If $B$ $B$ has one element:
- (EXC) holds vacuously;
- every argmax is that one-element set, which is an integral base set;
- so both sides are true.
Nonemptiness of each argmax is automatic, because $B$ is finite and nonempty.

Human review

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

View graph

Theorem 4.4 — (EXC) iff every argmax⁡(ω[p])\operatorname{argmax}(\omega[p])argmax(ω[p]) is an integral base set

Theorem 4.4 — (EXC) iff every $\operatorname{argmax}(\omega[p])$ is an integral base set