Math and TheoryThe multi-marginal converse of Minty's theorem fails in the plane
Problem and result
- Problem
- Multi-marginal converse of Minty's theorem (Bartz–Bauschke–Phan–Wang, Remark 2.6)
- Posed in
- Bartz, Bauschke, Phan and Wang, Math. Program. 185 (2021), Remark 2.6
- Status
- Answered negatively
- Result
- For three marginals on ℝ² with cost Σ⟨xᵢ, xⱼ⟩, an explicit three-point c-monotone set admits no compatible zero-sum tuple, so every maximally c-monotone set containing it has a nonconvex sum image omitting 0.
Abstract
Bartz, Bauschke, Phan and Wang asked whether the converse half of Minty's theorem extends to several marginals: does maximal c-monotonicity for the cost Σ⟨xᵢ, xⱼ⟩ force the sum image to be the whole space? For three marginals on ℝ², three integer points form a c-monotone set to which no tuple with sum zero can be added, because four compatibility inequalities have a positive weighted sum equal to a sum of squares plus 23/26. Every maximal extension, which exists by Zorn's lemma, therefore has a sum image that omits the origin and is not convex.
Details
- Year
- 2026
- Discipline
- Mathematics
- Area
- Optimization
- Subject
- Optimization
- Result type
- Counterexample answering a published question and reproducible proof package
- Formal proof
- Standalone Lean package
- Family
multimarginal-minty- Keywords
- multi-marginal optimal transport, c-monotonicity, maximal monotone operators, Minty's theorem, firmly nonexpansive mappings, partition of the identity, convex analysis
Statement and scope
Formal scope. The whole argument is formalized in Lean for the actual two-point swap condition and maximality among all subsets of (ℝ²)³: the finite obstruction over arbitrary real tuples, the Zorn extension and the nonconvexity of the sum image. The reformulation through firmly nonexpansive maps is proved in the text only.
A Lean check establishes only the formal statement that is checked. It does not establish novelty, historical priority or a faithful transcription of an external source. Known gaps are listed in UNFINISHED.md; the authorship disclosure describes how the results were produced.
Manuscript
- PDF on this site
manuscript.pdf245 KB- PDF on GitHub
papers/mathematics/ multimarginal-minty/ manuscript.pdf - LaTeX source
papers/mathematics/ multimarginal-minty/ manuscript.tex
Formal proof
This result has a standalone Lean 4 package, separate from the shared library. Build it with the toolchain and instructions given in its README.
- Proof package
papers/mathematics/ multimarginal-minty/ - Lean project
papers/8 Lean filesmathematics/ multimarginal-minty/ lean/ - Lakefile
papers/mathematics/ multimarginal-minty/ lean/ lakefile.toml - Toolchain
leanprover/lean4:v4.19.0 - Library roots
Reproduce
The commands below are quoted from papers/, which gives their context and working directory.
bash scripts/verify.sh /tmp/minty-verification- README
papers/mathematics/ multimarginal-minty/ README.md - Verification guide
papers/mathematics/ multimarginal-minty/ verification/ README.md - Verification record
papers/mathematics/ multimarginal-minty/ VERIFICATION.md - Authorship
papers/mathematics/ multimarginal-minty/ AUTHORSHIP.md - Repository guide
verification/README.md - Unfinished proofs
UNFINISHED.md
Source and prior work
Prior work. Bartz, Bauschke, Phan and Wang, 2021.
Questions and answers
Does maximal c-monotonicity imply that the sum image is the whole space for several marginals?
No. For three marginals on ℝ² with cost c(x) = Σ_{i<j}⟨xᵢ, xⱼ⟩ and the two-point swap notion of c-monotonicity, the preprint gives a three-point c-monotone set to which no zero-sum tuple can be added, so every maximal extension (which exists by Zorn's lemma) has a sum image that omits 0 and is not convex. This answers the question of Remark 2.6 of Bartz, Bauschke, Phan and Wang negatively; other numbers of marginals, other dimensions and cyclic c-monotonicity are not addressed.
How does this relate to Lim's example?
Lim (SIAM J. Optim. 2023) gave a two-dimensional contact set whose sum image has a hexagonal hole, but that set is not maximally c-monotone and can be enlarged by the zero tuple, so it does not answer Remark 2.6. Searches found no earlier answer, but historical priority is not certified.
Is the proof formally verified?
Yes. The finite obstruction over arbitrary real tuples, the Zorn extension and the nonconvexity of the sum image are formalized in Lean 4 for the actual swap condition and maximality among all subsets of (ℝ²)³; the reformulation through firmly nonexpansive maps is proved in the text only.
Cite
Citation file papers/. For the whole collection, use CITATION.cff or CITATION.bib.
@misc{goyal2026multimarginalminty,
author = {Goyal, Dev D.},
title = {The Multi-Marginal Converse of {Minty}'s Theorem Fails in the Plane},
year = {2026},
month = oct,
note = {Preprint. Fully autonomous agentic research; publication responsibility: Dev D. Goyal},
url = {https://github.com/dvgyl/math-and-theory/tree/main/papers/mathematics/multimarginal-minty}
}