# Nonattainment of the three-marginal Coulomb Monge problem

The following describes the scope of the Lean formalization related to the following accompanying paper(s):

- [A counterexample to the Monge ansatz for the three-marginal Coulomb cost](../../preprints/A-counterexample-to-the-Monge-ansatz-for-the-three-marginal-Coulomb-cost-September-25-2026/paper.pdf)

## Scope

The Monge ansatz asks whether an optimal multi-marginal transport plan can be induced by maps from one marginal. For the three-marginal Coulomb cost in $\mathbb R^3$, the formalization constructs a smooth compactly supported probability density, with smooth compactly supported square root, for which no pair of measure-preserving Borel maps attains the Kantorovich minimum.

Nevertheless, the Monge and Kantorovich infima are equal: preserving maps with finite costs approach the minimum. This is the three-dimensional Coulomb result; the paper's inverse-power extensions in every dimension are outside this statement.

## Comparator links

| Result | Comparator statement |
| --- | --- |
| Coulomb Monge nonattainment with equality of infima | [CoulombCounterexample.lean](../ComparatorChallenges/CoulombCounterexample.lean) |