All missions

Verified completion - 15 October 2026

The original exact goal EndStatement.ThreeSum.SolvedInTime 1.960614 is Proved on Prove2Me. All seven original milestones are complete. The complete machine extension has 481 accepted theorem proofs and reuses 110 proved theorem nodes; its accepted dependencies connect to the original main reduction. The independent fixed-model lower bound remains separate from the algorithm proof. Scientific priority and global optimality are not asserted by these formal verification results.

Why improve the deterministic integer 3SUM exponent?

3SUM asks whether three entries at distinct positions in an integer input sum to zero. Its familiar quadratic algorithm makes it a benchmark for studying how much arithmetic structure can reduce the cost of an exhaustive search. The relevant comparison is the exponent of input size in a precisely specified machine model. An improvement to that exponent is an asymptotic statement; it need not provide better measured running times at accessible input sizes.

Alman and Vassilevska Williams, 2026 developed a deterministic truly subquadratic framework for polynomially bounded integer 3SUM. The c0ldzy17 source snapshot, dated 11 October 2026, develops a subsequent deterministic construction with a formally stated 1.962 target. The author-supplied certificate package 3sum_certificate_1p960614_v3, dated 14 October 2026, studies a further parameter and switch refinement. It contains mathematical arguments and exact rational checks, and explicitly leaves the complete modified machine-program theorem unproved. This mission studies that remaining extension together with its supporting certificates.

Inputs, word instructions and analytic quantities

An input of size $n$ is an integer-valued function on the positions $0,\ldots,n-1$. For each fixed natural number $\kappa$, every value has absolute value at most $n^\kappa$. A YES instance has pairwise distinct positions $i,j,k$ satisfying $x_i+x_j+x_k=0$. Equal values at different positions are allowed. The problem asks for a decision, so a successful algorithm need not return the positions. Inputs of size less than three are NO instances.

The word RAM is the existing campaign foundation specification. A program is a finite list of instructions for constants, arithmetic, direct and indirect memory access, branching, acceptance and rejection. Words have a fixed width and a signed integer interpretation. For each fixed $\kappa$, one program, one word-width constant and one time function must work for every input size and every sufficiently large word width. The mission retains that specification without introducing an alternative computation model.

The supporting binary entropy is measured in bits:

$$H(t)=\frac{-t\log t-(1-t)\log(1-t)}{\log2},\qquad H(0)=H(1)=0.$$

For an integer expansion $c\ge3$, write

$$E_c=\frac c2H(1/c),\quad \kappa_c=2cH(1/(2c))-cH(1/c)-1,\quad \gamma_c(t)=cH(1/c)-cH((1-t)/c).$$

These are analytic quantities used to describe local encoding and reporting costs. The source's twelve charges also depend on a representation-scale parameter $e$, a band shift $b$, a box saving $S$, an initial threshold $\theta$, a terminal fraction $\tau$, and a uniform entropy coefficient $\rho$.

Formalization targets

The campaign goal is the exact proposition

$$\texttt{EndStatement.ThreeSum.SolvedInTime}\;(1.960614).$$

For $1.960614=980307/500000$, its time requirement is

$$\exists K\in\mathbb N\;\forall n\ge2,\quad T(n)^{500000}\le K n^{980307}.$$

Correctness and termination still cover all input sizes. The integer-size exponent includes $\kappa=0$, and the same program must be correct for every word width above its specified threshold.

The primary certificate uses $c=232$ and the rational quartic

$$P(t)=7.85174904t+0.72447023t^2+0.24044466t^3+0.12022459t^4.$$

Supporting targets establish its validity on $[0,1/2]$, its derivative and tangent bounds, and the uniform inequality $H(t)<0.27905030(1+P(t))$. The fixed parameters are $e=0.203889696$, $b=-0.062656016$, $S=0.193175570$, $\theta=0.040409899$, and $\tau=13/20$. The parameter theorem bounds every one of the twelve costs strictly below $1.96061388<1.960614$. Integer scheduling and general local-cover identities are separate milestones. A further independent milestone proves $R>1.96061349120$ for the explicitly defined relaxed fixed-expansion cost model. That model bound concerns its admissible parameter tuples; it is not a lower bound for 3SUM itself.

What these results establish

The supplied certificate demonstrates that a quartic switch already suffices for the proposed 1.960614 cost target. It also separates a uniform analytic inequality from a numerical experiment: the statement quantifies over the full closed interval. Its finite scheduling statement uses integer comparisons and accounts for the rounding error at every admissible level, rather than requiring executable logarithms.

Formalization adds checked statements about these continuous and finite objects and a reusable dependency structure. The full campaign goal requires an additional result: the actual modified program must obey the certified costs, and its operational correctness must reach the foundation specification. The upstream parameter certificate likewise distinguishes its exponent ledger from its separate implementation obligations. An exact rational checker passing is evidence for the numerical certificates; it does not establish the full new machine theorem.

Why the program extension remains substantive

Changing expansion from 256 to 232 changes the local universe and the vertex, output and degree counts together. The representation scale, band denominator and polynomial switch also change. Consequently, the original fixed-parameter runtime result cannot simply be invoked after replacing a few numerical constants. The new local construction, global encoding, sparse queries, reporting and arithmetic operations must share consistent parameters and a complete cost account.

The small gap between the principal cost cap and the target must absorb the proved subpolynomial overheads, including exceptional-size handling and the conversion to word instructions. The machine bridge has now been proved in this mission. Its accepted dependency tree connects the modified program and its runtime analysis to the unchanged campaign specification. Its statement has no assumed solver callback or unproved runtime contract. The fixed-model lower-bound milestone is an independent analytic root, and is not used to justify a faster algorithm.

Formalization scope and source boundaries

The campaign pins Lean 4.33.1 and Mathlib revision 0df444a360eaa60ab8c11dca51a86af692955474. Entropy and its derived quantities are real-valued; the final exponent is rational; finite subset counts and cleared switch comparisons use natural numbers. Theorems explicitly restrict logarithmic arguments and denominators to their intended domains. Natural-number subtraction in the switch is used only below the final level, with positive even microblock size.

The local-cover milestone covers every natural $c\ge3$ and positive half-block size. The cost-model milestone quantifies over all tuples satisfying its written assumptions and includes a whole-interval entropy constraint. Neither finite testing nor a floating-point optimizer substitutes for these universal statements. The initial package includes no Lean proof of the new machine goal, and the mission does not represent it as an established record.

The underlying algorithms and formal infrastructure retain their attribution to Alman and Vassilevska Williams; Björklund, Husfeldt, Kaski and Koivisto; Swapnil Jain; c0ldzy17; Anthropic; Jihoon Hyun; and Lean/Mathlib, as documented by the upstream source. The certificate development and this formalization use AI assistance. Scientific priority and global optimality are outside the mission's claims.

Selected references

• Author-supplied 3SUM: Positive-Coefficient Entropy Switch, 1.960614 Cost Certificate and Fixed-Model Lower Bound, certificate package v3, 14 October 2026. Exact source: 3sum_certificate_1p960614_v3/3sum_certificate_v3/PROOF.md, Sections 0–8; certificates/c232_quartic.json; verify_certificate.py. This is a supplied research artifact, not a claimed public publication.
• c0ldzy17, Deterministic 3SUM in O(n^1.962): method and proof, source documentation, 2026. Pinned METHOD.md, Parameters.lean, and LocalCoverBounds.lean.
• Josh Alman and Virginia Vassilevska Williams, Truly Subquadratic 3SUM and Truly Subcubic APSP via Triangles in Sparse Lopsided Graphs, arXiv preprint, 2026. arXiv:2610.06783v1.
• Anthropic, Truly Subquadratic 3SUM and Truly Subcubic APSP, Lean formalization, 2026. Pinned formal-math source. The campaign imports its shared word-RAM statement.

Source code and complete Lean formalization: GitHub repository. Fixed source revision: 8c25c0325de5.

Motivation

The Lightning Network is a payment layer built on top of Bitcoin: pairs of participants lock funds in a bilateral payment channel and then exchange payments off-chain, settling on the blockchain only occasionally. Keeping a channel open costs money, because it ties up capital and needs periodic rebalancing, and Guasoni, Huberman and Shikhelman (Lightning Network Economics: Channels, 2022, cited in the paper as [GHS22]) showed that this recurring cost depends on the channel's net flow and grows less than proportionally with it. Which network topology a population of payers and payees should use is therefore an economic question about subadditive costs on graphs.

Lightning Network Economics: Topology (SSRN 4439190; published version in Management Science, 2024, doi:10.1287/mnsc.2023.03872) answers this question in an axiomatic model. Its §3.2 introduces hermetization, which replaces the channels inside a group of nodes by channels to a new hub, and asks when this reduces cost. Theorem 3.8 gives a deterministic sufficient condition, a large average degree compared with the spread of channel sizes. Theorem 3.9, the subject of this mission, shows that the condition is typical: if channel sizes are random with thin, power-law-bounded cost tails, the network is hermetizable with high probability. The paper reads this as "cost reduction is the norm, not the exception", which is the economic argument for hubs in payment-channel networks.

Setting

Nodes form a finite set $V$. A Lightning Network (LN) is an anti-symmetric real matrix $\Lambda=(\lambda_{i,j})_{i,j\in V}$, $\lambda_{i,j}=-\lambda_{j,i}$, of net channel flows; $\lambda_{i,j}=0$ means there is no channel between $i$ and $j$. A channel cost is a function $c:\mathbb R\to\mathbb R_+$ with

• (MO) $c(x)>c(y)$ for $x>y\ge 0$; (SY) $c(-x)=c(x)$; (CI) $c(0)=0$;
• (SA) $c(x+y)<c(x)+c(y)$ for $x,y>0$;
• (SA+) for a strictly increasing $g_+:\mathbb R_+\to\mathbb R_+$, $c(kx)<\dfrac{k}{g_+(k)}c(x)$ for $k>1$, $x>0$.

The cost of the network is $c(G)=\tfrac12\sum_{i,j}c(\lambda_{i,j})$. For a node $i$, $d(i)$ is its number of channels, $s(i)$ the smallest and $S(i)$ the largest $|\lambda_{i,j}|$ over its channels.

The hermetization of a set of nodes $U$ deletes all channels inside $U$, adds a new node $v_0$, and joins each $i\in U$ to $v_0$ by a channel carrying $\sum_{j\in U}\lambda_{i,j}$, its net flow towards the rest of $U$. The set $U$ is hermetizable if this strictly lowers the cost, and the LN is hermetizable if some $U$ is.

In the random model a simple graph $E$ on $V$ fixes the channels, so $d(i)$ is the degree of $i$ in $E$ and is not random. On a probability space $(\Omega,\mathbb P)$, the flows $\lambda_{i,j}(\omega)$ are random variables, nonzero exactly on the channels of $E$, and $\Lambda(\omega)$ is an LN for every $\omega$.

Formalization targets

Goal: Theorem 3.9

Let $a>1$, $b>0$, $\varepsilon>0$. There is $k>0$, depending only on $(a,b,\varepsilon)$, such that for every finite $E$ with at least one channel, every $c,g_+$ satisfying (MO)–(SA+), and every random LN with, for all channels $ij\in E$,

$$\text{(i)}\ \ \mathbb P\big(c(\lambda_{i,j})>x\big)<b\,x^{-a}\ \ (x>0),\qquad \text{(ii)}\ \ \mathbb P\big(c(\lambda_{i,j})>\varepsilon\big)=1,$$

the LN is hermetizable with probability at least

$$1-k\sum_{i\in V}d(i)\,\big(g_+(d(i))\big)^{-a}.$$

The constant is not fixed: any $k$ uniform in the network and in $c,g_+$ is a proof of the goal.

Milestones

1. Lemma B.1. If every $i$ in a nonempty set $U$ has a channel in $U$ and $g_+(d_U(i))>2c(S_U(i))/c(s_U(i))$, with degrees and sizes in the subnetwork induced on $U$, then $U$ is hermetizable.
2. (8)–(10). $\mathbb P(\text{hermetizable})\ge 1-\sum_{i:\,d(i)\ge1}\mathbb P\big(g_+(d(i))\le 2c(S(i))/c(s(i))\big)$.
3. (11). Under (ii), $\mathbb P\big(g_+(d(i))\le 2c(S(i))/c(s(i))\big)\le\mathbb P\big(\tfrac{\varepsilon}{2}g_+(d(i))\le c(S(i))\big)$ for $d(i)\ge1$.
4. (12)–(13). Under (i), $\mathbb P\big(c(S(i))\ge x\big)\le d(i)\,b\,x^{-a}$ for every $x>0$.

The paper closes with "for some constant $k$, $\mathbb P\big(c(S(i))\ge\tfrac{\varepsilon}{2}g_+(d(i))\big)\le k\,d(i)\,(g_+(d(i)))^{-a}$, whence the claim."

Significance

The theorem turns the deterministic criterion of Lemma B.1 into a statement about typical networks. When degrees grow, $g_+(d)^{-a}$ decays, and the probability that no hub can reduce cost vanishes for any law with a power-bounded cost tail and a positive cost floor. This is the paper's evidence that hub-and-spoke structures are the economically stable outcome; the companion results of the paper (Theorem 3.1 on local restructuring, Theorem 3.10 on the star topology) are treated in sibling missions of this series.

The result is proved in the paper, in about half a page. It has no machine-checked proof. Formalizing it makes the quantifier structure explicit, in particular that $k$ does not depend on the network, settles the boundary cases the paper leaves implicit, and records corrected forms of two axioms that are unsatisfiable as printed. Lemma B.1 is shared with the mission on Theorem 3.8.

Difficulty

The probabilistic estimates are elementary; the obstacles are in the bookkeeping. Lemma B.1 compares two costs on different node sets (the hermetized network has one more node), and its degrees and channel sizes must be read in the subnetwork induced on $U$; with the degrees of the whole network the lemma is false. To apply it to a random network one must choose $U$: the set of all nodes fails when some node is isolated, because $s(i)$ is then undefined. The step from the strict tail $\mathbb P(c>x)$ of (i) to the weak tail $\mathbb P(c\ge x)$ used in (12)–(13) is a limit the paper does not write out. The inverse $g_+^{-1}$ that the paper uses need not exist, since $g_+$ is not assumed onto.

Formalization scope

Nodes are an arbitrary finite type V; the LN is Λ : V → V → ℝ, anti-symmetric; the channel graph is E : SimpleGraph V, with $\lambda_{i,j}(\omega)\ne0\iff ij\in E$ for every $\omega$, and $d(i)$ is E.degree i. The cost is the $\tfrac12\sum_{i,j}$ form. The hub $v_0$ of a hermetization is none : Option V. Probabilities are toReal of a probability measure, and events are not assumed measurable. Each $\lambda_{i,j}$ is assumed measurable in the goal. The conventions committed to:

• (SA) is used for all $x,y>0$: as printed ("for $x>y\ge0$") it demands $c(x)<c(x)$ at $y=0$. The corrected range is the one Appendix D verifies.
• (SA+) is used for $k>1$, $x>0$: as printed ($k\in\mathbb R_+$) it fails at $x=0$, and for $k\le1$ even for the paper's own example.
• Every condition $d>g_+^{-1}(y)$ is written $g_+(d)>y$.
• In Lemma B.1, $d$, $s$, $S$ are those of the subnetwork induced on $U$; $U$ is nonempty and each $i\in U$ has a channel in $U$. For a node without a channel, $s$ and $S$ take the junk value $0$, which no statement uses.
• The constants $a,b,\varepsilon$ are common to all channels. Neither independence nor identical distribution of the flows is assumed: the theorem's hypotheses are only (i) and (ii).
• The goal assumes at least one channel. With none, the printed bound is $1$ but the cost $0$ cannot be reduced.

The following formalizations are trivializing and are ruled out: a $k$ allowed to depend on $V$, $E$, $\mathbb P$, $\Lambda$, $c$ or $g_+$ (take $k$ large enough that the bound is $\le0$); a specific law, such as a Pareto law, or a specific cost such as $c(x)=\sqrt{|x|}$; replacing "the LN is hermetizable" by the event that every node satisfies Lemma B.1's inequality; an empty channel set; and the printed, unsatisfiable (SA) or (SA+), under which every statement is vacuous.

The development needs finite sums over Option V, a min/max over a node's channels, and union bounds for outer measures (Mathlib's measure_biUnion_finset_le). Contributions welcome: proofs of the milestones, a proof that the corrected axioms are satisfiable by $c(x)=\sqrt{|x|}$, $g_+(k)=k^{1/4}$, and a reusable statement of Lemma B.1 for the series.

Selected references

• P. Guasoni, G. Huberman, C. Shikhelman, Lightning Network Economics: Topology, SSRN working paper 4439190, version of February 3, 2023. https://ssrn.com/abstract=4439190 ; published in Management Science, 2024, https://doi.org/10.1287/mnsc.2023.03872
• P. Guasoni, G. Huberman, C. Shikhelman, Lightning Network Economics: Channels, 2022 (cited in the paper as [GHS22]; reference list, p. 16 of SSRN 4439190).
• J. Poon, T. Dryja, The Bitcoin Lightning Network: Scalable Off-Chain Instant Payments, 2016. https://lightning.network/lightning-network-paper.pdf

Learning to bid in first-price auctions

Most online advertising inventory is sold one impression at a time in automated auctions, and since about 2019 the major ad exchanges have moved from second-price to first-price rules: the highest bidder wins and pays its own bid. A bidder in a first-price auction must trade off winning probability against the price paid, and that trade-off depends on the unknown distribution of competing bids. A bidder who takes part in many such auctions can learn that distribution as it goes. The natural yardstick is regret: the expected shortfall of the bidder's cumulative reward relative to an oracle that knows the distribution of competing bids from the start.

Han, Zhou and Weissman (arXiv:2003.09795, Operations Research, 2025) give bidding policies whose expected regret is $\widetilde O(\sqrt T)$ over $T$ auctions, both for iid and for adversarial private values, under the censored feedback that real exchanges provide (only the winning bid is announced). Their Theorem 9 shows that the $\sqrt T$ rate cannot be improved, even in a much easier setting. This mission is that lower bound.

Related results put it in context. With binary feedback (only "won" or "lost"), regret of order $T^{2/3}$ is unavoidable (Kleinberg and Leighton, 2003). With a fixed value, repeated first-price bidding is a pricing problem on a one-dimensional action set whose reward $(1-b)G(b)$ need not be continuous in $b$. Theorem 9 shows that the extra information of the full competing bid buys $\sqrt T$ and nothing better.

Setting

In each round $t=1,\dots,T$ a bidder has a private value $v_t\in[0,1]$, submits a bid $b_t\in[0,1]$, and faces the highest other bid (HOB) $m_t\in[0,1]$, the largest bid of all competitors. The bidder wins when $b_t\ge m_t$, and its payoff is

$$r(v_t,b_t;m_t)=(v_t-b_t)\,\mathbb 1(b_t\ge m_t).$$

The HOBs $m_1,\dots,m_T$ are iid with an unknown cumulative distribution function $G(x)=\mathbb P(m_t\le x)$ on $[0,1]$. No smoothness is assumed: $G$ may have atoms. The expected reward of bid $b$ at value $v$ is $R(v,b)=(v-b)G(b)$, and the regret of the bids $b_1,\dots,b_T$ is

$$R_T(\pi;v)=\sum_{t=1}^T\Bigl(\max_{b\in[0,1]}R(v_t,b)-R(v_t,b_t)\Bigr).$$

A policy $\pi$ chooses $b_t$ from what it has observed before round $t$, and it may use internal randomness. Theorem 9 makes the problem as easy as possible: the value is $v_t=1$ in every round, and the HOB $m_t$ is revealed at the end of every round (full information), rather than only when the bidder loses. A policy is then a rule $b_t=\beta_t(u,m_1,\dots,m_{t-1})$, where $u$ is the policy's internal randomness.

The lower bound uses two HOB laws on $\{1/3,2/3\}$. For $\Delta\in(0,1/4)$, $G_1$ puts mass $\tfrac12+\Delta$ on $1/3$ and $\tfrac12-\Delta$ on $2/3$, and $G_2$ the reverse. $P_i^{\otimes T}$ is the law of $T$ iid HOBs from $G_i$. The total variation distance is $\|P-Q\|_{\mathrm{TV}}=\tfrac12\int|dP-dQ|$, and $D_{\mathrm{KL}}(P\|Q)=\int dP\log\frac{dP}{dQ}$ is the Kullback–Leibler divergence.

Formalization targets

Goal: Theorem 9 (p. 36)

There is an absolute constant $c>0$ such that, for every horizon $T\ge1$,

$$\inf_\pi\sup_G\ \mathbb E_G\bigl[R_T(\pi;v)\bigr]\ \ge\ c\sqrt T,\qquad v_t\equiv 1,$$

where the supremum is over all HOB distributions on $[0,1]$ and the infimum is over all full-information policies, randomized ones included. The constant is left unspecified, as in the paper; the paper's proof gives $c=1/(24e^2)$.

Milestones (App. A–B, pp. 36–38)

1. Oracle rewards (p. 37): with $v_t=1$, $\max_b(1-b)G_1(b)=(1+2\Delta)/3$, $\max_b(1-b)G_2(b)=1/3$ and $\max_b(1-b)(G_1+G_2)(b)=2/3$.
2. Separation (20): for every bid $b_t\in[0,1]$, the instantaneous regrets under $G_1$ and $G_2$ sum to at least $2\Delta/3$.
3. Two-point reduction (21): for every policy, $\tfrac12\mathbb E_{G_1}[R_T]+\tfrac12\mathbb E_{G_2}[R_T]\ge\frac{\Delta T}{3}\bigl(1-\|P_1^{\otimes T}-P_2^{\otimes T}\|_{\mathrm{TV}}\bigr)$.
4. Lemma 12: $1-\|P-Q\|_{\mathrm{TV}}\ge\tfrac12\exp\bigl(-(D_{\mathrm{KL}}(P\|Q)+D_{\mathrm{KL}}(Q\|P))/2\bigr)$.
5. KL computation (p. 37): $D_{\mathrm{KL}}(P_1^{\otimes T}\|P_2^{\otimes T})=T\,D_{\mathrm{KL}}(G_1\|G_2)\le32T\Delta^2$.
6. (22): $1-\|P_1^{\otimes T}-P_2^{\otimes T}\|_{\mathrm{TV}}\ge\tfrac12\exp(-32T\Delta^2)$.

Significance

The theorem shows that the upper bounds of the paper, $C\sqrt T\log^{2.5}T$ for iid values and $C\sqrt T\log^3T$ for adversarial values, are optimal up to logarithmic factors. Because the lower bound holds with a constant value and with every HOB revealed, it is not caused by censoring or by the value process. The $\sqrt T$ comes from the statistical difficulty of locating the maximizer of $(1-b)G(b)$ when $G$ is learned from samples. The same lower bound therefore applies to every richer feedback model and every value model that contains the constant sequence.

The milestones are general tools. Lemma 12 (a symmetrised Bretagnolle–Huber inequality), the product rule for KL divergences of iid laws, and the reduction (21) are the standard steps of Le Cam's two-point method. They recur in essentially every minimax lower bound for bandits and online learning.

The theorem has a complete proof in the paper (App. B). As far as is known it has not been machine-checked, and the needed pieces are only partly in Mathlib: there is a Kullback–Leibler divergence with a chain rule, but at the pinned revision there is no total variation distance and no Bretagnolle–Huber or Le Cam inequality. The work is to formalize the known proof.

Difficulty

The arithmetic is elementary, and the difficulty lies in the probabilistic reduction. The first idea, bounding the regret round by round under a single law, fails: for any fixed $G$ a policy that happens to bid the right point has zero regret, so the lower bound must come from a policy's inability to know which of two laws it faces. Making that precise requires the law of the observed history $(m_1,\dots,m_{t-1})$ under each hypothesis, the identity $\int\min\{dP,dQ\}=1-\|P-Q\|_{\mathrm{TV}}$, and monotonicity of total variation under marginalization from $T$ to $t-1$ coordinates. A randomized policy adds one more integration, over its internal randomness, before the per-round bound applies. The KL step needs the tensorization of KL over product measures and an elementary but explicit logarithmic inequality.

Formalization scope

All declarations live in the namespace FirstPriceLearning.LowerBound.

• Time. Rounds are Fin T; Lean round t is paper time $t+1$.
• HOB law. A measure μG on ℝ. The goal asks for a probability measure giving no mass outside $[0,1]$. The CDF is (μG (Set.Iic x)).toReal, with atoms allowed.
• Reward and regret. $R(v,b)=(v-b)G(b)$, and the oracle term is the supremum over $b\in[0,1]$ (a bounded nonempty family, attained). The regret is the pseudo-regret (3), a sum of expected-reward gaps.
• Policies. A policy carries a probability space $(U,\mu_U)$, with U : Type, for its internal randomness and bid maps bid t : U → (Fin t → ℝ) → ℝ that are jointly measurable with values in $[0,1]$. The history type Fin t → ℝ makes the policy non-anticipating by construction: it cannot read $m_t$ or later HOBs, and it never sees $G$.
• Expectation. An integral over $u\sim\mu_U$ independent of $m\sim G^{\otimes T}$ (Measure.prod with Measure.pi).
• Quantifiers. The goal is stated as $\exists c>0\ \forall T\ge1\ \forall\pi\ \exists G$, which implies the inf–sup form. The constant precedes $T$ and the policy, and the law is chosen after the policy.
• Divergences. KL is Mathlib's InformationTheory.klDiv, valued in $[0,\infty]$. Total variation is defined locally as $\tfrac12\int|p-q|\,d(P+Q)$ with Radon–Nikodym densities. In Lemma 12 the right-hand side is $0$ when a divergence is infinite ($\exp(-\infty)=0$).
• Hard laws. $G_1,G_2$ are explicit two-point measures; the milestones (20)–(22) are stated for $\Delta\in(0,1/4)$ as printed.

Two trivializing formalizations are excluded. A policy that observes $m_t$ (or $G$) before bidding would make the bound false rather than trivial, and the types forbid it. A non-measurable bid map would make the expectation the junk value $0$, and measurability is required. Restricting the policy class to deterministic policies, or reading $(\infty).\mathrm{toReal}=0$ in Lemma 12, would change the theorem and is not done.

Reusable beyond this mission: the total variation distance, Lemma 12, and the tensorization bound for KL. Contributions are welcome at every milestone, especially Lemma 12 and the data-processing step behind (21).

Selected references

• Y. Han, Z. Zhou, T. Weissman, Optimal No-regret Learning in Repeated First-price Auctions, Operations Research, 2025; preprint arXiv:2003.09795v7, 2024. https://arxiv.org/abs/2003.09795
• A. B. Tsybakov, Introduction to Nonparametric Estimation, Springer, 2009 (Lemma 2.6). https://doi.org/10.1007/b13794
• J. Bretagnolle, C. Huber, Estimation des densités: risque minimax, Z. Wahrscheinlichkeitstheorie verw. Gebiete 47, 1979. https://doi.org/10.1007/BF00535278
• R. Kleinberg, T. Leighton, The Value of Knowing a Demand Curve: Bounds on Regret for Online Posted-Price Auctions, FOCS, 2003. https://doi.org/10.1109/SFCS.2003.1238232

Reference prices and promotion-insensitive consumers

Consumers judge a price against a reference price, an internal standard formed from the prices they have seen before. A price above the reference is perceived as a loss and a price below it as a gain. When gains and losses weigh differently, the seller's current price shapes tomorrow's demand, and dynamic pricing becomes a sequential decision problem. A central question in this literature is whether the seller should hold a constant price in the long run or keep cycling through high and low prices.

For a single product, classic results show that loss aversion favours constant prices (Fibich, Gavious and Lowengart 2003; Popescu and Wu 2007; Nasiry and Popescu 2011). Hu and Nasiry (2018) showed that individual loss aversion need not carry over to aggregate demand, and under logit demand Jiang, Cao and Shen (2022, Proposition 5) found loss-averse single-product settings in which cyclic pricing is optimal. Guo, Jiang and Shen (2025) study the multi-product version under multinomial logit demand. For general parameters they show that an optimal steady state may fail to exist. This mission formalizes their positive result for one market: consumers who ignore gains, i.e. who do not respond to discounts. The paper motivates this case with luxury goods, where promotions can signal declining prestige.

Setting

A seller offers products $N=\{1,\dots,n\}$. Product $i$ has intrinsic utility $a_i\in\mathbb R$, price sensitivity $b_i>0$ and reference sensitivities $c_i^+\ge0$ (to gains) and $c_i^-\ge0$ (to losses). At price vector $\mathbf p$ and reference price vector $\mathbf r$, the utility of product $i$ is

$$u_i(\mathbf p,\mathbf r)=a_i-b_ip_i+c_i^+(r_i-p_i)_+-c_i^-(p_i-r_i)_+ ,$$

with $(x)_+=\max\{x,0\}$. The multinomial logit market share and the single-period revenue are

$$q_i(\mathbf p,\mathbf r)=\frac{e^{u_i(\mathbf p,\mathbf r)}}{1+\sum_{k\in N}e^{u_k(\mathbf p,\mathbf r)}},\qquad \Pi(\mathbf p,\mathbf r)=\sum_{i\in N}p_i\,q_i(\mathbf p,\mathbf r).$$

Prices and reference prices lie in the admissible box $\mathcal P^n=[0,p_H]^n$ with $p_H>0$. Reference prices follow exponential smoothing with memory $\alpha\in[0,1]$: $\mathbf r^{t+1}=\alpha\mathbf r^t+(1-\alpha)\mathbf p^t$. Revenue is discounted at rate $\beta\in[0,1)$, and the optimal value from reference price $\mathbf r^0$ is

$$V^\star(\mathbf r^0)=\sup_{(\mathbf p^t)_{t\ge0}\subset\mathcal P^n}\sum_{t\ge0}\beta^t\,\Pi(\mathbf p^t,\mathbf r^t).$$

The myopic policy $\mathbf p^m(\mathbf r)$ maximises $\Pi(\cdot,\mathbf r)$ over $\mathcal P^n$. An optimal steady state (Definition 4) is a price $\mathbf p^{\star\star}\in\mathcal P^n$ fixed by the optimal policy: holding the price at $\mathbf p^{\star\star}$ forever is optimal when the reference price is $\mathbf p^{\star\star}$.

Throughout §3–§4 the paper assumes the price ceiling is large enough: $p_H\ge\hat p_H$, where $\hat p_H$ is the root of

$$p=\chi+\sum_{i\in N}\frac{1}{b_i+c_i^+}\exp\big(a_i-b_ip+(b_i+c_i^+)\chi-1\big),\qquad \chi=\max_{i\in N}\frac{1}{b_i+\min\{c_i^+,c_i^-\}} .$$

Under this assumption the ceiling does not bind for the myopic problem.

Consumers are promotion-insensitive when $c_i^+=0$ for every $i$: a price below the reference brings no extra utility, while a price above it is penalised at rate $c_i^-\ge0$.

Formalization targets

Goal: Theorem 6 (p. 24)

If $c_i^-\ge c_i^+=0$ for all $i\in N$, then there exists $\mathbf p^{\star\star}\in\mathcal P^n$ with

$$V^\star(\mathbf p^{\star\star})\le\frac{\Pi(\mathbf p^{\star\star},\mathbf p^{\star\star})}{1-\beta}.$$

This holds for all parameters, memory and discount factors satisfying the hypotheses.

Milestone: the §4.2.1 observation (p. 24)

Under $c_i^+=0$ there is $\mathbf p^{\star\star}\in\mathcal P^n$ that is a fixed point of the myopic policy and whose diagonal pair attains the largest single-period revenue:

$$\Pi(\mathbf p,\mathbf r)\le\Pi(\mathbf p^{\star\star},\mathbf p^{\star\star})\qquad\text{for all }\mathbf p,\mathbf r\in\mathcal P^n .$$

Significance

Theorem 6 is the only general existence result for optimal steady states in the paper. Theorem 4 shows that a single gain-seeking product rules out any optimal steady state. Theorem 5 constrains where a steady state can lie when there is no gain-seeking product, but it does not say that one exists. Theorem 6 settles existence for promotion-insensitive markets, for every number of products and every parameter value: constant pricing is optimal in the long run regardless of parameters and initial reference prices. This holds even though the aggregate logit demand can be more sensitive to gains than to losses in some regions, which is exactly the situation in which earlier general guarantees for constant pricing do not apply.

The result is proved in the paper's online supplement (App. C.5), which is not part of the source file used here. It has no machine-checked proof. Formalizing it requires the first Lean treatment of reference-dependent MNL revenue, with a kinked utility, an outside option and an exponentially smoothed state. It also requires a sequence-form optimal value function for a deterministic infinite-horizon problem with a continuous state. The other missions of this series (myopic dynamics, optimality gap, gain-seeking cycles, steady-state structure, multi- versus single-price policies) use the same objects.

Difficulty

$\Pi(\mathbf p,\mathbf r)$ is neither concave nor monotone in a convenient way. Setting $c^+=0$ does not simply make the reference price irrelevant. Lowering a product's utility raises the logit revenue when that product's price is below the current revenue level, so a larger loss term can help. The joint maximisation over $(\mathbf p,\mathbf r)$ therefore does not reduce to "take $\mathbf r\ge\mathbf p$". The diagonal maximiser must also lie inside the box, and that is where the ceiling assumption $p_H\ge\hat p_H$, which involves the transcendental equation (9), enters. Finally, an optimal steady state is a statement about the infinite-horizon optimum $V^\star$, a supremum over all price sequences. It is not about the myopic policy, and a myopic fixed point is not in general an optimal steady state.

Formalization scope

Products are indexed by Fin n (the paper's product $i$ is index $i-1$), and vectors are Fin n → ℝ. The market shares (3) are defined directly. The Gumbel random-utility derivation is motivation only. Every statement carries the standing hypotheses of §2:

• $b_i>0$ and $c_i^\pm\ge0$ for all $i$;
• $\alpha\in[0,1]$ and $\beta\in[0,1)$ (Theorem 6 only);
• $p_H>0$;
• the ceiling assumption, stated as "some root $\hat p_H$ of (9) satisfies $\hat p_H\le p_H$", where $\chi$ is a supremum over Fin n (zero when $n=0$).

$V^\star$ is the supremum of the discounted revenue over all admissible price sequences rather than over stationary policies. For this deterministic problem with continuous revenue on a compact box the two values coincide. Optimal policies need not be unique, so an optimal steady state is stated as optimality of the constant price path: $\mathbf x\in\mathcal P^n$ and $V^\star(\mathbf x)\le\Pi(\mathbf x,\mathbf x)/(1-\beta)$. The milestone's "myopic fixed point" is stated as "$\mathbf p^{\star\star}$ maximises $\Pi(\cdot,\mathbf p^{\star\star})$ over the box", without fixing a myopic selection.

No trivializing reading is available. On the box $0\le\Pi\le p_H$, so the sequence family is bounded by $p_H/(1-\beta)$ and $V^\star$ is the genuine supremum, not Lean's default value $0$. The hypothesis is $c^+=0$ (no response to gains), not the opposite case $c^-=0$, and the conclusion is existence only, not uniqueness. A complete development needs bounds and continuity for the logit revenue, the joint single-period maximisation behind the milestone, and the comparison of the constant path with arbitrary sequences. The revenue model and the value function are reusable throughout the series. Proofs of either item, and of general facts about the shared model, are welcome.

Selected references

• M. A. Guo, H. Jiang, Z.-J. M. Shen, Multi-Product Dynamic Pricing with Reference Effects Under Logit Demand, Manufacturing & Service Operations Management, 2025; SSRN 4189049 (version of 2024-05-25). https://ssrn.com/abstract=4189049, https://doi.org/10.1287/msom.2024.0801
• G. Fibich, A. Gavious, O. Lowengart, Explicit Solutions of Optimization Models and Differential Games with Nonsmooth (Asymmetric) Reference-Price Effects, Operations Research 51(5):721–734, 2003.
• I. Popescu, Y. Wu, Dynamic Pricing Strategies with Reference Effects, Operations Research 55(3):413–429, 2007.
• J. Nasiry, I. Popescu, Dynamic Pricing with Loss-Averse Consumers and Peak-End Anchoring, Operations Research 59(6):1361–1368, 2011.
• Z. Hu, X. Chen, P. Hu, Dynamic Pricing with Gain-Seeking Reference Price Effects, Operations Research 64(1):150–157, 2016.
• Z. Hu, J. Nasiry, Are Markets with Loss-Averse Consumers More Sensitive to Losses?, Management Science 64(3):1384–1395, 2018.
• H. Jiang, J. Cao, Z.-J. M. Shen, Intertemporal Pricing via Nonparametric Estimation: Integrating Reference Effects and Consumer Heterogeneity, Manufacturing & Service Operations Management, 2022.

Motivation

In a budget-feasible procurement auction an auctioneer with a budget $B$ buys services from strategic sellers. Each seller knows privately what providing the service costs, and the auctioneer wants a set of services of maximum value without paying more than $B$ in total. The model was introduced by Singer (FOCS 2010) and is used to study crowdsourcing, data acquisition from individuals, and influence maximization in networks, where the value of a set of sellers typically shows diminishing returns: it is submodular.

Most of the mechanisms known for this problem are randomized, or are deterministic only when the auctioneer's valuation is monotone, i.e. adding a seller never lowers the value. Amanatidis, Kleer and Schäfer named the existence of deterministic budget-feasible constant-factor mechanisms for submodular valuations the most intriguing open problem of the area. Balkanski, Garimidi, Gkatzelis, Schoepflin and Tan (arXiv:2107.09239, Operations Research 2025) give deterministic clock auctions for these settings. In a clock auction each bidder only ever sees a sequence of decreasing take-it-or-leave-it prices, which makes truthful behaviour obvious to the bidders. This mission covers §4 of that paper: the first deterministic budget-feasible mechanism with a constant approximation ratio for general, not necessarily monotone, submodular valuations.

Timeline. Singer (2010) gave the first budget-feasible mechanisms for monotone submodular valuations. Chen, Gravin and Lu (SODA 2011) improved the constants. Amanatidis, Kleer and Schäfer (EC 2019) gave a randomized 505-approximate mechanism for non-monotone submodular valuations and introduced the idea of building two disjoint tentative sets simultaneously. Balkanski et al. (2021) give a deterministic clock auction for this class with approximation ratio 64.

Setting

There are $n$ bidders $N = \{0, \dots, n-1\}$. Bidder $i$ has a private cost $c_i \ge 0$, the least payment it accepts. The auctioneer has a budget $B > 0$ and a valuation $v : 2^N \to \mathbb{R}_{\ge 0}$ that is submodular: $v(S) + v(T) \ge v(S \cap T) + v(S \cup T)$ for all $S, T \subseteq N$. The marginal contribution of $T$ to $S$ is $v(T \mid S) = v(S \cup T) - v(S)$. A set $O$ is budget feasible if $\sum_{i \in O} c_i \le B$, and $OPT$ is the largest value of a budget-feasible set.

Simultaneous-Iterative-Pruning (Mechanism 3) works in phases with a target $\widetilde{OPT}_t$ that starts at $\max_i v(\{i\})$ and doubles in each phase. In phase $t$ it grows two disjoint tentative sets $S^1_t$ and $S^2_t$. At each step it picks a bidder $i$ and an index $k \in \{1,2\}$ maximizing $v(\{i\} \mid S^k_t)$, offers the price $p_i \leftarrow \min\{p_i,\ v(\{i\} \mid S^k_t)\cdot B/\widetilde{OPT}_t\}$, and adds $i$ to $S^k_t$ if it accepts. A bidder who rejects leaves the auction for good. A phase ends when one of the two sets reaches the target or no bidder remains to be offered a price. The two sets of the previous phase are set aside during a phase. After the last phase $\hat t$, an unconstrained submodular maximization subroutine $\mathrm{USM}$ is applied to the four sets of the last two phases, giving $T^k_j = \mathrm{USM}(S^k_j)$. The mechanism returns the best of the six sets $S^1_{\hat t-1}, S^2_{\hat t-1}, T^1_{\hat t}, T^2_{\hat t}, T^1_{\hat t-1}, T^2_{\hat t-1}$, minus its last added bidder if the prices of its bidders exceed $B$. The subroutine is required to be a 2-approximation: $\mathrm{USM}(X) \subseteq X$ and $2\,v(\mathrm{USM}(X)) \ge v(Y)$ for all $Y \subseteq X$.

Formalization targets

Goal: Theorem 5 (p. 12)

For every non-negative submodular $v$, costs $c \ge 0$, budget $B > 0$ and 2-approximate subroutine $\mathrm{USM}$, the set $S$ and prices $p$ returned by Simultaneous-Iterative-Pruning satisfy

$$\sum_{i \in S} p_i \le B \qquad\text{and}\qquad v(O) \le 64\, v(S) \ \text{ for every budget-feasible } O.$$

Milestones

• Lemma 6 (p. 12): the bidders of a budget-feasible $O$ rejected in phase $t \le \hat t$ have value $v(O^-_t) \le 6\,\widetilde{OPT}_t$. The page prints "$\ge$", a typo the proof corrects.
• Corollary 1 (p. 13): the bidders of $O$ still active at the end of phase $t$ have value $v(O^+_t) \ge v(O) - 12\,\widetilde{OPT}_t$.
• Lemma 7 (p. 13): one of the six candidates has value at least $v(O)/32$.
• Budget feasibility (p. 12): $\sum_{i \in S} p_i \le B$.
• Pruning step (p. 14): $v(S)$ is at least half the value of every candidate.

Significance

Theorem 5 shows that, for budget-feasible procurement with submodular valuations, determinism costs only a constant factor even without monotonicity. Before this paper no deterministic mechanism, polynomial-time or not, achieved a constant ratio for non-monotone submodular valuations. The mechanism is also a clock auction, whose interface to the bidders is a sequence of decreasing prices. The constant 64 is not claimed to be tight, and better constants are open.

No part of this paper is formalized anywhere that we know of. A machine-checked proof would verify an argument whose bookkeeping is easy to get wrong: two simultaneous tentative sets, sets of the previous phase put aside and later returned to the pool, prices that are lowered across phases, and a pruning step whose case analysis depends on the phase a candidate comes from. The formalization already surfaced two issues in the printed text. Lemma 6 states the wrong inequality. And for $n = 1$ it needs $v(\emptyset) = 0$, a normalization the paper never assumes.

Difficulty

The approach of the monotone case does not carry over. There, the value of the active optimal bidders is bounded by the value of all active bidders, and that fails once adding a bidder can lower the value. The proof therefore has to account separately for the optimal bidders the auction rejects (Lemma 6, which uses both tentative sets of a phase to absorb the rejected bidders) and for those it keeps, whose value is recovered only through the unconstrained maximization step applied to the four tentative sets of the last two phases (Lemma 7). Budget feasibility needs the fact that every accepted bidder's marginal contribution was non-negative when it was added. Otherwise its offered price would have been negative and it would have rejected. The final pruning step must not lose more than half the value. This holds because a removed bidder's marginal contribution is at most the initial target, while the best candidate exceeds twice that whenever a removal happens.

Formalization scope

Bidders are Fin n and sets of bidders are Finset (Fin n). The tentative sets are lists in insertion order, so that "the last bidder added" is defined; the candidate $T^k_j$ is the sublist of $S^k_j$ of the bidders that lie in $\mathrm{USM}(S^k_j)$. Valuations, costs and prices are real. The model's standing assumptions appear as hypotheses: $v \ge 0$, $v$ submodular (the published definition NonmonotoneSubmod.Shared.Submodular), and $c_i \ge 0$. A bidder offered the price $x$ accepts iff $c_i \le x$. Every argmax breaks ties by the least bidder index (in line 5, least bidder first, then $k = 1$ before $k = 2$; in line 12, the first maximizer in the printed order). The paper fixes no tie rule, and its claims hold for any.

Added hypotheses: $B > 0$ everywhere (the paper says only "a budget $B$"), and, in Lemma 6 only, "$n \ge 2$ or $v(\emptyset) = 0$", which excludes the one-bidder instances where the printed lemma fails. The theorems quantify over every subroutine $\mathrm{USM}$ with the 2-approximation guarantee. The paper's example of such a subroutine (Buchbinder et al.) is randomized, and a deterministic 2-approximation exists (Buchbinder and Feldman 2018). The phase loop runs with fuel $n + 2$. For non-negative submodular $v$ this is enough unless $\max_i v(\{i\}) = 0$, in which case $v \equiv 0$ and every statement is trivial.

Out of scope: running time (Lemma 12 and the "polynomial-time" clause) and the incentive properties. The clock-auction property is built into the definition, as every price update is a minimum with the old price. A Lean function is deterministic.

The goal cannot be satisfied trivially. It is stated about the mechanism's actual output for every non-negative submodular $v$ and every admissible subroutine, and the approximation compares $v(S)$ with every budget-feasible set rather than a supremum. Requiring $\mathrm{USM}$ to be an exact maximizer would weaken the theorem and is not done. Contributions of general lemmas on submodular functions (subadditivity of non-negative submodular functions, telescoping marginal sums along a list) are reusable well beyond this mission.

Selected references

• E. Balkanski, P. Garimidi, V. Gkatzelis, D. Schoepflin, X. Tan, Deterministic Budget-Feasible Clock Auctions, arXiv:2107.09239v2, 2021; Operations Research, 2025. https://arxiv.org/abs/2107.09239
• Y. Singer, Budget Feasible Mechanisms, FOCS 2010. https://doi.org/10.1109/FOCS.2010.78
• N. Chen, N. Gravin, P. Lu, On the Approximability of Budget Feasible Mechanisms, SODA 2011. https://arxiv.org/abs/1007.3801
• G. Amanatidis, P. Kleer, G. Schäfer, Budget-Feasible Mechanism Design for Non-Monotone Submodular Objectives: Offline and Online, EC 2019; Mathematics of Operations Research 47(3), 2022. https://arxiv.org/abs/1905.00848
• N. Buchbinder, M. Feldman, J. Naor, R. Schwartz, A Tight Linear Time (1/2)-Approximation for Unconstrained Submodular Maximization, SIAM J. Comput. 44(5), 2015. https://doi.org/10.1137/130929205
• N. Buchbinder, M. Feldman, Deterministic Algorithms for Submodular Maximization Problems, ACM Trans. Algorithms 14(3), 2018. https://doi.org/10.1145/3184990

Motivation

A portfolio manager who observes side information, the covariate $X$ (a market state, a set of signals), wants to choose a portfolio for the asset returns $Y$ given the current value $x_0$ of that covariate. Estimating the conditional law of $Y$ given $X=x_0$ from $N$ joint samples is fragile: typically no sample has $\hat x_i=x_0$ exactly, and a nearest-neighbour or kernel estimate inherits all the noise of the few samples near $x_0$. Nguyen, Zhang, Wang, Blanchet, Delage and Ye robustify this decision with optimal transport: they let an adversary perturb the empirical joint distribution within a transport budget and evaluate the portfolio by its worst conditional expected loss over the perturbed distributions. This mission formalizes their main reformulation result for the general case, a fiber of positive radius with a positive mass requirement.

Setting

Let $\mathcal X$ and $\mathcal Y$ be Polish spaces. The data are $N\ge1$ samples $(\hat x_i,\hat y_i)\in\mathcal X\times\mathcal Y$, $i\in[N]$, with empirical distribution $\hat{\mathbb P}=N^{-1}\sum_i\delta_{(\hat x_i,\hat y_i)}$. Ground costs $\mathbb D_{\mathcal X}$ and $\mathbb D_{\mathcal Y}$ give the joint cost $\mathbb D((x,y),(x',y'))=\mathbb D_{\mathcal X}(x,x')+\mathbb D_{\mathcal Y}(y,y')$, and the optimal transport cost $\mathbb W(\mathbb Q,\hat{\mathbb P})$ is the least expected cost $\mathbb E_\pi[\mathbb D]$ over couplings $\pi$ of $\mathbb Q$ and $\hat{\mathbb P}$. The ambiguity set is the ball

$$\mathbb B_\rho=\{\mathbb Q\in\mathcal M(\mathcal X\times\mathcal Y):\mathbb W(\mathbb Q,\hat{\mathbb P})\le\rho\}.$$

The neighbourhood of the observed covariate is $\mathcal N_\gamma(x_0)=\{x:\mathbb D_{\mathcal X}(x,x_0)\le\gamma\}$, and $\mathcal N_\gamma(x_0)\times\mathcal Y$ is the fiber set. For a fixed portfolio the loss is a function $\ell:\mathcal Y\to\mathbb R$, and the quantity of interest is the worst-case conditional expected loss

$$\sup\Big\{\mathbb E_{\mathbb Q}[\ell(Y)\mid X\in\mathcal N_\gamma(x_0)]:\ \mathbb Q\in\mathbb B_\rho,\ \mathbb Q(X\in\mathcal N_\gamma(x_0))\ge\varepsilon\Big\},$$

where $\varepsilon>0$ is a minimum mass the adversary must leave on the fiber, so that the conditional expectation is well defined.

Three more data enter the result. The minimum radius $\rho_{\min}(x_0,\gamma,\varepsilon)$ is the least $\mathbb W(\mathbb Q,\hat{\mathbb P})$ over $\mathbb Q$ with fiber mass at least $\varepsilon$. The index sets are $\mathcal I_1=\{i:\hat x_i\in\mathcal N_\gamma(x_0)\}$ and $\mathcal I_2=[N]\setminus\mathcal I_1$. The boundary distances are $d_i=\inf_{x\in\partial\mathcal N_\gamma(x_0)}\mathbb D_{\mathcal X}(x,\hat x_i)$. The dual set $\mathcal V$ (display (16)) consists of the tuples $(\lambda,s,\nu^+,\nu^-,\phi,\varphi,\psi)$ with $\lambda,\psi\in\mathbb R^N_+$, $s\in\mathbb R^N$, $\nu^\pm,\varphi\ge0$, $\phi\in\mathbb R$, subject to

$$\phi-d_i\varphi+\psi_i-s_i\ge0\ (i\in\mathcal I_1),\quad \phi+d_i\varphi+\psi_i-s_i\ge0\ (i\in\mathcal I_2),\quad \nu^+-\nu^-+\Big(\sum_{i\in\mathcal I_1}d_i-N\rho\Big)\varphi-\sum_i\psi_i\ge0,\quad \varphi\ge\lambda_i.$$

Formalization targets

Goal: Theorem 4.4

For $\gamma>0$, $\varepsilon>0$ and $\rho>\rho_{\min}(x_0,\gamma,\varepsilon)$,

$$\sup_{\substack{\mathbb Q\in\mathbb B_\rho\\ \mathbb Q(X\in\mathcal N_\gamma(x_0))\ge\varepsilon}}\mathbb E_{\mathbb Q}[\ell(Y)\mid X\in\mathcal N_\gamma(x_0)]=\inf\Big\{\phi+\frac{\nu^+}{N\varepsilon}-\frac{\nu^-}{N}:\ (\lambda,s,\nu^+,\nu^-,\phi,\varphi,\psi)\in\mathcal V,\ s_i\ge\sup_{y\in\mathcal Y}\{\ell(y)-\lambda_i\mathbb D_{\mathcal Y}(y,\hat y_i)\}\ \forall i\Big\}.$$

Milestones

1. Representation (24) of $\mathbb B_\rho$ as the set of averages $N^{-1}\sum_i\pi_i$ of probability measures with $N^{-1}\sum_i\mathbb E_{\pi_i}[\mathbb D(\cdot,(\hat x_i,\hat y_i))]\le\rho$.
2. Proposition 2.5: $\rho_{\min}$ is the value of a fractional knapsack linear program, and a feasible $\mathbb Q$ exists iff $\rho\ge\rho_{\min}$.
3. Reduction (proof of Theorem 4.4, pp. 48–49): the worst case equals a supremum over weights $p_i\in[0,1]$ and laws $\mu_0^i$ on $\mathcal Y$ of $\sum_ip_i\mathbb E_{\mu_0^i}[\ell]/\sum_ip_i$, under a transport budget and $\sum_ip_i\ge N\varepsilon$.
4. Conic duality (p. 50) for one sample: $\sup\{\mathbb E_{\mu}[\upsilon\ell]:\mathbb E_\mu[\upsilon\mathbb D_{\mathcal Y}(\cdot,\hat y)]\le\theta\}=\inf_{\lambda\ge0}\theta\lambda+\upsilon\sup_y\{\ell(y)-\lambda\mathbb D_{\mathcal Y}(y,\hat y)\}$ for $\theta>0$.
5. LP duality (29) (pp. 50–51): the supremum of $\sum_i\theta_i\lambda_i+\upsilon_is_i$ over the Charnes–Cooper variables $(\upsilon,t)$ and the budgets $\theta$ equals the infimum of $\phi+(N\varepsilon)^{-1}\nu^+-N^{-1}\nu^-$ over $\mathcal V$.

Significance

The theorem turns an infinite-dimensional problem, a supremum over probability measures on $\mathcal X\times\mathcal Y$ of a ratio of integrals, into a program in $O(N)$ real variables whose only infinite part is the per-sample supremum $\sup_y\{\ell(y)-\lambda_i\mathbb D_{\mathcal Y}(y,\hat y_i)\}$. For the losses used in portfolio selection (mean–variance, CVaR) this supremum has a closed form or a conic representation, and the outer minimization over portfolios becomes a single convex program; this is how the paper computes its conditional robust portfolios. It is the most general of the paper's four cases (Figure 1, p. 12); the companion missions of this series treat a singleton fiber ($\gamma=0$) and a zero mass requirement ($\varepsilon=0$).

The result is proved in the paper, not formalized anywhere. A machine-checked version requires, and would leave behind, an optimal-transport representation of Wasserstein balls around empirical measures, a Dirac-nominal conic duality for moment problems, and finite-dimensional linear programming duality, none of which is in Mathlib.

Difficulty

The conditional expectation is a ratio, so the problem is not a linear program in $\mathbb Q$ and the standard Wasserstein DRO duality does not apply directly. Passing to finitely many sample weights requires that leaving the fiber from a sample inside it costs exactly $d_i$, which depends on the geometry of the neighbourhood and not only on Assumption 2.4. The two duality steps are of different kinds: an infinite-dimensional one over laws on $\mathcal Y$, where the loss is only measurable, and a finite-dimensional linear program whose strong duality must be certified from $\rho>\rho_{\min}$. The representation of the ball needs an optimal coupling, which is an existence theorem on Polish spaces.

Formalization scope

• $\mathcal X$, $\mathcal Y$ are Polish Borel spaces; $[N]$ is Fin N with $N\ge1$; samples may repeat.
• $\mathbb W$ is the published RWPI.SqrtLasso.transportCost, an infimum over couplings of a lower integral of the $[0,\infty]$-valued cost; the ball compares it with ENNReal.ofReal ρ.
• Expectations of the loss are the published ModelRiskOT.Duality.extIntegral, $\int\ell^+-\int\ell^-$ in the extended reals. Both sides of the goal are extended reals; the infimum over an empty set is $+\infty$.
• The loss is an arbitrary measurable $L:\mathcal Y\to\mathbb R$, standing for $\ell(\cdot,\alpha,\beta)$ at any fixed feasible $(\alpha,\beta)$; no boundedness or continuity is assumed.
• Assumption 2.4 (separable, symmetric, nonnegative, continuous costs; unique projections onto $\mathcal N_\gamma(x_0)$; vicinity of boundary points) is a hypothesis of every statement. $\partial$ is the topological frontier in $\mathcal X$; $\kappa_i$ and $d_i$ are real infima.
• Added hypotheses. A boundary-regularity predicate: $\partial\mathcal N_\gamma(x_0)\ne\emptyset$, $d_i$ is the greatest lower bound of $\mathbb D_{\mathcal X}(x,\hat x_i)$ over $x\notin\mathcal N_\gamma(x_0)$ for $i\in\mathcal I_1$, and $d_i=\kappa_i$ for $i\in\mathcal I_2$. The proof uses both facts, and neither follows from Assumption 2.4 for a general continuous cost; both hold when $\mathbb D_{\mathcal X}$ is a norm distance. Measurability of $L$. In the conic duality milestone, $\theta>0$.
• Ruled out. The conditional expectation is never evaluated at a $\mathbb Q$ with zero fiber mass (the supremum ranges only over $\mathbb Q$ with mass at least $\varepsilon>0$); no Bochner integral of a possibly non-integrable loss appears; $\rho\ge0$ follows from $\rho>\rho_{\min}$, so ofReal never collapses a negative radius; and the supremum ranges exactly over $\mathbb B_\rho$ intersected with the mass constraint, not over all measures.
• Welcome contributions: existence of optimal couplings on Polish spaces, the decomposition of couplings with a finitely supported marginal, a Dirac-nominal moment duality, and LP strong duality in the form needed for (29). These are reusable well beyond this paper.

Selected references

• V. A. Nguyen, F. Zhang, S. Wang, J. Blanchet, E. Delage, Y. Ye, Robustifying conditional portfolio decisions via optimal transport, arXiv:2103.16451v3, 2024; Operations Research, 2025. https://arxiv.org/abs/2103.16451
• J. Blanchet, K. Murthy, Quantifying distributional model risk via optimal transport, Mathematics of Operations Research 44(2), 2019. https://arxiv.org/abs/1604.01446
• C. Villani, Optimal Transport: Old and New, Springer, 2009 (Theorem 4.1, existence of optimal couplings). https://doi.org/10.1007/978-3-540-71050-9
• A. Charnes, W. W. Cooper, Programming with linear fractional functionals, Naval Research Logistics Quarterly 9, 1962. https://doi.org/10.1002/nav.3800090303
• M. Sion, On general minimax theorems, Pacific Journal of Mathematics 8(1), 1958. https://doi.org/10.2140/pjm.1958.8.171

Motivation

A portfolio manager who observes side information, such as a vector of market covariates $x_0$ today, wants a decision that performs well conditionally on that information: the relevant risk is the expected loss of the portfolio given that the covariate equals, or is close to, $x_0$. Estimating this conditional loss from $N$ historical pairs $(\hat x_i,\hat y_i)$ of covariates and returns is fragile, since few or no samples may lie near $x_0$. Nguyen, Zhang, Wang, Blanchet, Delage and Ye (arXiv:2103.16451, Operations Research 2025) robustify the conditional decision with an optimal-transport ambiguity set: the worst case of the conditional expected loss is taken over all distributions within transport budget $\rho$ of the empirical distribution.

Conditioning makes this worst case delicate. The adversary may move mass away from the conditioning set, and a conditional expectation on a set of probability zero is undefined. Section 4.1 of the paper treats a neighbourhood of positive radius $\gamma$ around $x_0$ and requires only that the conditioning set have positive probability. This mission formalizes the result showing that, when the budget is below an explicit threshold $\rho_{\max}$, the requirement "positive probability" is automatically "probability at least $\underline\varepsilon$", with $\underline\varepsilon>0$ the value of a small linear program.

Setting

Let $\mathcal X$ and $\mathcal Y$ be Polish spaces carrying their Borel $\sigma$-algebras, with ground costs $\mathbb D_{\mathcal X}$ and $\mathbb D_{\mathcal Y}$ and the separable joint cost $\mathbb D((x,y),(x',y'))=\mathbb D_{\mathcal X}(x,x')+\mathbb D_{\mathcal Y}(y,y')$. The data are $N\ge1$ samples $(\hat x_i,\hat y_i)$, $i\in[N]$, and the empirical distribution is $\widehat{\mathbb P}=N^{-1}\sum_i\delta_{(\hat x_i,\hat y_i)}$.

The optimal transport cost $\mathbb W(\mathbb Q,\widehat{\mathbb P})$ is the infimum of $\mathbb E_\pi[\mathbb D]$ over couplings $\pi$ of $\mathbb Q$ and $\widehat{\mathbb P}$, and the ambiguity set is the ball $\mathbb B_\rho=\{\mathbb Q:\mathbb W(\mathbb Q,\widehat{\mathbb P})\le\rho\}$ of probability measures on $\mathcal X\times\mathcal Y$.

The covariate neighbourhood is $\mathcal N_\gamma(x_0)=\{x:\mathbb D_{\mathcal X}(x,x_0)\le\gamma\}$, and $\mathcal N_\gamma(x_0)\times\mathcal Y$ is the fiber set. For a loss $\ell:\mathcal Y\to\mathbb R$ (the loss $y\mapsto\ell(y,\alpha,\beta)$ of a fixed portfolio decision), the worst-case conditional loss under a mass requirement is

$$\sup_{\mathbb Q\in\mathbb B_\rho,\ \mathbb Q(X\in\mathcal N_\gamma(x_0))\ \ge\ \varepsilon}\ \mathbb E_{\mathbb Q}\big[\ell(Y)\mid X\in\mathcal N_\gamma(x_0)\big],$$

and problem (12) replaces "$\ge\varepsilon$" by "$>0$".

Two derived quantities organize §4.1. The maximal budget $\rho_{\max}(x_0,\gamma)$ is the least transport cost of a distribution that puts no mass on the fiber. Write $\mathcal I_1=\{i:\hat x_i\in\mathcal N_\gamma(x_0)\}$ and $\mathcal I_2$ for its complement, and let $d_i$ be the cost from $\hat x_i$ to the boundary $\partial\mathcal N_\gamma(x_0)$. Assumption 2.4 asks that the costs be symmetric, non-negative and continuous, with $\mathbb D=0$ exactly on the diagonal, that each $\hat x_i$ have a unique projection onto $\mathcal N_\gamma(x_0)$, and that every boundary point be approached from outside the neighbourhood.

Formalization targets

Goal: Proposition 4.3 (p. 19)

For $\gamma>0$ and $0\le\rho<\rho_{\max}(x_0,\gamma)$, let

$$\underline\varepsilon=\min\Big\{\tfrac1N\textstyle\sum_{i\in\mathcal I_1}p_i:\ p\in[0,1]^N,\ \tfrac1N\sum_{i\in\mathcal I_1}d_i(1-p_i)\le\rho\Big\}.$$

Then $\underline\varepsilon>0$, and for every loss $\ell$

$$\sup_{\mathbb Q\in\mathbb B_\rho,\ \mathbb Q(X\in\mathcal N_\gamma(x_0))>0}\mathbb E_{\mathbb Q}[\ell(Y)\mid X\in\mathcal N_\gamma(x_0)]=\sup_{\mathbb Q\in\mathbb B_\rho,\ \mathbb Q(X\in\mathcal N_\gamma(x_0))\ge\underline\varepsilon}\mathbb E_{\mathbb Q}[\ell(Y)\mid X\in\mathcal N_\gamma(x_0)].$$

Milestones

1. Display (24), p. 47: $\mathbb Q\in\mathbb B_\rho$ if and only if $\mathbb Q=N^{-1}\sum_i\pi_i$ for probability measures $\pi_i$ with $N^{-1}\sum_i\mathbb E_{\pi_i}[\mathbb D_{\mathcal X}(X,\hat x_i)+\mathbb D_{\mathcal Y}(Y,\hat y_i)]\le\rho$.
2. Proposition 4.1, p. 18: $\rho_{\max}(x_0,\gamma)=N^{-1}\sum_{i\in\mathcal I_1}d_i$.
3. Proof of Proposition 4.3, p. 47: for $\rho<\rho_{\max}$, $\inf_{\mathbb Q\in\mathbb B_\rho}\mathbb Q(X\in\mathcal N_\gamma(x_0))>0$.
4. Proof of Proposition 4.3, pp. 47–48: for $\rho>0$, $\inf_{\mathbb Q\in\mathbb B_\rho}\mathbb Q(X\in\mathcal N_\gamma(x_0))=\underline\varepsilon$.

Significance

Proposition 4.3 removes the degenerate constraint "positive probability" from the conditional robust problem whenever the budget is below $\rho_{\max}$. The degenerate constraint defines a feasible set that is not closed, and conditional expectations along it can involve divisions by arbitrarily small masses; after the reduction, the problem has a positive, explicitly computable mass requirement $\underline\varepsilon$, and the finite-dimensional dual reformulation of Theorem 4.4 (which needs a positive mass requirement) applies. Together with Proposition 4.2, which shows that above $\rho_{\max}$ the worst case degenerates to $\sup_y\ell(y,\alpha,\beta)$, it gives a complete picture of the regime $\gamma>0$, $\varepsilon=0$. The LP defining $\underline\varepsilon$ is a fractional knapsack problem, solvable greedily.

The paper proves these results; none of them has a machine-checked proof. The mission produces a formal account of the transport-ball representation (24) on Polish spaces, the closed form of $\rho_{\max}$, and the reduction itself. It also records, with explicit counterexamples, where the printed arguments need additional hypotheses (see Formalization scope).

Difficulty

The obvious argument fixes $\mathbb Q\in\mathbb B_\rho$, splits it as $N^{-1}\sum_i\pi_i$, and bounds the cost of the mass that each $\pi_i$ moves out of the fiber. Two steps resist. The splitting with the exact budget $\le\rho$ requires an optimal coupling, so attainment of the transport infimum on Polish spaces is needed. And the bound "moving a fraction $1-p_i$ of sample $i$ out of the fiber costs at least $d_i(1-p_i)$" needs the cost of leaving $\mathcal N_\gamma(x_0)$ from $\hat x_i$ to equal the boundary cost $d_i$, which is not implied by continuity of $\mathbb D_{\mathcal X}$. Identifying the infimal fiber mass with the LP value also requires approximating boundary points from outside the neighbourhood, so the LP minimum is approached but not attained by measures in the ball.

Formalization scope

Spaces are Polish with Borel $\sigma$-algebras; $[N]$ is Fin N with $N\ge1$; repeated samples are allowed. The transport cost is the published RWPI.SqrtLasso.transportCost (an infimum over couplings with first marginal $\mathbb Q$ and second marginal $\widehat{\mathbb P}$, lower Lebesgue integrals of a $[0,\infty]$-valued cost); the paper's "min" is not built into it. Expectations of the loss are $\int\ell^+-\int\ell^-$ in the extended reals (published ModelRiskOT.Duality.extIntegral). Worst-case values are suprema in EReal over probability measures. The loss is an arbitrary function $\ell:\mathcal Y\to\mathbb R$, which covers every decision $(\alpha,\beta)$. $\kappa_i$ and $d_i$ are infima (sInf), and $\partial$ is the topological frontier in $\mathcal X$.

Hypotheses beyond the page, all disclosed in the statements:

• Every statement about $\gamma>0$ carries Assumption 2.4 and a predicate BoundaryRegular: the boundary of $\mathcal N_\gamma(x_0)$ is nonempty, for $i\in\mathcal I_1$ the infimum of $\mathbb D_{\mathcal X}(x,\hat x_i)$ over $x\notin\mathcal N_\gamma(x_0)$ is $d_i$, and for $i\in\mathcal I_2$, $d_i=\kappa_i$. It holds for norm distances; without it Proposition 4.1 fails for some continuous costs.
• $\rho\ge0$, the paper's standing $\rho\in\mathbb R_+$.
• Milestone 4 is stated for $\rho>0$: at $\rho=0$ a sample on the boundary has $d_i=0$ but cannot be moved, and the identity fails.

The formalization excludes the trivializing readings: no conditional expectation is evaluated at a distribution with zero fiber mass, no Bochner integral of a possibly non-integrable loss is used, a negative $\rho$ cannot enter through ENNReal.ofReal, and the suprema range exactly over the probability measures of $\mathbb B_\rho$ satisfying the stated mass constraint. "Equivalent" is formalized as equality of the inner suprema for every loss, which is stronger than equality of the min–max values.

A complete development needs couplings and gluing for finitely supported marginals, existence of optimal couplings for continuous costs on Polish spaces, and finite LP facts (attainment, positivity). The transport-ball representation and the optimal-coupling existence are reusable beyond this mission. Proofs of any milestone, and of the representation (24) in particular, are welcome.

Selected references

• V. A. Nguyen, F. Zhang, S. Wang, J. Blanchet, E. Delage, Y. Ye, Robustifying conditional portfolio decisions via optimal transport, arXiv:2103.16451v3, 2024; Operations Research, 2025. https://arxiv.org/abs/2103.16451
• C. Villani, Optimal Transport: Old and New, Grundlehren der mathematischen Wissenschaften 338, Springer, 2009. https://doi.org/10.1007/978-3-540-71050-9
• J. Blanchet, K. Murthy, Quantifying distributional model risk via optimal transport, Mathematics of Operations Research 44(2), 2019. https://doi.org/10.1287/moor.2018.0936