All missions

The Karush–Kuhn–Tucker conditions are the central result of convex optimization: for a convex differentiable problem satisfying Slater's condition, a point is optimal exactly when primal feasibility, dual feasibility, complementary slackness and Lagrangian stationarity hold. This mission formalizes Chapters 4–5 of Boyd & Vandenberghe end to end — the first-order optimality criterion, concavity of the Lagrange dual, weak duality, Slater's strong-duality theorem with dual attainment (via the separating-hyperplane argument of §5.3.2), the saddle-point characterization, sensitivity bounds and Pareto scalarization — culminating in the full KKT characterization.

Linear programming has a complete duality theory; integer programming does not — and the Lagrangean dual measures exactly how far duality reaches. This mission formalizes the duality theory of integer programming from Section 11.4 of Bertsimas–Tsitsiklis, built on the general linear programming duality of Section 4.10. For the integer program

with integer data, the complicating constraints $Ax \ge b$ are dualized with multipliers $p \ge 0$ over the tractable set $X = \{x \text{ integer} \mid Dx \ge d\}$: the dual function is

and the Lagrangean dual is $Z_D = \max_{p \ge 0} Z(p)$. Weak duality $Z_D \le Z_{IP}$ (Theorem 11.2) always holds, but strong duality can fail. The convex hull $CH(X)$ of the integer points of a polyhedron with integer data is itself a polyhedron (Theorem 11.3, Meyer's theorem), and the capstone — Theorem 11.4, the central result of Section 11.4 — identifies the Lagrangean dual exactly: $Z_D$ equals the optimal cost of the linear program

. This is the geometric explanation of the strength of Lagrangean relaxation, yields the bound ordering $Z_{LP} \le Z_D \le Z_{IP}$, and Corollary 11.1 characterizes exactly when the bounds collapse. The polyhedral engine is the general weak/strong duality pair (Theorems 4.17/4.18) over a primal $\min c'x$ s.t. $Ax \ge b$, $x \in P = \{x \mid Dx \ge d\}$, and the formulation-strength comparison $P_{sub} \subseteq P_{cut}$ of Theorem 10.1 supplies the motivating principle that tighter relaxations of the same integer set give sharper bounds.

How can an unbounded polyhedron be described by finitely many geometric objects? Sections 4.8-4.9 of Bertsimas-Tsitsiklis build the cone machinery: recession cones $\{d \mid Ad \ge 0\}$ and their rays, extreme rays (defined, like basic solutions, by $n-1$ linearly independent active constraints), the pointedness criterion (Theorem 4.12: $0$ is an extreme point of a polyhedral cone iff the cone contains no line iff $n$ of the constraint vectors are linearly independent), and the characterization of unbounded linear programs (Theorems 4.13-4.14: over a pointed polyhedral cone, and then over any polyhedron with an extreme point, the optimal cost is $-\infty$ iff some extreme ray $d$ has $c'd < 0$). The capstone is the resolution theorem (Theorem 4.15): a nonempty polyhedron $P$ with at least one extreme point equals $Q = \{\sum_i \lambda_i x^i + \sum_j \theta_j w^j \mid \lambda_i \ge 0, \theta_j \ge 0, \sum_i \lambda_i = 1\}$ — the convex hull of its extreme points plus the cone generated by a complete set of its extreme rays. It specializes to Theorem 2.9 / Corollary 4.4 (a nonempty bounded polyhedron is the convex hull of its extreme points) and Corollary 4.5 (a pointed polyhedral cone is generated by its extreme rays). The converse, Theorem 4.16, states that every finitely generated set is a polyhedron — in particular the convex hull of finitely many vectors is a polyhedron. Together these form the Minkowski-Weyl equivalence of the two representations of polyhedra, verified absent from Mathlib and the genuine content of this mission.

Matrix completion — recovering a low-rank matrix $M = ZZ^\top$ from a small random subset of its entries — powers recommender systems and collaborative filtering. In practice it is solved by running (stochastic) gradient descent on the non-convex objective

where $\Omega=\{(i,j)|M_{i,j} \text{ is observed}\}$ and $R(X)$ is a certain regularizer. from a random starting point, and it just works.

Ge, Lee and Ma (NeurIPS 2016 Best student paper award) explained why: the regularized objective has no spurious local minima — every local minimum is global and exactly recovers $M$. This mission formalizes that landmark theorem in Lean 4, in its strongest known form and along its simplest known proof: the unified landscape analysis of Ge–Jin–Zheng (ICML 2017) and an improved sampling bound in Chen–Li (JMLR 2019). Conditional on an explicit good-sample predicate (which holds with high probability under Bernoulli sampling), every local minimum $X$ of $f$ satisfies $XX^\top = ZZ^\top$.

Bandit feedback is only one point on a spectrum: a learner might see more than its own loss (full information) or less (a spam filter never learns what happened to mail it deleted). Chapter 37 of Lattimore–Szepesvári studies finite adversarial games $G = (\mathcal{L}, \Phi)$ where the loss matrix and the feedback matrix are decoupled. The goal theorem is the celebrated classification theorem: every finite partial-monitoring game has minimax regret exactly $0$, $\Theta(\sqrt{n})$, $\Theta(n^{2/3})$ or $\Omega(n)$ — determined by two purely combinatorial conditions, global and local observability, on the game's neighbourhood structure. A single geometric dichotomy thus governs the price of information in every online decision problem with finite actions and feedback.

When actions are feature vectors and the mean reward is linear — $X_t = \langle \theta_*, A_t\rangle + \eta_t$ — a bandit can generalize across arms: pulling one arm reveals information about all of them. Chapter 19 of Lattimore–Szepesvári carries the optimism principle into this setting: LinUCB (a.k.a. OFUL) plays the action maximizing $\max_{\theta\in\mathcal{C}_t}\langle\theta, a\rangle$ over the confidence ellipsoid $\mathcal{C}_t$ of Mission IX. The goal theorem: with probability $1-\delta$, $\hat R_n \le \sqrt{8n\beta_n \log\frac{\det V_n}{\det V_0}} \le \sqrt{8dn\beta_n\log\frac{d\lambda + nL^2}{d\lambda}}$ — regret $\tilde O(d\sqrt{n})$ independent of the number of actions. The combinatorial engine is the elliptical potential lemma, bounding how many times adaptively chosen directions can be surprising. Chapter 22's phased elimination with G-optimal design (Mission IX) sharpens this to $\tilde O(\sqrt{dn\log k})$ for finite action sets.

Least-squares estimation from adaptively collected data is the statistical heart of linear bandits: the actions $A_t$ depend on past noise, so classical fixed-design theory does not apply. Chapter 20 of Lattimore–Szepesvári resolves this with the method of mixtures: the process $M_t(x) = \exp(\langle x, S_t\rangle - \frac{1}{2}\|x\|^2_{V_t(\lambda)})$ is a supermartingale, and integrating over a Gaussian mixture yields the self-normalized bound — the goal theorem — $\mathbb{P}\big(\exists t : \|S_t\|^2_{V_t(\lambda)^{-1}} \ge 2\log\frac{1}{\delta} + \log\frac{\det V_t(\lambda)}{\lambda^d}\big) \le \delta$, valid uniformly over all times. The resulting confidence ellipsoids for the regularized least-squares estimator (Abbasi-Yadkori et al.) calibrate every algorithm of Mission X. The mission also formalizes the Kiefer–Wolfowitz theorem of Chapter 21: G-optimal and D-optimal experimental designs coincide, with optimal value exactly $d$ — the classical equivalence theorem of optimal design theory.

Motivation

Itô's lemma is the stochastic chain rule. It identifies the additional drift created when a nonlinear function is applied to a process with Brownian fluctuations. This second-order correction is central to stochastic differential equations, martingales and mathematical finance. The Wikipedia article discusses the scalar formula, multidimensional and jump extensions, geometric Brownian motion, stochastic exponentials, product rules and Black–Scholes.

The mission will formalise these statements in a dependency-first Lean 4 development. Wikipedia supplies the topic map; rigorous proof obligations use stochastic integration and quadratic variation. Rémy Degenne's BrownianMotion and MathFin are independently developed Lean comparison sources. Their exact scopes and pinned dependencies must be audited before import or adaptation.

A live Prove2Me catalogue audit on 26 October 2026 found accepted Brownian-increment, elementary Itô-integral, isometry, continuous-modification and time-independent vector Itô-formula theorems at the same Mathlib revision. Those results are reusable prerequisites, so the new mission concentrates on the time-dependent and semimartingale gaps. The full time-dependent multidimensional continuous-semimartingale theorem is an existing Open target.

Setting

Let $(\Omega,\mathcal F,(\mathcal F_t)_{t\ge0},\mathbb P)$ be a filtered probability space with the usual conditions, and $B$ a real Brownian motion adapted to the filtration. Fix a deterministic finite horizon $T$. Initially let $\mu,\sigma$ be bounded adapted continuous real processes. Their integrals define

Let $f:[0,T]\times\mathbb R\to\mathbb R$ be $C^{1,2}$, with continuous derivatives $f_t,f_x,f_{xx}$ satisfying sufficient boundedness/integrability assumptions. The principal capstone proves, for each deterministic $t\le T$, almost surely,

A later milestone uses continuous modifications to strengthen this to one probability-one event for all $t\in[0,T]$. The notation $(dB)^2=dt$ describes quadratic variation in a probabilistic limit, not pointwise differential equality. No formal process definition may assume the identity it is supposed to prove.

Formalization targets

Brownian motion and quadratic variation

Reuse exact compatible Prove2Me Brownian-process results and pinned Mathlib declarations. Prove increment moment and independence identities, deterministic partition quadratic-variation convergence $\sum_{\pi_n}(B_v-B_u)^2\to T$ in $L^2$ or probability, weighted quadratic-variation convergence and vanishing drift-Brownian covariation. State the convergence mode and partition assumptions for each theorem.

Stochastic-integral construction and isometry

Audit and reuse the Prove2Me results for predictable simple-process integration, representation independence and the elementary isometry; establish new statements only for missing mathematical interfaces or stronger conditions: $\mathbb E[(\int_0^T H_s\,dB_s)^2]=\mathbb E[\int_0^T H_s^2\,ds]$ for square-integrable predictable $H$. A central theorem is the isometry in integral form:

Extend by completion and establish centred martingale, adaptedness and continuous-version results. External packages cannot be assumed present in Prove2Me; importable prerequisites must be published and remotely verified.

Brownian scalar and time-dependent chain rules

First prove the formula for $g(B_t)$ with the $\tfrac12 g''$ correction and bounded derivatives, then for $f(t,B_t)$ with additional $f_t$. Prove convergence of the Taylor remainder rigorously. Unbounded-derivative and local-martingale statements remain distinct extensions.

Adapted diffusion capstone

First use the accepted time-independent vector formula on an augmented process with coordinates $(t,X_t)$, clock drift one and zero clock diffusion. This gives a globally $C^2$ time-dependent case under the vector theorem's boundedness assumptions. Then extend the spatially second-order formula to $C^{1,2}$ test functions by a separately justified approximation that does not demand a second time derivative. Prove the displayed integral identity for $X=x_0+\int\mu ds+\int\sigma dB$, bounded adapted continuous coefficients and suitable $C^{1,2}$ hypotheses. Subsequently strengthen the fixed-time almost-sure result to indistinguishable continuous process versions, and extend by stopping-time localisation to more general coefficients and functions.

Product rule, squares and exponentials

Prove the product rule $d(XY)=X\,dY+Y\,dX+d[X,Y]$ and $d(B_t^2)=2B_t\,dB_t+dt$. Verify that $S_t=S_0\exp((\mu-\sigma^2/2)t+\sigma B_t)$ solves geometric Brownian motion's SDE for constant coefficients, and derive the logarithmic correction under positivity, using localisation where derivative growth requires it.

Multidimensional diffusion

For a $d$-dimensional process driven by $m$-dimensional Brownian motion with drift $b$ and matrix $G$, prove the covariance cross-terms and $df=[f_t+\nabla f\cdot b+\frac12\operatorname{tr}(G^\top Hf\,G)]dt+(\nabla f)^\top G\,dB$. Dimensions, orientation, smoothness and measurability are explicit. Do not use the target formula itself as a hypothesis.

Jumps and discontinuous semimartingales

As a separate advanced branch, prove finite-activity jump corrections, reusing the Lévy-process mission if its results are accepted. A general càdlàg semimartingale extension must distinguish continuous quadratic variation $[X]^c$, left limits $X_{s-}$ and the sum of exact jump remainders $f(X_s)-f(X_{s-})-f'(X_{s-})\Delta X_s$. This extension does not obstruct the continuous-diffusion capstone.

Black–Scholes application

Under precise self-financing, trading, asset-price, volatility and bank-account assumptions, derive delta-hedging identities and the Black–Scholes PDE from the diffusion formula. Reuse any compatible theorem in the financial-derivatives mission programme.

The intended graph is Brownian laws → stochastic integral/isometry and quadratic variation → Brownian chain rules → adapted-diffusion capstone → products/exponentials and higher-dimensional applications. Jump and option-pricing milestones have additional dependencies and are not prerequisites of the core scalar theorem.

Significance

The classical scalar Itô theorem is already established mathematically in the literature, while the proposed Prove2Me formalisation remains unverified. The MathFin project provides a relevant checked comparison development. The result supplies an importable stochastic-calculus foundation for SDEs, diffusion generators, mathematical finance and insurance risk. In particular it can support future stochastic verification in the spectrally negative Lévy dividend mission, subject to its separate jump and filtration assumptions. MathFin reports fixed-time adapted-coefficient and time-dependent Brownian Itô theorems, but its own scope notes distinguish unbounded functions such as exponential and square functions, and record that its two-dimensional version is a reduced core. These are useful nontrivial extension targets. External build claims do not constitute Prove2Me proof acceptance.

Difficulty

Core challenges include adapting already accepted integration and quadratic-variation interfaces, closing the clock-augmentation bridge, controlling the $C^2$-to-$C^{1,2}$ approximation, Taylor remainders, almost-sure event quantifiers and localisation. The multidimensional formula needs correct covariance rather than coordinatewise increments alone. Jump formulas need exact left-limit and compensation conventions. The Wikipedia presentation contains heuristic differential manipulations; every Lean target must be stated as an integral or precisely quantified convergence identity. Pinned-environment imports, declarations and types require independent remote validation.

Formalization scope

The central mission is the genuine real-valued time-dependent Itô formula for continuous Brownian drift-diffusions on a finite horizon, initially with bounded coefficients and derivatives. The underlying stochastic integrals are mathematically defined, and the identity is an independently proved conclusion. Stronger growth, time-quantifier, dimension and jump cases are staged as separate milestones with their own prerequisites. No vacuous model, circular field assumption, deterministic-only case or restatement with the desired result assumed can discharge the capstone.

The Prove2Me environment is pinned to Mathlib revision 0df444a360eaa60ab8c11dca51a86af692955474. External BrownianMotion/MathFin imports are research references until exact compatibility is demonstrated. Already-Proved Prove2Me Itô and Brownian theorems should be imported or cited directly after source-identity verification; their statements are not to be republished under new names. Create private unconfirmed items, audit reusable accepted declarations and theorem-source correspondence, validate each declaration remotely and read back the draft before human confirmation. Draft, elaborated, proved, published and reviewed are distinct states. Do not automatically submit for moderator review.

Selected references

• Wikipedia contributors, Itô's lemma, Wikipedia, 2026. https://en.wikipedia.org/wiki/It%C3%B4%27s_lemma (accessed 26 October 2026).
• Rémy Degenne, BrownianMotion: Construction of a Brownian Motion in Lean, Lean 4 software, 2026. https://github.com/RemyDegenne/brownian-motion (accessed 26 October 2026).
• Mathlib contributors, BrownianMotion.Basic documentation, Mathlib 4, 2026. https://leanprover-community.github.io/mathlib4_docs/Mathlib/Probability/BrownianMotion/Basic.html (accessed 26 October 2026).
• Raphael Coelho and contributors, MathFin: The Lean Financial Mathematics Library, software, 2026. https://github.com/formal-applied-math/formal-mathfin (Apache-2.0, accessed 26 October 2026).
• Rémy Degenne, Stochastic Integral and Itô's Lemma for Semimartingales, project intention, 4 July 2026. https://github.com/leanprover-community/project-intentions/issues/24.

Motivation

Many tasks in computational biology ask for a short pattern that occurs, with few errors, in each of a family of DNA or protein sequences: locating binding sites, finding conserved regions in unaligned sequences, designing PCR primers and genetic probes, and searching for a drug sequence that binds to a set of pathogen genomes. With Hamming distance as the error measure, two basic problems arise. Closest String asks for one string close to all inputs, and Closest Substring asks for one string close to some window of each input. Closest String is NP-hard (Frances and Litman, 1997), so Closest Substring is too, and both are studied for their approximability.

Timeline.

• 1997–1999: LP relaxation with randomized rounding gives near-optimal centers for Closest String when the optimal radius is large, super-logarithmic in the number of strings (Ben-Dor, Lancia, Perone and Ravi, 1997). Ratio-$4/3$ algorithms follow for all radii (Gąsieniec, Jansson and Lingas, SODA 1999; Lanctot, Li, Ma, Wang and Zhang, SODA 1999). For Closest Substring the known ratios are a trivial $2$ (Lanctot et al.) and then $2-\frac{2}{2|\Sigma|+1}$ (Li, Ma and Wang, STOC 1999).
• 2000: Li, Ma and Wang give polynomial-time approximation schemes for both problems (arXiv:cs/0002012; journal version J. ACM 49(2), 2002). The Closest Substring scheme is randomized.

This mission formalizes the Closest Substring scheme, Theorem 9 of the preprint.

Setting

Fix a finite alphabet $\Sigma$. A string of length $m$ is a map $\{1,\dots,m\}\to\Sigma$, and $d(s,s')$ is the number of positions where $s$ and $s'$ differ. For a set $T$ of positions, $d^T(u,v)$ counts the positions of $T$ where $u$ and $v$ differ. For a position multiset $R$, $d^R(u,v)$ counts the entries of $R$, with multiplicity, where they differ.

An instance of Closest Substring is $n\ge1$ strings $s_1,\dots,s_n$ of length $m$ and an integer $1\le L\le m$. A length-$L$ substring $t\sqsubseteq s_i$ is a window $s_i[p+1]\cdots s_i[p+L]$. The cost of a center $c\in\Sigma^L$ is

and $d_{\mathrm{opt}}=\min_{c\in\Sigma^L}\mathrm{cost}(c)$.

Algorithm closestSubstring (Figure 3) has an integer $r\ge2$ and a real $\varepsilon>0$ as constants. For every admissible tuple of $r$ length-$L$ substrings $t_{i_1},\dots,t_{i_r}$ (repeats allowed, but two entries from the same $s_i$ coincide) it does the following.

1. It forms the agreement set $Q=\{j: t_{i_1}[j]=\dots=t_{i_r}[j]\}$ and its complement $P$.
2. It draws a multiset $R$ of $k=\lceil (4/\varepsilon^2)\ln(nm)\rceil$ independent uniform positions of $P$.
3. For every $y\in\Sigma^k$, it picks in each $s_i$ a substring $t'_i$ minimizing $d(y,t'_i|_R)\,|P|/|R|+d(t_{i_1}|_Q,t'_i|_Q)$.
4. It solves problem (8),

within additive error $\varepsilon|P|$. 5. It proposes the candidate $s'$ with $s'|_P=x$ and $s'|_Q=t_{i_1}|_Q$.

The length-$L$ substrings of $s_1$ are also candidates. The output is a candidate of minimum cost.

Formalization targets

Goal: Theorem 9

For every $\Sigma$, $r\ge2$ and $\varepsilon>0$:

for every instance and every solver of (8) within error $\varepsilon|P|$. In addition, some $c=c(|\Sigma|,r,\varepsilon)$ bounds the number of candidates, and hence of solver calls, by $c\,(nm+1)^c$. The constants are those the proof derives. Taking $\frac1{2r-1}+3\varepsilon r\le\delta$ gives the paper's "$(1+\delta)$ with high probability, in polynomial time".

Milestones, in proof order

• Claim 2, Claim 3 and Lemma 1, the combinatorial core: if $\max_{i,j}d(t_i,t_j)>(1+\frac1{2r-1})d_{\mathrm{opt}}$, some $r$-tuple's agreement set carries an almost optimal center.
• The bound $|P|\le r\,d_{\mathrm{opt}}$.
• Lemmas 4 and 5 (Chernoff bounds).
• The sampling tails (11)–(12).
• Fact 2: with probability $\ge1-2(nm)^{-1/3}$, $d(s^*,t'_i)\le d(s^*,t_i)+2\varepsilon|P|$ for all $i$.
• The deterministic chain (15)–(16).
• The randomized-rounding bound from the proof of Lemma 6.

Significance

The result. Theorem 9 shows that Closest Substring, an NP-hard problem, can be approximated within any factor $1+\delta$ in polynomial time. Earlier algorithms only reached ratios near $2$. The method works by guessing the right $r$ windows and the center's letters on a logarithmic random sample, and then solving a smaller problem on the remaining positions.

Formalizing it. The theorem is proved on paper; no machine-checked proof of it or of the Closest String scheme is known to exist. A formal proof checks three things the paper leaves implicit:

• the union bound over all windows and all strings that yields the exponent $-1/3$;
• the interaction of the random multiset with the exhaustive guess $y$;
• the bookkeeping that turns the additive errors $2\varepsilon|P|$ and $\varepsilon|P|$ into $3\varepsilon r\,d_{\mathrm{opt}}$.

Lemma 1 and Claims 2–3 also give the Closest String scheme (Theorem 7) once Lemma 6's solver is formalized.

Difficulty

The obvious idea is to apply the Closest String method to the substrings. It fails because problem (8) needs the right window of every input string, which are the closest substrings $t_i$ of an unknown optimum. There are $(m-L+1)^n$ choices of windows, too many to try. Random sampling replaces that search, but the selection rule of step 1(c)(i) only sees a sample of $P$. It must be shown that every window that is much worse than $t_i$ on the full string also scores worse on the sample, simultaneously for all windows and strings. This needs concentration bounds whose constants match the sample size $\lceil(4/\varepsilon^2)\ln(nm)\rceil$ exactly.

The combinatorial Lemma 1 is the other obstacle. The obvious averaging over $r$-tuples does not give the factor $1/(2r-1)$; the telescoping of Claims 2 and 3 is needed.

Formalization scope

Strings are Fin m → A with 0-based positions, and distance is Mathlib's hammingDist. Substrings are indexed by start position. Position multisets are Fin k → Fin L. The ratios $\rho_k$ of Section 2 are stored multiplied by $d$, so $d_{\mathrm{opt}}=0$ needs no division. Index tuples may repeat indices: the paper's "distinct" reading of Claim 3 fails when $n<r+1$. The logarithm is natural, and $n\ge1$, $1\le L\le m$.

The randomness is one independent multiset per admissible tuple, each with i.i.d. uniform entries on $P_\tau$. When $P_\tau=\emptyset$, $R_\tau$ is a fixed multiset that is never read. Ties in step 1(c)(i) go to the smallest start position (Fact 2 is stated for every minimizer). The output is any minimizer of cost.

The solver of (8) is a parameter. It receives only the instance (the strings $t'_i$, the set $P$, the offsets) and must return $x$ with $d(t'_i|_P,x)+\text{offset}_i\le d_0+\varepsilon|P|$ for all $i$. The exact minimizer qualifies, and so does Lemma 6's method. "Polynomial time" is formalized as a polynomial count of candidates and solver calls. The solver's own running time (LP solving and derandomized rounding) has no machine model here and is outside the statement, as is the remark that Figure 3 can be derandomized.

The algorithm never receives an optimal center, the optimal windows or $d_{\mathrm{opt}}$. A version that did, or a probability taken over "some" multiset rather than the algorithm's law, or a solver hypothesis mentioning the optimum, would make the goal trivial. All three are ruled out by the definitions.

Needed infrastructure:

• finite product measures and Hoeffding/Chernoff bounds (Mathlib's measure_sum_ge_le_of_iIndepFun; the platform's HighDimProb.Concentration.chernoff and ComputationalLearning.chernoff_bounds are usable tools);
• marginals of Measure.pi;
• a union bound;
• elementary counting with Finset.filter.

Lemmas 4–5, (11)–(12) and the rounding bound are reusable beyond this mission. Contributions to any milestone are welcome, in particular to the concentration lemmas and to Lemma 1.

Selected references

• M. Li, B. Ma, L. Wang, On the Closest String and Substring Problems, arXiv:cs/0002012v1, 2000. https://arxiv.org/abs/cs/0002012 (journal version: J. ACM 49(2):157–171, 2002, https://doi.org/10.1145/506147.506150).
• M. Frances, A. Litman, On covering problems of codes, Theory of Computing Systems 30:113–119, 1997 (reference [4] of the preprint, listed at https://arxiv.org/abs/cs/0002012).
• A. Ben-Dor, G. Lancia, J. Perone, R. Ravi, Banishing bias from consensus sequences, CPM 1997, pp. 247–261 (reference [1] of the preprint).
• K. Lanctot, M. Li, B. Ma, S. Wang, L. Zhang, Distinguishing string selection problems, SODA 1999, pp. 633–642 (reference [11] of the preprint).
• R. Motwani, P. Raghavan, Randomized Algorithms, Cambridge University Press, 1995. https://doi.org/10.1017/CBO9780511814075

Motivation

Bike-sharing and car-sharing systems, and ride-hailing platforms, all move a fixed fleet of units between stations. Every ride takes a unit away from its origin and leaves it at its destination, so demand that is unbalanced across stations drains some stations and floods others. Pricing is the main lever an operator has: raising the price of rides out of a depleted station throttles the outflow. Choosing such prices optimally is hard, because the optimal policy may react to the full system state, a placement of $m$ units over $n$ stations, of which there are $\binom{m+n-1}{n-1}$.

Banerjee, Freund and Lykouris (arXiv:1608.06819v4, Operations Research 2022) give an approximation framework for this control problem. Their first result, Theorem 15, shows that one convex program yields state-independent prices whose steady-state performance is within a factor $m/(m+n-1)$ of the best state-dependent policy. The guarantee holds simultaneously for throughput, social welfare and revenue under regular demand.

Timeline. Gordon and Newell (1967) gave the product-form stationary law of closed queueing networks. Whitt (1984) observed that balanced closed networks give every node availability $m/(m+n-1)$. George and Xia (2011) studied availability in vehicle-rental networks via closed queueing networks. Waserhole and Jost (2014) proved the $m/(m+n-1)$ guarantee for throughput. Banerjee, Freund and Lykouris extended it to concave reward curves, and to travel times and other controls.

Setting

There are $n$ nodes and $m$ units. A state is $x\in S_{n,m}=\{x\in\mathbb N_0^n:\sum_ix_i=m\}$. Customers wishing to travel from $i$ to $j$ arrive at node $i$ at rate $\varphi_{ij}\ge0$. A quantile $q_{ij}\in[0,1]$ is the fraction of them willing to pay the quoted price. A customer who accepts engages a unit at $i$ if one is present, moving the system from $x$ to $x-e_i+e_j$.

A state-dependent policy chooses quantiles $q_{ij}(x)\in[0,1]$ at every state, with $q_{ij}(x)=0$ when $x_i=0$. A stationary law $\pi$ is a probability vector on $S_{n,m}$ satisfying the balance equation (1):

Rewards are given by per-ride rewards $I_{ij}$, functions of the quantile, with reward curves $R_{ij}(q)=q\,I_{ij}(q)$. The steady-state objective (2) is

and $\mathrm{Opt}_m$ is its best value over all state-dependent policies and their stationary laws.

The elevated flow relaxation (Algorithm 1) drops availability from the objective and adds a flow-conservation constraint:

A feasible $q$ has balanced demand. Its optimum $\tilde q$ is then quoted as a fixed price at every non-empty station.

Formalization targets

Goal: Theorem 15

If every $R_{ij}$ is concave on $[0,1]$, $\tilde q$ is an optimal solution of Algorithm 1 whose support graph $\{(a,b):a\ne b,\ \varphi_{ab}\tilde q_{ab}>0\}$ is strongly connected, and $\tilde\pi$ is a stationary law of $\tilde q$, then for every state-dependent policy $q$ and every stationary law $\pi$ of it,

The connectivity hypothesis is the paper's standing irreducibility assumption, and the printed statement is false without it.

Milestones

These follow the paper's own sequence:

• Propositions 7 and 8 (demand bounding, supply circulation);
• Lemma 9, $\widehat{\mathrm{Obj}}(\tilde q)\ge\mathrm{Opt}_m$;
• the reduction of a state-independent policy to a Gordon–Newell network (§2.3) and the Gordon–Newell theorem (Theorem 2, an already proved platform theorem);
• Lemma 3, availability in product-form networks;
• Lemma 13, a weighted bipartite graph between $S_{n,m}$ and $S_{n,m-1}$;
• Lemma 14, $A_m=r_{\max}G_{m-1}/G_m\ge m/(m+n-1)$;
• Proposition 6, infinite-unit availabilities $r_i/\max_jr_j$;
• Lemma 10, equal availabilities under balanced demand;
• Lemma 11, $\mathrm{Obj}_\infty=\widehat{\mathrm{Obj}}$;
• Lemma 12, $\mathrm{Obj}_m=A_m\,\mathrm{Obj}_\infty$.

Significance

The result. Theorem 15 turns an exponentially large control problem into a convex program with $n^2$ variables and a guarantee that does not depend on the arrival rates. The factor $m/(m+n-1)$ tends to $1$ as the fleet grows relative to the number of stations. The same framework gives the paper's later results on travel times, rebalancing and constrained pricing. In those settings the balanced-demand shortcut is unavailable and the infinite-unit comparison (Lemmas 12 and 14) carries the argument.

Formalizing it. The theorem is proved in the paper; nothing here is open. The mission produces a machine-checked version and a reusable layer: stationarity of finite-state rate-based chains via balance equations, the identification of state-independent pricing with Gordon–Newell networks, and availability identities for product-form laws. The Gordon–Newell product form itself is already proved on the platform and is referenced, not restated. No result of this paper had a machine-checked proof on the platform when the mission was drafted.

Difficulty

The comparison is against state-dependent policies, which can be reducible and have many stationary laws. Lemma 9 must hold for every one of them, so no product form is available on that side: only the balance equations are.

On the other side, the availability of a state-independent policy depends on the traffic intensities in a way that has no closed form for finite $m$, and the bound $m/(m+n-1)$ must hold uniformly over all of them.

A natural first idea is to compare $\tilde q$ directly with the averaged quantiles of the optimal policy. That idea fails: averaging ignores availability, which is exactly the loss being bounded.

Finally, identifying the stationary law of $\tilde q$ with the uniform law uses irreducibility, which must be derived from the connectivity hypothesis.

Formalization scope

Nodes are Fin n, so the paper's node $i$ is index $i-1$. States reuse the closed-network vocabulary of the platform (states, moveState, productForm, normConst, tailMarginal). Laws are real functions on $\mathbb N^n$ that vanish off $S_{n,m}$.

Decisions and rewards.

• Decision variables are quantiles. Value distributions and prices do not appear, and $I_{ij}$ is any real function of the quantile.
• $R_{ij}(q):=q\,I_{ij}(q)$, so $R_{ij}(0)=0$. Concavity is required on $[0,1]$ only.
• A state-independent $q$ enters the $m$-unit system as the policy $x\mapsto q_{ij}\mathbf 1\{x_i>0\}$.

Stationarity and the optimum.

• Stationarity is the balance equation (1) plus nonnegativity, vanishing off $S_{n,m}$ and total mass $1$. Without the total mass, the zero function would satisfy (1).
• $\mathrm{Opt}_m$ is never a supremum: the goal quantifies over every policy and every stationary law, so no junk value of sSup can enter.
• Policies must vanish at empty stations, so no ride is counted from a station without units.

Ratios and traffic.

• Ratios are stated as products, e.g. $\mathrm{Obj}_m=A_m\,\mathrm{Obj}_\infty$, so there is no division by an objective.
• Traffic intensities are solutions of $\sum_jr_j\varphi_{ji}q_{ji}=r_i\sum_k\varphi_{ik}q_{ik}$.

The milestones that depend on connectivity (Proposition 6, Lemmas 10 and 11) state it as a hypothesis, as the goal does.

The needed infrastructure is finite sums over $S_{n,m}$, Jensen's inequality for concave functions on $[0,1]$, and the bridge from the balance equation to the closed-network steady state. Proofs of any milestone, and alternative proofs of the bridge, are welcome.

Selected references

• S. Banerjee, D. Freund, T. Lykouris, Pricing and Optimization in Shared Vehicle Systems: An Approximation Framework, Operations Research 70(3), 2022; arXiv:1608.06819v4. https://arxiv.org/abs/1608.06819
• W. J. Gordon, G. F. Newell, Closed Queuing Systems with Exponential Servers, Operations Research 15(2), 1967. https://doi.org/10.1287/opre.15.2.254
• D. K. George, C. H. Xia, Fleet-sizing and service availability for a vehicle rental system via closed queueing networks, European Journal of Operational Research 211(1), 2011. https://doi.org/10.1016/j.ejor.2010.12.015
• A. Waserhole, V. Jost, Pricing in vehicle sharing systems: optimization in queuing networks with product forms, EURO Journal on Transportation and Logistics 5(3), 2016. https://doi.org/10.1007/s13676-014-0054-4
• R. Serfozo, Introduction to Stochastic Networks, Springer, 1999. https://doi.org/10.1007/978-1-4612-1482-3

Motivation

Bike-sharing operators periodically move docks between stations: a station that often runs out of bikes or of open docks frustrates users, but every moved dock costs money. Freund, Henderson and Shmoys modelled this dock re-allocation problem as a separable nonlinear integer program with a budget on the number of moved docks (Freund–Henderson–Shmoys, IPCO 2017). Shioura observed that, after a change of variables, the objective is an M-convex function and the budget is an $\ell_1$-ball around the current allocation, and studied the resulting problem in general (Shioura, arXiv:1809.03126).

M-convex functions are the discrete analogue of convex functions on the integer points of a hyperplane, introduced by Murota (Murota, Adv. Math. 1996; Murota, Discrete Convex Analysis, SIAM 2003). Their unconstrained minimization is well understood: a local minimum with respect to single exchanges $x \mapsto x + \chi_i - \chi_j$ is global, and steepest descent converges. Adding an $\ell_1$-distance constraint breaks the M-convex structure of the feasible region, and whether the exchange method survives such a constraint is the question this mission formalizes.

Setting

Let $V$ be a finite set (the stations), and write $x(V) = \sum_{v \in V} x(v)$ for $x \in \mathbb Z^V$, $\chi_i$ for the $i$-th unit vector, $\chi_0 = \mathbf 0$, $\mathrm{supp}^+(z) = \{v \mid z(v) > 0\}$, $\mathrm{supp}^-(z) = \{v \mid z(v) < 0\}$ and $\|z\|_1 = \sum_v |z(v)|$. For $f : \mathbb Z^V \to \mathbb R \cup \{+\infty\}$, the effective domain is $\operatorname{dom} f = \{x \mid f(x) < +\infty\}$. The function $f$ is M$^\natural$-convex if

and M-convex if, in addition, $\operatorname{dom} f \subseteq \{x \mid x(V) = \theta\}$ for some $\theta \in \mathbb Z$.

Fix an M-convex $f$ with bounded $\operatorname{dom} f$ and a center $x_c$ with $x_c(V) = \theta$; the center need not lie in $\operatorname{dom} f$. For $k \in \mathbb Z_+$ the problem

has optimal set $M_k$. Put $2\sigma = \min\{\|x - x_c\|_1 \mid x \in \operatorname{dom} f\}$ (the radius at which the problem becomes feasible) and $2\tau = \min\{\|x - x_c\|_1 \mid x \in \arg\min f\}$ (the radius at which the constraint stops binding). For a budget $\gamma \ge \sigma$, the problem (MML1) is (MML1($\gamma$)).

Algorithm SteepestDescentMML1 (p. 8): choose $x_\sigma \in M_\sigma$; for $k = \sigma + 1, \dots, \gamma$ set $x_k = x_{k-1} + \chi_{i_k} - \chi_{j_k}$, where $(i_k, j_k) \in V \times V$ minimizes $f(x_{k-1} + \chi_i - \chi_j)$ over all pairs; output $x_\gamma$.

Formalization targets

Goal: Theorem 4.2

Every run of SteepestDescentMML1, with any choice in Step 0 and any tie-breaking, satisfies

The goal fixes no constant and covers every M-convex $f$ with bounded domain, every center on the hyperplane, and every budget $\gamma \ge \sigma$.

Milestones

1. (M-EXC) (§2.1, p. 4): $f$ is M-convex if and only if $\forall x, y \in \operatorname{dom} f,\ \forall i \in \mathrm{supp}^+(x - y),\ \exists j \in \mathrm{supp}^-(x - y)$ with the exchange inequality.
2. Lemma A.1 (p. 16): if $y \ne \tilde y$, $y(V) = \tilde y(V)$ and $\|y - x_c\|_1 \le \|\tilde y - x_c\|_1$, then $\tilde y$ exceeds $x_c$ somewhere on $\mathrm{supp}^+(\tilde y - y)$ or falls below it somewhere on $\mathrm{supp}^-(\tilde y - y)$.
3. Lemma A.2 (p. 16): $\|x - z\|_1 + \|y - z\|_1 \ge \|(x - \chi_i + \chi_j) - z\|_1 + \|(y + \chi_i - \chi_j) - z\|_1$ for $i \in \mathrm{supp}^+(x - y)$, $j \in \mathrm{supp}^-(x - y)$.
4. Lemma A.3 (p. 17): from $y \in \operatorname{dom} f$ with $\|y - x_c\|_1 < 2\tau$ there is a monotone sequence with strictly decreasing values to the point of $M_\tau$ nearest to $y$.
5. Theorem 4.1 (p. 8): (i) $\mu_\sigma > \mu_{\sigma+1} > \cdots > \mu_\tau$ and $M_k \subseteq \{\|x - x_c\|_1 = 2k\}$ for $k \in [\sigma, \tau]$; (ii) every $y \in M_k$ has a neighbour $y + \chi_i - \chi_j \in M_{k+1}$ with $i \notin \mathrm{supp}^-(y - x_c)$, $j \notin \mathrm{supp}^+(y - x_c)$; (iii) every $y \in M_{k+1}$ has a neighbour $y - \chi_i + \chi_j \in M_k$ with $i \in \mathrm{supp}^+(y - x_c)$, $j \in \mathrm{supp}^-(y - x_c)$, for $k \in [\sigma, \tau - 1]$.

Significance

Theorem 4.2 gives a pseudo-polynomial algorithm for (MML1): after the initial point, it needs $\gamma - \sigma$ rounds of $|V|^2$ function evaluations. It is also a structural statement: the greedy path from the center passes through an optimum at every radius simultaneously, so a single run answers the whole family of budget questions $k = \sigma, \dots, \gamma$, which is what an operator comparing budgets needs. Theorem 4.1 underlies the paper's polynomial-time proximity and scaling algorithms (§5) and its fast algorithm for dock re-allocation (§6).

The result is proved in the paper; nothing here is open mathematics. No part of it is formalized: the platform has M-convex vocabulary and unconstrained steepest descent bounds from Murota's book, but nothing about $\ell_1$-constrained minimization, the sets $M_k$, or steepest descent under a distance constraint. The mission produces a machine-checked proof of the algorithm's correctness, including the case of an infeasible center and budgets beyond $\tau$, which the printed theorem sets aside.

Difficulty

The feasible region of (MML1($k$)) is not M-convex, so the classical optimality criterion for M-convex functions does not apply to it directly, and a local optimum of the constrained problem need not be global. The obvious induction, "a steepest step from an optimum at radius $2k$ lands at an optimum at radius $2(k+1)$", requires knowing that some optimum at radius $2(k+1)$ is a single exchange away and that its exchange moves away from the center; that is Theorem 4.1 (ii), whose proof rests on the strict monotonicity of the optimal values and on the tightness of the constraint (Theorem 4.1 (i)), which in turn rests on constructing strictly decreasing exchange paths towards a nearest minimizer (Lemma A.3). The bookkeeping of $\ell_1$ distances along such paths, which change by $-2$, $0$ or $+2$ per step, is the delicate part.

Formalization scope

Vectors are V → ℤ over a finite type V with decidable equality (no lower bound on $|V|$); values are WithTop ℝ, with $+\infty = \top$; $\|x - y\|_1$ is the natural number L1Dist x y. M-convexity is the paper's definition, (M$^\natural$-EXC) plus the hyperplane condition, using the published MNatExchangeAxiom; it is not defined through (M-EXC), whose equivalence is a milestone. The hyperplane condition through the center is the hypothesis $\forall x \in \operatorname{dom} f,\ x(V) = x_c(V)$; $x_c \in \operatorname{dom} f$ is not assumed. $\sigma$ and $\tau$ are natural numbers given by IsLeast hypotheses on the doubled minima. $M_k$ is a set defined from $f$, $x_c$ and $k$, and the optimal value $\mu_k$ is never a separate real number: Theorem 4.1 (i) asserts $M_k \ne \emptyset$ and compares values of $f$ on consecutive sets. A run is a sequence x : ℕ → V → ℤ satisfying Step 0 and Steps 2–3, with all pairs $(i, j)$, $i = j$ included, admissible in Step 2.

The goal is not vacuous: the run hypothesis is satisfiable whenever $\operatorname{dom} f \ne \emptyset$ (the minima over the finite sets $V \times V$ exist and $M_\sigma \ne \emptyset$), and a sanity file exhibits an instance with an explicit run. The paper's standing assumption $\tau > \gamma$ is dropped; the goal therefore also covers budgets past the nearest minimizer.

A complete development needs the M-convex exchange calculus (the (M-EXC) equivalence and its use with $\ell_1$ distances), which is reusable for any M-convex problem with a distance or budget constraint. Proofs of the milestones in any order are welcome, as are alternative proofs of Theorem 4.1.

Selected references

• A. Shioura, M-convex Function Minimization Under L1-Distance Constraint (published as M-Convex Function Minimization Under L1-Distance Constraint and Its Application to Dock Reallocation in Bike-Sharing System, Mathematics of Operations Research, 2022), arXiv:1809.03126v3, 2018. https://arxiv.org/abs/1809.03126
• D. Freund, S. G. Henderson, D. B. Shmoys, Minimizing multimodular functions and allocating capacity in bike-sharing systems, Proc. 19th IPCO, LNCS 10328, 2017. https://arxiv.org/abs/1611.09304
• K. Murota, Discrete Convex Analysis, SIAM, 2003. https://doi.org/10.1137/1.9780898718508
• K. Murota, Convexity and Steinitz's exchange property, Advances in Mathematics 124:272–311, 1996. https://doi.org/10.1006/aima.1996.0084
• K. Murota, On steepest descent algorithms for discrete convex functions, SIAM Journal on Optimization 14:699–707, 2003. https://doi.org/10.1137/S1052623402419005

Motivation

A cooperative game with transferable utility (a TU-game) assigns to every coalition of players a number, the worth that coalition can secure on its own. The central allocation concept is the core, introduced by Gillies (1953): the payment vectors that distribute exactly the worth of the grand coalition while giving every coalition at least its worth. The core may be empty. Bondareva (1963) and Shapley (1967) characterized the games with a nonempty core as the balanced games, through a finite family of linear inequalities indexed by minimal balanced collections. The set of balanced games is therefore a polyhedron, and Garcia-Segador, Grabisch and Miranda (arXiv:2501.14341) study its geometry: its lineality space, extremal rays and facets, and those of two of its sections.

The motivation given in the paper is a projection problem: finding the balanced game closest to a non-balanced one would give a new solution concept for games with an empty core, and an orthogonal projection onto a polyhedron needs a detailed description of that polyhedron. Games are set functions vanishing on the empty set, so the same objects appear in decision theory (capacities), voting theory (simple games) and combinatorial optimization (polymatroid rank functions).

This mission concerns the third section studied in the paper: the nonnegative balanced games normalized by $v(N)=1$. This set is a polytope, and the paper shows that it is a combinatorial polytope in the sense of Naddef and Pulleyblank (1981) and that its graph is Hamilton-connected.

Setting

Let $N=\{1,\dots,n\}$ be the set of players. A coalition is a subset $S\subseteq N$, and a game is a function $v:2^N\to\mathbb R$ with $v(\varnothing)=0$. Write $x(S)=\sum_{i\in S}x_i$ for $x\in\mathbb R^n$. The core of $v$ is

and $v$ is balanced when $C(v)\ne\varnothing$.

$\mathcal G_+(n)$ is the set of games with $v(S)\ge 0$ for every $S$ and $v(N)=1$, and

A vertex of $\mathcal{BG}_+(n)$ is an extreme point. Two distinct vertices are adjacent when the segment between them is an edge (a one-dimensional face). The adjacency graph has the vertices as nodes and the adjacent pairs as edges. For a vertex $v$, its family is $\mathcal D(v)=\{S\ne\varnothing,N : v(S)=1\}$; conversely a family $\mathcal D$ of proper nonempty coalitions defines the game $v_{\mathcal D}$ equal to $1$ on $\mathcal D\cup\{N\}$ and $0$ elsewhere.

A polytope $P\subseteq\mathbb R^d$ is combinatorial (Definition 1) when all its vertices are 0-1-valued and, for any two distinct non-adjacent vertices $v_1,v_2$, there are two other different vertices $v_3,v_4$ with $v_1+v_2=v_3+v_4$. A graph is Hamilton-connected when every two distinct nodes are joined by a Hamiltonian path, and the hypercube $Q_d$ is the graph on $\{0,1\}^d$ whose edges join vectors at Hamming distance one.

Formalization targets

Goal: Theorem 12

Both clauses are part of the goal; the first includes that $\mathcal{BG}_+(n)$ is a polytope, since Definition 1 applies to polytopes. Hamilton-connectedness (a Hamiltonian path between every pair of distinct vertices) is stronger than having a Hamiltonian cycle.

Milestones

1. Theorem 1 (Bondareva–Shapley): $C(v)\ne\varnothing$ iff $v$ is balanced. Already proved on the platform.
2. Proposition 1: $\mathcal{BG}_+(n)$ is a $(2^n-2)$-dimensional polytope.
3. Theorem 8: $v\in\mathcal G_+(n)$ is a vertex of $\mathcal{BG}_+(n)$ iff $v$ is balanced and 0-1-valued.
4. Theorem 9: for a family $\mathcal D\subseteq 2^N\setminus\{\varnothing,N\}$, $v_{\mathcal D}$ is a vertex iff $\mathcal D=\varnothing$ or $\bigcap\mathcal D\ne\varnothing$.
5. Lemma 5: distinct vertices $v_1,v_2$ are non-adjacent iff $v_1+v_2=v_3+v_4$ for vertices $v_3,v_4\notin\{v_1,v_2\}$; then $\mathcal D_3\cup\mathcal D_4=\mathcal D_1\cup\mathcal D_2$ and $\mathcal D_3\cap\mathcal D_4=\mathcal D_1\cap\mathcal D_2$.
6. Theorem 11 (Naddef–Pulleyblank): the adjacency graph of a combinatorial polytope is a hypercube or Hamilton-connected.
7. Proof of Theorem 12: for $n\ge 2$ the adjacency graph of $\mathcal{BG}_+(n)$ is not a hypercube.

Significance

The result. The vertices of $\mathcal{BG}_+(n)$ are the balanced 0-1-valued games, and their number grows doubly exponentially in $n$ (Proposition 3 of the paper). Theorem 12 places this polytope in the class of combinatorial polytopes studied by Naddef and Pulleyblank, in which non-adjacency of two vertices is witnessed by a pairwise exchange $v_1+v_2=v_3+v_4$. Hamilton-connectedness gives, between any two prescribed vertices, an ordering of all vertices in which consecutive vertices share an edge of the polytope, that is, a traversal of the whole vertex set by edge moves.

Formalizing it. The theorem is proved in the paper; no machine-checked proof exists. The mission produces formal definitions of the core-based balanced-game polytope, of the adjacency graph of a convex set, of hypercube graphs, of Hamilton-connectedness and of combinatorial polytopes. The Naddef–Pulleyblank theorem (Theorem 11) is cited in the paper without proof and is itself a substantial formalization target, reusable for every combinatorial polytope.

Difficulty

Three steps carry the weight. Theorem 11 is a graph-theoretic result about all combinatorial polytopes; its proof is not in this paper. Lemma 5 requires showing that non-adjacency of two vertices is witnessed by a single pair of other vertices with the same sum; a general non-adjacent pair only has its midpoint expressed as a convex combination of possibly many other vertices, and the printed proof starts from the two-vertex form, which is exactly what needs proving (the statement has been checked numerically for $n\le 4$ exhaustively and sampled for $n=5$). The non-hypercube step must rule out a graph isomorphism to any $Q_d$, which the printed observation about $\hat\delta_{\{i\}}$ and $\hat\delta_{\{j\}}$ does not do by itself.

Formalization scope

Players are Fin n (0-based), coalitions are Finset (Fin n), and a game is a vector Finset (Fin n) → ℝ. The coordinate at $\varnothing$ is part of the vector and is fixed at $0$ by $\mathcal G_+(n)$; the paper's space $\mathbb R^{2^N\setminus\{\varnothing\}}$ is an affine copy, so vertices, edges, sums and dimension are unchanged. Balancedness is the nonemptiness of the core, using the published definition Supermodularity.Cooperative.Core; the paper's inequality description (4) is linked to it by Theorem 1. A polytope is the convex hull of a finite set. Vertices are extreme points, adjacency is the published Hirsch.Adj (distinct points whose segment is an extreme subset), a hypercube is a graph isomorphic to $Q_d$ for some $d\ge 0$, and Hamilton-connected is stated with Mathlib's Walk.IsHamiltonian for every ordered pair of distinct vertices.

The goal is stated for every $n$; at $n=0$ the polytope is empty and every clause holds trivially. Proposition 1 and Theorem 9 keep the paper's $n\ge 1$, and the non-hypercube step needs $n\ge 2$ ($\mathcal{BG}_+(1)$ is one point, whose graph is $Q_0$).

Lemma 5's "In addition" clause is formalized for every pair of vertices $v_3,v_4$ with $v_1+v_2=v_3+v_4$, the stronger of the two possible readings. The printed proof of Lemma 5 assumes a two-vertex representation of the midpoint, a gap a solver must close.

Vertices are never defined as balanced 0-1 games, and adjacency is never defined through the families $\mathcal D$ or the exchange condition: either choice would make Theorem 8 or Lemma 5 true by definition and empty the goal.

Contributions welcome: a proof of the Naddef–Pulleyblank theorem from Definition 1; facts about extreme points and faces of polytopes given as convex hulls; the vertex characterization via cores.

Selected references

• P. Garcia-Segador, M. Grabisch, P. Miranda, On the set of balanced games, arXiv:2501.14341v1, 2025 (Mathematics of Operations Research, 2025). https://arxiv.org/abs/2501.14341
• D. Naddef, W. R. Pulleyblank, Hamiltonicity and combinatorial polyhedra, Journal of Combinatorial Theory, Series B 31 (1981), 297–312.
• O. Bondareva, Some applications of linear programming to the theory of cooperative games, Problemy Kibernetiki 10 (1963), 119–139 (in Russian).
• L. S. Shapley, On balanced sets and cores, Naval Research Logistics Quarterly 14 (1967), 453–460.
• D. Gillies, Some theorems on n-person games, PhD thesis, Princeton, 1953.
• T. Matsui, S. Tamura, Adjacency on combinatorial polyhedra, Discrete Applied Mathematics 56 (1995), 311–321.

Motivation

Large language models are increasingly used as digital twins of survey respondents: a model is prompted with a persona and asked to answer the same questionnaire a human would. The appeal is cost and speed, since a new question can be "fielded" to thousands of simulated respondents in minutes. The obstacle is fidelity. Large language models exhibit systematic bias and miscalibration relative to real human behavior (Fan, Huang, Peng, Wang, Wu, 2026).

SYN-DIGITS proposes to calibrate twin output with ideas from synthetic control (Abadie, Diamond, Hainmueller, 2010): learn on the twins how answers to a new question relate to answers to existing questions, then apply the learned relation to the humans, whose answers to the existing questions are observed. The paper evaluates ten calibration methods of this kind on MovieLens and on the Twin-2K-500 survey dataset. Its Theorem 4.1 is the explanation offered for why this works even when twins and humans disagree: the error of the transferred prediction splits into a structural part, controlled by how well the twins' inter-question structure aligns with the humans', and an estimation part that shrinks with sample size.

Setting

There are $n$ users and $m$ existing questions. The human response matrix is $Y \in \mathbb{R}^{n\times m}$ and the twin response matrix on the same questions is $\tilde Y \in \mathbb{R}^{n\times m}$. For a new question, the twins' answers $\tilde Y_v \in \mathbb{R}^n$ are observed and the humans' answers $Y_v \in \mathbb{R}^n$ are to be predicted.

Latent factor model. There are user embeddings $U \in \mathbb{R}^{n\times d}$, question embeddings $V \in \mathbb{R}^{m\times d}$ (one row per question) and a noise matrix $\mathcal E \in \mathbb{R}^{n\times m}$ with $Y = UV^\top + \mathcal E$. The new question has embedding $v \in \mathbb{R}^d$ and noise $\mathcal E_v$, so $Y_v = Uv + \mathcal E_v$. Its embedding is decomposed as $v = V^\top b + e$: $b \in \mathbb{R}^m$ are coefficients on the existing questions and $e \in \mathbb{R}^d$ is the part no combination of existing questions represents.

Ridge fit-and-transfer. With the sample moments of the twin system

and a penalty $\lambda \ge 0$, the Ridge fit on the twins is $\hat\beta = (\hat{\tilde\Sigma} + \lambda I)^{-1}\hat{\tilde\gamma}$, and the prediction is its transfer to the humans, $\hat Y_v = Y\hat\beta$.

Population target. With the population moments $\tilde\Sigma = \frac1n\mathbb E[\tilde Y^\top\tilde Y]$ and $\tilde\gamma = \frac1n\mathbb E[\tilde Y^\top\tilde Y_v]$, the target coefficients are $\beta^* = (\tilde\Sigma + \lambda I)^{-1}\tilde\gamma$ and the structural residual is $r = Y_v - Y\beta^*$.

Vector norms $\|\cdot\|_2$ are Euclidean, matrix norms $\|\cdot\|_2$ are spectral, and $\sigma_{\min}$ is the smallest singular value.

Formalization targets

Goal: Theorem 4.1 (p. 11), both clauses

The first term of the first bound is the structural error and the second is the estimation error. The bound is deterministic: it holds for every realization of the data, with no probabilistic assumption.

Milestones (Appendix B.1, pp. 32–33)

1. The residual split $\hat Y_v - Y_v = Y(\hat\beta - \beta^*) - r$ and its norm bound.
2. The fact $\|(S + \lambda I)^{-1}\|_2^{-1} = \sigma_{\min}(S) + \lambda$ for positive semidefinite $S$.
3. The normal equations and the coefficient error bound for $\|\hat\beta - \beta^*\|_2$.
4. The structural split $r = Ue + (\mathcal E_v - \mathcal E b) + Y(b - \beta^*)$ and its norm bound.
5. The population coefficient bound for $\|\beta^* - b\|_2$.