All missions

Bilevel problems on a network

Bilevel optimization chooses an upper-level variable $x$ to minimize an objective that depends on the solution $y^*(x)$ of a lower-level problem. Hyperparameter tuning and meta-learning are the standard examples (Franceschi et al. 2018; Ghadimi and Wang 2018). In the decentralized version the data are split among $n$ agents. Each agent sees only its own upper- and lower-level functions $F_i$ and $f_i$, and it can talk only to its neighbours in a communication network. The paper's example is $n$ hospitals tuning a regularization weight of a logistic-regression model. No hospital may share its patients' data, but the hyperparameter has to be good for the pooled data.

Decentralized bilevel algorithms before this paper converged only under a heterogeneity assumption, a bound on how much the agents' functions may differ. DSBO (Chen, Huang and Ma 2024) assumes i.i.d. local data, MA-DSBO (Chen et al. 2023) a uniform bound on $\|\nabla_2 f_i - \nabla_2 f\|$, and SLAM (Lu et al. 2022) Lipschitz-type closeness of the local Hessians. Such assumptions fail exactly when the agents' data differ, which is the case that motivates decentralization in the first place. Dong, Ma, Yang and Yin propose SLDBO, a single-loop method that needs no such assumption, and prove an $O(1/K)$ rate for it.

Setting

There are $n\ge1$ agents. Agent $i$ holds $F_i,f_i:\mathbb R^p\times\mathbb R^q\to\mathbb R$. Write $F=\frac1n\sum_iF_i$ and $f=\frac1n\sum_if_i$. Problem (6) is

$$\min_{x\in\mathbb R^p}\ \Phi(x)=F(x,y^*(x)),\qquad y^*(x)=\arg\min_{y\in\mathbb R^q}f(x,y).$$

Assumption 2.1 gives constants $\sigma>0$ and $L_{F,0},L_{F,1},L_{f,1},L_{f,2}\ge0$. Each $f_i(x,\cdot)$ is $\sigma$-strongly convex. $F_i$ is $L_{F,0}$-Lipschitz with an $L_{F,1}$-Lipschitz gradient. $f_i$ is twice differentiable with an $L_{f,1}$-Lipschitz gradient and an $L_{f,2}$-Lipschitz Hessian. Under these conditions $y^*$ is well defined and $\Phi$ is differentiable, with the hypergradient (7)

$$\nabla\Phi(x)=\nabla_1F(x,y^*(x))-\nabla^2_{12}f(x,y^*(x))\,v^*(x),\qquad v^*(x)=\big[\nabla^2_{22}f(x,y^*(x))\big]^{-1}\nabla_2F(x,y^*(x)).$$

Here $\nabla_1,\nabla_2$ are the partial gradients, $\nabla^2_{22}f$ is the Hessian of $f$ in $y$, and $\nabla^2_{12}f$ is the Jacobian of $\nabla_1f$ in $y$.

Assumption 2.2. The agents communicate through a nonnegative, symmetric, doubly stochastic mixing matrix $W=(w_{ij})$, and $\rho<1$ bounds the contraction of $W$ away from consensus.

SLDBO (Algorithm 1) keeps three local iterates $x^k_i,y^k_i,v^k_i$ per agent. Agent $i$ computes the local directions $d^k_{y,i}=\nabla_2f_i$, $d^k_{v,i}=\nabla_2F_i-\nabla^2_{22}f_i\,v^k_i$ and $d^k_{x,i}=\nabla_1F_i-\nabla^2_{12}f_i\,v^k_i$ at $(x^k_i,y^k_i)$. It feeds them into gradient-tracking variables $t^k_{\cdot,i}=\sum_jw_{ij}t^{k-1}_{\cdot,j}+d^k_{\cdot,i}-d^{k-1}_{\cdot,i}$, which estimate the network averages of the directions. It then takes one mixed step on each iterate with constant step sizes $\beta,\eta,\alpha$. The step on $v$ is followed by the projection $\mathcal P_{r_v}$ onto the ball of radius $r_v=L_{F,0}/\sigma$, which contains every $v^*(x)$. All agents start from common points with $t^{-1}=d^{-1}=0$ (BOX 1). Bars denote averages over agents, e.g. $\bar x^k=\frac1n\sum_ix^k_i$.

Formalization targets

Goal: Theorem 3.1

The step sizes have thresholds depending only on $(\sigma,L_{F,0},L_{F,1},L_{f,1},L_{f,2},\rho)$: first $\bar\beta$, then $\bar\eta$ given $\beta$, then $\bar\alpha$ given $\beta,\eta$. Below these thresholds, every instance with $\Phi$ bounded below has a constant $C$ such that for all $K\ge1$

$$\min_{0\le k\le K-1}\|\nabla\Phi(\bar x^k)\|^2\le\frac CK,\qquad \min_{0\le k\le K-1}\frac1n\sum_{i=1}^n\|z^k_i-\bar z^k\|^2\le\frac CK\quad(z\in\{x,y,v\}).$$

The goal fixes no explicit step sizes and no explicit constant $C$; it asserts the rate.

Milestones

These are the paper's own statements, in attack order:

• the hypergradient formula (7);
• the mixing and projection lemmas A.1–A.2;
• the tracking identity (25);
• the consensus recursions A.3–A.4 with Remarks A.1–A.2;
• the bounds A.5–A.7 with Remark A.3 (A.5 and A.7 are included as supporting statements rather than milestones);
• the Lipschitz continuity of $y^*$ and $v^*$ (A.11) and of $\nabla\Phi$;
• the descent inequality for $\Phi$ (A.8);
• the contractions of $\|\bar y^k-y^*(\bar x^k)\|$ and $\|\bar v^k-v^*(\bar x^k)\|$ (A.9–A.10).

Significance

The theorem shows that a single-loop decentralized method reaches the $O(1/K)$ stationarity rate known for centralized single-loop bilevel methods (Ji et al. 2022; Dagréou et al. 2022). Each iteration needs $\Theta(1)$ communication rounds and one Hessian- and one Jacobian-vector product, with no heterogeneity bound. The consensus clauses add that the agents agree at the same rate.

The result is proved in the paper; nothing about it is formalized. The mission adds three things. First, a machine-checked statement with explicit conventions. Second, a check of the constants. The printed $L_\Phi$ in (8) has a term that is not homogeneous in the scale of $F$, and the explicit step-size bounds (62) do not make the Lyapunov coefficient $A_2$ nonnegative (checked numerically). The goal is therefore stated in a form the argument supports. Third, reusable lemmas for gradient-tracking analyses: the mixing-matrix contraction, the projected-consensus inequality, the tracking identity and the hypergradient formula.

Difficulty

The obvious analysis of a decentralized SOBA-type method bounds the change of the directions $d^k_{x,i}$ and $d^k_{v,i}$ between iterations by the change of the iterates. Those directions contain $\nabla^2f_i\,v^k_i$. Without control of $\|v^k_i\|$, their variation is bounded only by assuming the local Hessians are close, which is the heterogeneity assumption. The projection removes the need for it. The price is that $\bar v^k$ no longer follows the averaged direction, so the consensus and error recursions for $v$ have to be derived separately. All of these recursions are then combined into one Lyapunov function (15) whose coefficients must be balanced against three coupled step sizes. Most of the work, and the published constants' main failure, is in that balancing.

Formalization scope

Vectors live in EuclideanSpace ℝ (Fin d). Lipschitz conditions in $(x,y)$ use $\sqrt{\|x-x'\|^2+\|y-y'\|^2}$, never Lean's sup norm on a product. The model and the added hypotheses:

• Hessian condition. It is imposed on the two blocks $\nabla^2_{12}f_i$ and $\nabla^2_{22}f_i$ in the operator norm. This is weaker than the paper's Frobenius-Lipschitz full Hessian.
• Mixing rate. $\rho$ is any bound of $W$ on $\mathbf 1^\perp$; the paper's eigenvalue $\rho$ is the least one.
• Lower-level solution. $y^*$ is a given map with $y^*(x)$ minimizing $f(x,\cdot)$ for every $x$.
• Hypergradient. $v^*$ is defined through ContinuousLinearMap.inverse, and $\nabla\Phi$ is the formula (7). A milestone proves that (7) is the gradient of $\Phi$.
• Algorithm. Algorithm 1 with BOX 1 is one deterministic function run. Its state at index $k$ holds $(x^k,y^k,v^k,t^{k-1},d^{k-1})$.
• Rate. "$O(1/K)$" is one constant $C$, fixed after the instance and before $K$; the minimum over $0\le k\le K-1$ is an existential $k<K$.
• $\Phi$ bounded below. This is added to the goal. Without it the claim fails: $F_i(x,y)=-x$ and $f_i(x,y)=y^2/2$ satisfy Assumption 2.1, yet $\nabla\Phi\equiv-1$.
• Lemma A.5 is posed for $k\ge1$. At $k=0$ it would claim $d^0=0$.
• Lemmas A.9 and A.10 carry the two bounds of (62) their proofs use, $\beta L_{f,1}<1$ and $\eta L_{f,1}<1$.
• $L_\Phi$ is $(L_{F,1}+L_{f,2}r_v)(1+L_{f,1}/\sigma)^2$, which is (8) with $L_{F,0}^2$ corrected to $L_{F,0}$.
• Step sizes. The goal is stated with nested thresholds instead of (62).

The goal would become trivial if the thresholds were chosen after the instance or $C$ after $K$, and false without $\Phi$ bounded below; the statement rules both out. All hypotheses are satisfiable: a two-agent instance with $\rho=0$ and $f_i=\|y\|^2/2$ is checked in Lean.

A complete development needs the implicit-function theorem for $y^*$, the descent lemma, strong-convexity inequalities for gradient steps, and the gradient-tracking bookkeeping. The mixing-matrix and tracking lemmas are reusable for other gradient-tracking methods. Proofs of any milestone, and repaired explicit step-size conditions, are welcome.

Selected references

• Y. Dong, S. Ma, J. Yang, C. Yin, A Single-Loop Algorithm for Decentralized Bilevel Optimization, Mathematics of Operations Research, 2025; arXiv:2311.08945v3. https://arxiv.org/abs/2311.08945
• M. Dagréou, P. Ablin, S. Vaiter, T. Moreau, A framework for bilevel optimization that enables stochastic and global variance reduction algorithms, NeurIPS 35, 2022. https://arxiv.org/abs/2201.13409
• S. Ghadimi, M. Wang, Approximation methods for bilevel programming, arXiv:1802.02246, 2018. https://arxiv.org/abs/1802.02246
• X. Chen, M. Huang, S. Ma, Decentralized bilevel optimization, Optimization Letters, 2024. https://arxiv.org/abs/2206.05670
• X. Chen, M. Huang, S. Ma, K. Balasubramanian, Decentralized stochastic bilevel optimization with improved per-iteration complexity, ICML 2023. https://arxiv.org/abs/2210.12839
• S. Lu, S. Zeng, X. Cui, M. Squillante, L. Horesh, B. Kingsbury, J. Liu, M. Hong, A stochastic linearized augmented Lagrangian method for decentralized bilevel optimization, NeurIPS 35, 2022. https://proceedings.neurips.cc/paper_files/paper/2022 (pp. 30638–30650)
• K. Ji, M. Liu, Y. Liang, L. Ying, Will bilevel optimizers benefit from loops, NeurIPS 35, 2022. https://arxiv.org/abs/2205.14224
• S. Pu, A. Nedić, Distributed stochastic gradient tracking methods, Mathematical Programming 187, 409–457, 2021. https://arxiv.org/abs/1805.11454
• L. Franceschi, P. Frasconi, S. Salzo, R. Grazzi, M. Pontil, Bilevel programming for hyperparameter optimization and meta-learning, ICML 2018. https://arxiv.org/abs/1806.04910

Motivation

A learner who minimizes a regularized population risk

$$\varphi(x)=\mathbb E_{z\sim P}[f(x,z)]+r(x)$$

usually has access to $P$ only through an i.i.d. sample $S=(z_1,\dots,z_m)$, and so works with the empirical risk $\varphi_S(x)=\frac1m\sum_{i=1}^m f(x,z_i)+r(x)$ instead. The question this mission formalizes is how well the first-order behaviour of $\varphi_S$ reflects that of $\varphi$ when the loss is neither smooth nor convex. This matters because the algorithms used in practice for such problems (stochastic subgradient, proximal point and Gauss–Newton methods) find only approximately stationary points, and a uniform estimate of the gap between empirical and population stationarity tells one when further optimization of the empirical problem stops improving the population one.

For convex losses with strongly convex regularization, Shalev-Shwartz, Shamir, Srebro and Sridharan (COLT 2009) showed that the regularized empirical minimizer is stable and generalizes at a dimension-free rate. For smooth nonconvex losses, Mei, Bai and Montanari (Ann. Statist. 2018) and Foster, Sekhari and Sridharan (NeurIPS 2018) proved uniform convergence of gradients. For nonsmooth nonconvex losses, pointwise convergence of the stationarity measure $\operatorname{dist}(0,\partial\varphi(x))$ was known, but uniform results were asymptotic and needed extra structure, because $x\mapsto\operatorname{dist}(0,\partial\varphi(x))$ is highly discontinuous. Davis and Drusvyatskiy (arXiv:1810.07590, Mathematics of Operations Research 2022) replace it by a smoothed measure, the gradient of a Moreau-type envelope, and prove finite-sample uniform bounds for it. The losses covered are the weakly convex ones: phase retrieval, blind deconvolution, robust PCA, censored block models, conditional value-at-risk and sparse dictionary learning all fit (Table 1 of the paper).

Setting

Fix a finite-dimensional real normed space $E$ with norm $\|\cdot\|$ and dual norm $\|\cdot\|_*$. Extended-valued functions $g:E\to\mathbb R\cup\{+\infty\}$ are described by their domain $\operatorname{dom} g$ and their values there.

A Legendre function $\Phi$ is proper, closed and strictly convex, differentiable on the nonempty interior of its domain, and its gradient norm blows up at the boundary of the domain. It induces the Bregman divergence

$$D_\Phi(y,x)=\Phi(y)-\Phi(x)-\langle\nabla\Phi(x),y-x\rangle,\qquad x\in\operatorname{int}(\operatorname{dom}\Phi),$$

and its symmetrization $D^{\mathrm{sym}}_\Phi(x,y)=D_\Phi(x,y)+D_\Phi(y,x)$. For $\Phi=\frac12\|\cdot\|_2^2$, $D_\Phi(y,x)=\frac12\|y-x\|_2^2$. A function $g$ is $\rho$-weakly convex relative to $\Phi$ if $g+\rho\Phi$ is convex, and compatible with $\Phi$ if $\operatorname{ri}(\operatorname{dom} g)\subseteq\operatorname{int}(\operatorname{dom}\Phi)$. For $\bar\rho>0$ the Φ-proximal map and Φ-envelope are

$$\operatorname{prox}^\Phi_{g/\bar\rho}(x)=\operatorname*{argmin}_y\{g(y)+\bar\rho D_\Phi(y,x)\},\qquad g^\Phi_{1/\bar\rho}(x)=\inf_y\{g(y)+\bar\rho D_\Phi(y,x)\}.$$

The standing assumptions are: (A1) $\Phi$ is Legendre, compatible with $r$, and $\frac\alpha2\|y-x\|^2\le D_\Phi(x,y)$ on $\operatorname{dom} r\cap\operatorname{int}(\operatorname{dom}\Phi)$; (A2) for a.e. $z$, $f(\cdot,z)+r$ is $\rho$-weakly convex relative to $\Phi$ and bounded below; (A3) $|f(x,z)-f(y,z)|\le L(z)\sqrt{D^{\mathrm{sym}}_\Phi(x,y)}$ with $L\ge0$ and $\sqrt{\mathbb E L^2}\le\sigma$. Finally $\psi_{\varepsilon L}(\lambda)=\log\mathbb E\,e^{\lambda\varepsilon L(z)}$ for an independent Rademacher sign $\varepsilon$, and $\psi^\star_{\varepsilon L}$ is its Fenchel conjugate.

Formalization targets

Goal: Theorem 4.4 (concentration of the stationarity measure)

For every $C\subseteq\operatorname{int}(\operatorname{dom}\Phi)$, $\delta>0$, $s\ge0$ and $\bar\rho>\rho$, with probability at least $1-\mathcal N(C,\Phi,\delta)\exp(-m\,\psi^\star_{\varepsilon L}(s/\sqrt m))$,

$$\sup_{y\in C}\big\|\operatorname{prox}^\Phi_{\varphi_S/\bar\rho}(y)-\operatorname{prox}^\Phi_{\varphi/\bar\rho}(y)\big\|\le\sqrt{\frac{4(\sigma+s)^2}{\alpha(\bar\rho-\rho)^2m}}+\frac{2\bar\rho\delta}{\alpha(\bar\rho-\rho)},$$

where $\mathcal N(C,\Phi,\delta)$ is the covering number of $C$ in the metric $\|\nabla\Phi(x)-\nabla\Phi(y)\|_*$. If $\Phi$ is twice differentiable, the same probability bounds the event $\sup_{y\in C}\|\nabla(\varphi_S)^\Phi_{1/2\rho}(y)-\nabla\varphi^\Phi_{1/2\rho}(y)\|^*_y\le\sqrt{16(\sigma+s)^2/(\alpha m)}+8\rho\delta/\alpha$ in the local dual norm.

Milestones

1. Theorem 3.1: the Φ-proximal point of a closed, lower-bounded, weakly convex, compatible $g$ is unique and interior, and the envelope has gradient $\frac1\lambda\nabla^2\Phi(x)(x-\operatorname{prox}^\Phi_{\lambda g}(x))$.
2. Theorem 4.1: stability of Bregman-regularized ERM, $\sqrt{D^{\mathrm{sym}}_\Phi(\mathcal A(S),\mathcal A(S^i))}\le\frac{L(z_i)+L(z_i')}{(\bar\rho-\rho)m}$, and the expectation bounds (4.2), (4.3).
3. Theorem 4.2: McDiarmid's inequality with data-dependent differences $\omega_i(z_i,z_i')$, in log-MGF form (4.7) and tail form (4.8).
4. Lemma 4.3: $\operatorname{prox}^\Phi_{g/\bar\rho}$ is $\frac{\bar\rho}{\alpha(\bar\rho-\rho)}$-Lipschitz from the metric $\|\nabla\Phi(x)-\nabla\Phi(y)\|_*$ to $\|\cdot\|$.

Significance

The result gives a sample size beyond which approximate stationarity of the empirical problem certifies approximate stationarity of the population problem, uniformly over a region, with an explicit dependence on the sample size $m$ and on the covering number of the region. Because the graph of the proximal map is linearly isomorphic to the graph of the subdifferential, it also bounds the Hausdorff distance between $\operatorname{gph}\partial\varphi$ and $\operatorname{gph}\partial\varphi_S$ (Theorem 4.5 of the paper, not part of this mission). The Bregman setting covers non-Euclidean geometries (an $\ell_1$-setup) and losses that are only locally Lipschitz with polynomial growth. Theorem 4.2 is reusable on its own: it is a McDiarmid inequality for unbounded, light-tailed differences.

The paper's proofs are complete; nothing here is open. None of the statements has been formalized before. Mathlib has the Fréchet derivative, product measures, cumulant generating functions and convexity, but no Legendre functions, Bregman proximal maps or envelopes, and no McDiarmid inequality with data-dependent differences; the platform has McDiarmid only with constant differences.

Difficulty

The naive route, McDiarmid's inequality applied to $\|\operatorname{prox}^\Phi_{\varphi_S/\bar\rho}(y)-\operatorname{prox}^\Phi_{\varphi/\bar\rho}(y)\|$, needs a bounded difference constant, and the stability estimate (4.1) gives only $L(z_i)+L(z_i')$, which is unbounded unless the data are. The concentration step therefore needs a version of McDiarmid's inequality whose differences are random. A second obstacle is that the empirical objects are random sets: proving that the proximal points are single-valued, interior, and measurable in the sample is a step the paper takes for granted. Third, uniformity over $C$ comes through Lemma 4.3 in the mirror metric $\|\nabla\Phi(x)-\nabla\Phi(y)\|_*$, not in the norm of $E$.

Formalization scope

The space is a finite-dimensional real normed space $E$; gradients are Fréchet derivatives, the dual norm is the operator norm, and $\nabla^2\Phi(y)$ is the second Fréchet derivative, a map $E\to E^*$. Extended-valued functions are pairs (domain, real values), so no extended-real arithmetic occurs. Proximal maps are sets of minimizers; envelopes are real infima, used only where Theorem 3.1 guarantees attainment. "With probability $1-p$" is an outer-measure bound on the failure set under $P^m$. The covering number is replaced by the size of an arbitrary finite $\delta$-net fixed before the sample, and $\exp(-m\psi^\star(t))$ by $\exp(-m(\lambda t-\psi(\lambda)))$ for an arbitrary $\lambda$ with $\cosh(\lambda L)$ integrable; both replacements are equivalent to the page. Hypotheses the paper uses without stating are explicit: $\bar\rho>0$, $m\ge1$, $\operatorname{dom} r$ nonempty and convex, $f(x,\cdot)$ measurable and integrable, closedness of $f(\cdot,z)+r$ and of $\varphi$, $\varphi$ bounded below; the second display of the goal assumes $\rho>0$ and an invertible Hessian on $C$. Theorem 4.1 is read, as its proof is, with $\mathcal A^*$ and $\mathcal A(S)$ the proximal points at $y$.

A pointwise version (fixed $y$), a version where the net may depend on the sample, a bound for one fixed $\lambda$, or the Euclidean case $\Phi=\frac12\|\cdot\|_2^2$ alone would each be a strictly weaker theorem and does not close the goal.

A complete development needs: Legendre-function theory (coercivity of $D_\Phi(\cdot,x)$, interiority of Bregman proximal points), Danskin-type differentiation of the envelope, measurability of argmin maps, the extended McDiarmid inequality, and a covering/union bound. The McDiarmid extension and the Bregman proximal-point lemmas are reusable well beyond this paper. Proofs of the milestones, sanity instances of (A1)–(A3), and intermediate lemmas from the paper's proofs are all welcome.

Selected references

• D. Davis, D. Drusvyatskiy, Graphical Convergence of Subgradients in Nonconvex Optimization and Learning, Mathematics of Operations Research, 2022. arXiv:1810.07590
• D. Davis, D. Drusvyatskiy, K. J. MacPhee, Stochastic model-based minimization under high-order growth, 2018. arXiv:1807.00255
• H. H. Bauschke, M. N. Dao, S. B. Lindstrom, Regularizing with Bregman–Moreau envelopes, SIAM J. Optim., 2018. arXiv:1705.06019
• S. Shalev-Shwartz, O. Shamir, N. Srebro, K. Sridharan, Stochastic Convex Optimization, COLT, 2009. https://www.cs.mcgill.ca/~colt2009/papers/018.pdf
• C. McDiarmid, On the method of bounded differences, Surveys in Combinatorics, LMS Lecture Note Ser. 141, 1989. doi:10.1017/CBO9781107359949.008
• A. Kontorovich, Concentration in unbounded metric spaces and algorithmic stability, ICML, 2014. arXiv:1309.1007
• S. Mei, Y. Bai, A. Montanari, The landscape of empirical risk for nonconvex losses, Ann. Statist., 2018. arXiv:1607.06534
• D. J. Foster, A. Sekhari, K. Sridharan, Uniform convergence of gradients for non-convex learning and optimization, NeurIPS, 2018. arXiv:1810.11059

Motivation

The state of a finite-dimensional quantum system is a density: a positive semidefinite matrix of trace one. Under coherent (Hamiltonian) control the evolution is unitary, $\rho\mapsto U\rho U^*$, and preserves the eigenvalues of $\rho$. Even with full unitary control, a state can therefore only be moved within its unitary orbit. A mixed state cannot be purified, and a pure state cannot be made mixed. Dissipation, modelled by Lindblad generators (Gorini–Kossakowski–Sudarshan 1976, Lindblad 1976), is what breaks these spectral invariants. Engineered dissipation is a standard tool for state preparation (Verstraete–Wolf–Cirac 2009).

This raises a basic control question: how much dissipation must be added to full unitary control before every state can be steered to every other state? Cai, Govindarajan and Junge (arXiv:2504.04883v2) answer it for $k$ qubits. One amplitude-damping jump and one dephasing operator, both acting on a single qubit, suffice.

Timeline.

• Brockett (1972) and Jurdjevic–Sussmann (1972) established the Lie-algebra rank condition for controllability on compact Lie groups. This settled the closed (unitary) case.
• Altafini (2003) began the controllability analysis of Markovian master equations driven by coherent controls.
• Dirr, Helmke, Kurniawan and Schulte-Herbrüggen (2009) described Markovian channels through Lie semigroups and Lie wedges.
• Araiza, Chen, Junge and Wu (2023) studied resource-dependent classes of channels generated by a resource set $S$. The present mission's class $\overline{\mathrm{Channel}(S)}$ follows that approach.
• Cai, Govindarajan and Junge (2025) proved Theorem 2.12: $\overline{\mathrm{Channel}(S)}$ is transitive once $S$ contains a single-qubit amplitude-damping jump and a single-qubit dephasing operator. With a convex hull, Theorem 2.8 of the same paper needs only the amplitude-damping jump.

Setting

Let $H=\mathbb C^{2^k}$ be the space of $k$ qubits, with computational basis $|\omega\rangle$, $\omega\in\{0,1\}^k$. A superoperator is a linear map on $k$-qubit matrices. Densities form the set $\mathcal D(H)=\{\rho:\rho=\rho^*,\ \rho\ge0,\ \operatorname{tr}\rho=1\}$.

For an operator $a$, the Lindblad generator with rate $2$ is

$$L_a(\rho)=2a\rho a^*-a^*a\rho-\rho a^*a .$$

For every $t\ge0$, $e^{tL_a}$ is a quantum channel.

Fix a resource set $S$ of operators with $S=S^*$. The closed class $\overline{\mathrm{Channel}(S)}$ is the smallest closed set $\mathcal C$ of superoperators with three properties:

• (UN) $\operatorname{Ad}_{e^{tX}}\in\mathcal C$, where $\operatorname{Ad}_U(\rho)=U\rho U^*$, for every anti-Hermitian $X=iH$ in the complex span of $S$ and every $t\ge0$;
• (JU) $e^{tL_a}\in\mathcal C$ for every $a\in S$ and every $t\ge0$;
• (CO) $\mathcal C$ is closed under composition.

$S$ generates a Hörmander system if the real Lie algebra generated by the anti-Hermitian part of $\operatorname{span}S$ contains $\mathfrak{su}(2^k)$, the traceless anti-Hermitian matrices. A set $O$ of superoperators is transitive if for all $\rho,\sigma\in\mathcal D(H)$ some $\Phi\in O$ satisfies $\Phi(\rho)=\sigma$. The range of $\rho$ is $D_S(\rho)=\{\Phi(\rho):\Phi\in\overline{\mathrm{Channel}(S)}\}$.

On one qubit, $Z=\operatorname{diag}(1,-1)$, $|0\rangle\langle1|$ is the amplitude-damping jump, and $E_\infty$ keeps the diagonal of a $2\times2$ matrix and deletes the rest. The replacer channel is $\mathcal R_\sigma(\rho)=\operatorname{tr}(\rho)\,\sigma$, and $|0_k\rangle=|0\cdots0\rangle$.

Formalization targets

Goal: Theorem 2.12

If $S=S^*$ generates a Hörmander system on $\mathbb C^{2^k}$ and

$$|0\rangle\langle1|\otimes I^{\otimes(k-1)}\in S,\qquad Z\otimes I^{\otimes(k-1)}\in S,$$

then

$$\forall\,\rho,\sigma\in\mathcal D(H)\quad \exists\,\Phi\in\overline{\mathrm{Channel}(S)}:\ \Phi(\rho)=\sigma .$$

The goal asserts reachability only. It places no bound on time or on the number of compositions.

Milestones

1. Proposition 2.2(i), as used. $\operatorname{Ad}_U\in\overline{\mathrm{Channel}(S)}$ for every unitary $U$.
2. Proposition 2.2(iii). $e^{tL_{uau^*}}$ and $e^{t\sum_jL_{u_ja_ju_j^*}}$ lie in the class for $a,a_j\in S$, unitaries $u,u_j$ and $t\ge0$.
3. Amplitude-damping semigroup ([CW16], p. 8). For $a=|0\rangle\langle1|$ on one qubit, $e^{tL_a}$ has the closed form $\big(\rho_{00}+(1-e^{-2t})\rho_{11},\ e^{-t}\rho_{01};\ e^{-t}\rho_{10},\ e^{-2t}\rho_{11}\big)$.
4. Dephasing generator (p. 8). On one qubit, $L_Z=4(E_\infty-\mathrm{id})$ and $e^{tL_Z}\to E_\infty$.
5. Lemma 2.11(ii). If $Z_1\in S$, then $E_\infty\otimes\mathrm{id}^{k-1}$ and $E_\infty^{\otimes k}$ lie in the class.
6. Replacer claim (proof of Theorem 2.12). $e^{tL_a}\to\mathcal R_{|0\rangle\langle0|}\otimes\mathrm{id}$, and both $\mathcal R_{|0\rangle\langle0|}\otimes\mathrm{id}$ and $\mathcal R_{|0_k\rangle\langle0_k|}$ lie in the class.
7. Lemma 2.11(iii). $D_S(|0_k\rangle\langle0_k|)=\mathcal D(H)$.

Significance

The result. Full unitary control alone cannot change the spectrum of a state. Theorem 2.12 shows that two dissipative resources acting on one qubit already remove every obstruction. This is close to optimal: Proposition 2.7 of the paper shows that self-adjoint jumps alone produce only unital channels, which fix the maximally mixed state, so at least one non-self-adjoint resource is necessary. The result also needs no convexity. The class contains genuine Markovian semigroups, their compositions and their limits, but no mixtures. The surrounding statements are reusable on their own:

• every unitary is generated by a Hörmander system (Chow's theorem in the form used here);
• the pinching and the reset are limits of Lindblad semigroups;
• the pure state $|0_k\rangle$ reaches every density.

Formalizing it. The paper's proof is short, but several steps are stated without detail: "by assumption", "using the conjugation trick and products", and Chow's theorem cited for a semigroup rather than a group. A formal proof fixes exactly what the closure (CL) contributes. It supplies the negative-time unitaries (milestone 1) and the conditional expectations $E_\infty$ and $\mathcal R$ (milestones 4–6), none of which is of the form $e^{tL}$. No machine-checked proof of these statements is known (a search of the Prove2Me library in October 2026 found none). Mathlib has the matrix exponential, the operator norm on superoperators and Lie subalgebras. It has neither Chow's theorem nor the correspondence between Lie subalgebras and connected subgroups of $U(d)$.

Difficulty

The one hard step is milestone 1. (UN) supplies only the forward flows $e^{tX}$, $t\ge0$, of the directions in the span of $S$. The Hörmander condition is a statement about the Lie algebra they generate, while the class is a semigroup closed under limits. The naive argument applies the Lie-algebra/Lie-group correspondence directly, but that correspondence speaks about the group generated by the flows $e^{tX}$, $t\in\mathbb R$. The class contains only nonnegative times and their compositions and limits, so the step from the generated group to the closed semigroup is exactly what has to be supplied.

The remaining milestones are explicit matrix analysis: exponentials of explicit superoperators on one qubit and their limits as $t\to\infty$, and register swaps. Milestone 7 has two halves. The inclusion $\supseteq$ is the construction. The inclusion $\subseteq$ requires every element of the closed class, limits included, to be positive and trace-preserving.

Formalization scope

• Carrier. The basis of $\mathbb C^{2^k}$ is indexed by bit strings Fin k → Bool, with false $=|0\rangle$. Operators are complex matrices on this index set. Superoperators are continuous $\mathbb C$-linear maps with the operator norm over the $L^2$-operator norm on matrices. In finite dimension every norm gives the same topology, so closedness and limits do not depend on this choice. Exponentials are NormedSpace.exp on matrices and on superoperators. Milestones 3 and 4 are stated on $2\times2$ matrices indexed by Fin 2, with basis order $(|0\rangle,|1\rangle)$.

• The class. $\overline{\mathrm{Channel}(S)}$ is the intersection of all closed sets with (UN), (JU) and (CO). A formalization in which some class with these properties is merely assumed to exist would make the goal trivial (take all superoperators), and is ruled out. Likewise, the Hörmander hypothesis is containment of $\mathfrak{su}(2^k)$ in the generated real Lie algebra, not in the span of $S$.

• Conventions committed to.

  • The dissipator has the standard sign $2a\rho a^*-a^*a\rho-\rho a^*a$. The page prints (JU) with the opposite sign, but every computation in the paper uses this one.
  • $S=S^*$ means $a\in S\Rightarrow a^*\in S$.
  • $k\ge1$ is assumed wherever the first qubit is named; the first qubit is index $0$.
  • Proposition 2.2(i) is posed for every unitary $U$, as its proof and its uses read it.
  • The middle term of the page's $L_Z$ display is a slip; the outer identity $L_Z=4(E_\infty-\mathrm{id})$ is posed.
  • In Lemma 2.11(iii), the printed "$|0\rangle\langle I|\otimes 1^{k-1}$" is read as $|0\rangle\langle1|\otimes I^{\otimes(k-1)}$.

• Infrastructure needed.

  • Generation of $SU(d)$ from one-parameter subgroups of a Lie-generating set.
  • Positivity and trace preservation of $e^{tL}$ for Lindblad $L$, and stability of complete positivity under limits.
  • Exponentials of superoperators that act diagonally on matrix units.
  • Swap and tensor-product manipulations on bit-string indices.

  The first two are reusable well beyond this mission. Proofs of individual milestones, and of general lemmas on Lindblad semigroups, are welcome.

Selected references

• J. Cai, A. Govindarajan, M. Junge, How Far do Lindbladians Go?, arXiv preprint, v2, 2025. https://arxiv.org/abs/2504.04883
• V. Gorini, A. Kossakowski, E. C. G. Sudarshan, Completely positive dynamical semigroups of N-level systems, J. Math. Phys. 17 (1976) 821–825. https://doi.org/10.1063/1.522979
• G. Lindblad, On the generators of quantum dynamical semigroups, Comm. Math. Phys. 48 (1976) 119–130. https://doi.org/10.1007/BF01608499
• W.-L. Chow, Über Systeme von linearen partiellen Differentialgleichungen erster Ordnung, Math. Ann. 117 (1940) 98–105. https://doi.org/10.1007/BF01450011
• R. W. Brockett, System theory on group manifolds and coset spaces, SIAM J. Control 10 (1972) 265–284. https://doi.org/10.1137/0310021
• V. Jurdjevic, H. J. Sussmann, Control systems on Lie groups, J. Differential Equations 12 (1972) 313–329. https://doi.org/10.1016/0022-0396(72)90035-6
• R. Cleve, C. Wang, Efficient quantum algorithms for simulating Lindblad evolution, arXiv preprint, 2016. https://arxiv.org/abs/1612.09512
• R. Araiza, Y. Chen, M. Junge, P. Wu, Resource-dependent complexity of quantum channels, arXiv preprint, 2023. https://arxiv.org/abs/2303.11304
• F. Verstraete, M. M. Wolf, J. I. Cirac, Quantum computation and quantum-state engineering driven by dissipation, Nature Physics 5 (2009) 633–636. https://doi.org/10.1038/nphys1342

Time inconsistency and equilibrium controls

An agent who maximizes an expected sum of rewards over time is time-inconsistent when the plan that is optimal today stops being optimal tomorrow. This happens as soon as discounting is not exponential: with hyperbolic or quasi-hyperbolic discounting, a reward far in the future is weighed differently at time 0 and at time 1, and the agent's future selves want to revise today's plan. Strotz (Strotz 1955) proposed to treat the problem as a game between the current self and all future selves and to look for a strategy that no self wants to deviate from: an equilibrium. Non-exponential discounting is documented in experimental economics (Laibson 1997), and equilibrium controls are the standard solution concept for such problems in mathematical finance and stochastic control (Björk, Khapko, Murgoci 2017).

The basic question is whether an equilibrium exists. For a Markov decision process on a finite state space with a general action set, Huang and Zhou proved existence when the actions available in each state form a closed convex set and the reward is concave in the action. Without convexity there need not be an equilibrium among deterministic feedback controls. Bayraktar, Huang, Wang and Zhou show that existence is restored for relaxed (randomized) controls, under only Lipschitz continuity and a geometric condition on the action space. This mission formalizes their discrete-time result.

Setting

The action space is a compact set $U\subset\mathbb R^\ell$ with positive Lebesgue measure $\mathrm{Leb}(U)>0$, and the state space is $\mathcal S=\{1,\dots,d\}$. Each action $u\in U$ has a transition matrix $p^u=(p^u_{ij})$, with $i$-th row $p^u_i$. A reward function $f(t,i,u)$ depends on the time difference $t\in\mathbb N_0$, the state and the action.

A relaxed feedback control is a map $\pi:\mathcal S\to\mathcal P(U)$: in state $i$ the agent samples an action from the probability measure $\pi(i)$. The set of relaxed controls is $\Pi$. The chain then moves with the averaged matrix $p^\pi_{ij}=\int_U p^u_{ij}\,(\pi(i))(du)$, and the value is

$$J^\pi(i)=\mathbb E_i\Big[\sum_{k\ge0}f^{\pi(X_k)}(k,X_k)\Big],\qquad f^\mu(t,i)=\int_U f(t,i,u)\,\mu(du).$$

For $\pi,\pi'\in\Pi$, the concatenation $\pi'\otimes_1\pi$ uses $\pi'$ at time $0$ and $\pi$ afterwards. A control $\pi\in\Pi$ is a relaxed equilibrium if

$$J^{\pi'\otimes_1\pi}(i)-J^\pi(i)\le0\qquad\text{for all } i\in\mathcal S,\ \pi'\in\Pi .$$

The paper also uses an entropy-regularized problem. A control is regular ($\pi\in\Pi_r$) if each $\pi(i)$ has a density $\rho_i$ on $U$ whose differential entropy $\mathcal H(\rho_i)=-\int_U\rho_i\ln\rho_i\,du$ is finite. For $\lambda>0$ and a discount function $\delta$, the regularized value $J^\pi_\lambda$ adds $\lambda\delta(k)\mathcal H(\pi(X_k))$ to the reward at time $k$. A regular control is a regular relaxed equilibrium if no regular deviation $\pi'$ improves $J_\lambda$. The Gibbs density

$$\Gamma_\lambda(y,i)(u)=\frac{e^{\frac1\lambda(f(0,i,u)+p^u_i\cdot y)}}{\int_U e^{\frac1\lambda(f(0,i,v)+p^v_i\cdot y)}\,dv},\qquad y\in\mathbb R^d,$$

defines the map $\Psi_\lambda(y)=V_\lambda^{\Gamma_\lambda(y,\cdot)}$, where $V_\lambda$ is the continuation value from time $1$.

The assumptions are the following.

• Assumption 2.1: $\sum_t\big(\sup_{i,u}|f(t,i,u)|+\delta(t)\big)<\infty$.
• Assumption 2.2: $u\mapsto f(t,i,u)$ and $u\mapsto p^u_i$ are Lipschitz, uniformly in $(t,i)$, with constant $\Theta$.
• Assumption 2.3: a uniform cone condition. Some cone of fixed angle $\iota$ and fixed height $\vartheta$ with vertex at any point of $U$ lies in $U$. Polyhedra and ellipsoids satisfy it.

Formalization targets

Goal: Theorem 2.2

Under Assumptions 2.1–2.3, there exists $\pi\in\Pi$ with

$$J^{\pi'\otimes_1\pi}(i)\le J^\pi(i)\qquad\forall i\in\mathcal S,\ \forall\pi'\in\Pi.$$

The statement fixes no constants and assumes no convexity.

Regularized problem (milestones, in attack order)

1. The one-step decomposition $J^{\pi'\otimes_1\pi}_\lambda(i)=f^{\pi'(i)}(0,i)+\lambda\mathcal H(\pi'(i))+\mathbb E_i[V^\pi_\lambda(X^{\pi'}_1)]$ (p. 6).
2. $\Gamma_\lambda(y,i)$ is the unique maximizer of the one-step objective (2.11)–(2.12).
3. Proposition 2.1 and Corollary 2.1: regular relaxed equilibria correspond to fixed points $\Phi_\lambda(\pi)=\pi$, and their values to fixed points $\Psi_\lambda(y)=y$.
4. Lemma 2.1: $\sup_i|\mathcal H(\Gamma_\lambda(y,i))|\le\kappa+\ell\ln(1+|y|)$ (2.17), and $\le\kappa_1+\kappa_2|\ln\lambda|+\ell\ln(1+|y|)$ for small $\lambda$ (2.18).
5. Continuity of $\Psi_\lambda$, then Theorem 2.1: for every $\lambda>0$, $\Psi_\lambda$ has a fixed point, which gives a regular relaxed equilibrium.

Vanishing regularization

6. Lemma 2.2: fixed points $y^n=\Psi_{\lambda_n}(y^n)$ stay bounded as $\lambda_n\downarrow0$.
7. Proposition 2.2: $\pi$ is a relaxed equilibrium iff $\pi\in\Phi(\pi)=\Gamma(V^\pi)$, where $\Gamma(y)$ collects the controls carried by $\arg\max_u\{f(0,i,u)+p^u_i\cdot y\}$.
8. Two steps of the limit argument (pp. 22–23). Weak limits of Gibbs controls lie in $\Gamma(y^\infty)$, and their regularized values converge, $V^{\Gamma_{\lambda_n}(y^n,\cdot)}_{\lambda_n}\to V^{\pi^*}$ (A.12)–(A.13).

Significance

The result. Theorem 2.2 removes the convexity and concavity assumptions of the earlier existence theorem for discrete-time time-inconsistent MDPs. Its price is randomization. The action space may be a finite union of polytopes, for example, and the reward need not be concave in the action. Theorem 2.1 is of independent interest for reinforcement learning, where entropy-regularized objectives are the standard way to encourage exploration (Ziebart et al. 2008). With non-exponential discounting, the theorem guarantees a randomized policy that all future selves uphold. The regularized equilibria are fixed points of a single-valued map, and the paper (Remark 2.6) points to them as a computational route to relaxed equilibria.

The formalization. The results are proved in the paper. None of them has a machine-checked proof, and this mission produces the first. Along the way it requires a formal treatment of relaxed controls as measure-valued maps, of the differential entropy of densities on a subset of $\mathbb R^\ell$, and of Gibbs variational principles for such densities.

Difficulty

The obvious route to existence is a fixed-point theorem for the best-response correspondence on deterministic controls. It needs convex values, hence a convex action set and a concave reward, and both are absent here. Relaxing to measures restores convexity of each best-response set. However, the unregularized best response $\pi\mapsto\Gamma(V^\pi)$ is set-valued on an infinite-dimensional space, and the value $V^\pi$ depends nonlinearly on $\pi$ through the whole future of the chain. The regularized problem has a single-valued best response, but a fixed point needs a uniform bound on entropies of Gibbs densities. That bound must grow only logarithmically in $|y|$ (otherwise no ball is invariant) and stay controlled as $\lambda\to0$. The geometric Assumption 2.3 enters exactly there, and again in the limit, where Gibbs measures must concentrate on maximizers that a cusp or isolated point of $U$ would otherwise hide.

Formalization scope

Actions are points of EuclideanSpace ℝ (Fin ℓ) with $\ell>0$. The state space is Fin d, value vectors are Fin d → ℝ, and every norm $|y|$ on $\mathbb R^d$ (and $|p^{u_1}_i-p^{u_2}_i|$) is Euclidean. A control is a family of measures on $\mathbb R^\ell$:

• relaxed means probability measures carried by $U$;
• regular adds absolute continuity with respect to Lebesgue measure on $U$ and integrability of $\rho\ln\rho$ for the Radon–Nikodym density $\rho$.

Expected values are infinite sums through products of the averaged transition matrices (Remark 2.1), and the concatenation $\pi'\otimes_1\pi$ is the control sequence $(\pi',\pi,\pi,\dots)$. The p. 6 decomposition is therefore a theorem, not a definition. Weak convergence is tested against bounded continuous functions on $\mathbb R^\ell$. Constants that the paper says depend on $(\ell,\lambda,\mathrm{Leb}(U),\iota,\vartheta,\Theta)$ are quantified before $d$, $U$, $f$, $p$ and $y$.

Disclosed conventions:

• each $p^u$ is a stochastic matrix;
• $\Theta>0$;
• the cone of Assumption 2.3 has one nappe and the ball is open (weaker than the printed double cone, which no polyhedron vertex satisfies);
• measurability of $f$ and $p$ is assumed where only Assumption 2.1 is cited;
• $\operatorname{supp}\pi(i)\subseteq E$ is written $\pi(i)(E^c)=0$.

A trivializing formalization is ruled out. Equilibria quantify over all relaxed deviations, Dirac controls included. $J^{\pi'\otimes_1\pi}$ is computed from the process, not from the one-step formula. The hypotheses of the goal are satisfiable: a verified instance with $\ell=d=1$ and $U=[-1,1]$ exists in the development.

Needed infrastructure, reusable beyond this mission:

• entropy and Gibbs principles for densities on subsets of $\mathbb R^\ell$;
• lower bounds on Lebesgue measure of cone sections;
• weak convergence on compact metric spaces;
• Brouwer's fixed-point theorem.

Proofs of any milestone and of reusable lemmas are welcome.

Selected references

• E. Bayraktar, Y.-J. Huang, Z. Wang, Z. Zhou, Relaxed Equilibria for Time-Inconsistent Markov Decision Processes, Mathematics of Operations Research, 2025; arXiv:2307.04227v2. https://arxiv.org/abs/2307.04227
• Y.-J. Huang, Z. Zhou, Strong and weak equilibria for time-inconsistent stochastic control in continuous time, Mathematics of Operations Research 46(2), 2021. https://arxiv.org/abs/1809.09243
• R. H. Strotz, Myopia and inconsistency in dynamic utility maximization, Review of Economic Studies 23(3), 1955. https://doi.org/10.2307/2295722
• D. Laibson, Golden eggs and hyperbolic discounting, Quarterly Journal of Economics 112(2), 1997. https://doi.org/10.1162/003355397555253
• T. Björk, M. Khapko, A. Murgoci, On time-inconsistent stochastic control in continuous time, Finance and Stochastics 21(2), 2017. https://doi.org/10.1007/s00780-017-0327-5
• B. D. Ziebart, A. Maas, J. A. Bagnell, A. K. Dey, Maximum entropy inverse reinforcement learning, AAAI 2008. https://cdn.aaai.org/AAAI/2008/AAAI08-227.pdf

Motivation

Firms disclose information to capital markets, but the same disclosures are read by other parties with a stake in the firm's cash flows. Labor unions are a leading example: anticipated good performance is associated with more aggressive union demands (evidence cited in Arya and Ramanan, p. 11: Bova 2013; Chung et al. 2016; Aobdia and Cheng 2018). A firm's choice of information system, that is, whether to gather information at all, whether to commit to publishing it, or whether to keep discretion over what to release, therefore trades off stock-market valuation against the union's bargaining posture.

Arya and Ramanan (Endogenizing Discretion in Disclosures, Management Science; authors' manuscript SSRN 3935991) make this choice endogenous. The ex post discretionary branch builds on the single-threshold disclosure equilibrium of Dye (1985); the ex ante branch relates to information design in the sense of Kamenica and Gentzkow (2011). The paper's main result says which information system the firm's CEO installs as a function of the union's strength.

Setting

A firm's cash flow $c$ is uniform on $[0,\bar c]$. The CEO sells her shares at an interim date and maximizes the stock price $\wp$. A union observes every public signal; bargaining costs it $k>0$ and, if undertaken, transfers an expected fraction $t\in(0,1)$ of the cash flow (in the paper $t=\lambda t'$, a success probability times a share).

The CEO first chooses an information system $I\in\{N,P,D\}$:

• $N$: nothing is learned; the public signal is $s=\phi$ (silence).
• $P$: the system learns $c$ with probability $p\in(0,1)$ and publishes it; otherwise $s=\phi$.
• $D$: the CEO privately learns $c$ with probability $p$ and then chooses, truthfully, whether to disclose it ($s=c$) or stay silent ($s=\phi$).

The union bargains if $E[c\mid I,s]>k/t$, does not if $E[c\mid I,s]<k/t$, and mixes with any probability $q\in[0,1]$ at equality (Lemma 1); the price is $\wp(I,s)=[q(1-t)+1-q]\,E[c\mid I,s]$ (Lemma 2). Throughout, $\bar c>k/[t(1-t)]$.

Under $D$, write $x=c^\phi=E[c\mid D,\phi]$ for the value of silence and $q$ for the union's bargaining probability after silence. The price of a disclosed $c$ is $V(c)=c$ for $c\le k/t$ and $(1-t)c$ for $c>k/t$, and the silence price is $[q(1-t)+1-q]\,x$. A $D$-subgame equilibrium is a pair $(x,q)$ such that $q$ is a Lemma 1 best response to $x$, and $x$ is the Bayes posterior mean of $c$ given silence when the informed CEO withholds exactly the $c$ with $V(c)$ below the silence price. The CEO's ex ante objective is the expected price $E[\wp(I,s)]$, written $E_N$, $E_P$, and $E_D(x,q)$.

Formalization targets

Goal: Proposition 9

With $k_{2A}=t\bar c[\sqrt{(1-p)(1-pt^2)}-(1-p)]/(p[1-t^2])$:

$$k\ge \tfrac{t\bar c}{2}\Rightarrow N,\qquad k_{2A}\le k<\tfrac{t\bar c}{2}\Rightarrow D,\qquad k<k_{2A}\Rightarrow P .$$

Concretely: (a) for $k\ge t\bar c/2$, $E_P<E_N$ and $E_D(x,q)<E_N$ at every $D$-subgame equilibrium; (b) for $k_{2A}\le k<t\bar c/2$, some equilibrium has $E_D>\max(E_N,E_P)$, and every equilibrium does when $k>k_{2A}$; (c) for $k<k_{2A}$, $E_N<E_P$, some equilibrium has $E_D<E_P$, and every equilibrium with $x>k/t$ does.

Milestones

• Propositions 1–4: the four equilibrium regimes of the $D$-subgame (single-tailed disclosure, Cases 2A, 2B, and the mixed Case 2C), with the closed forms $c_1^\phi$, $c^\phi_{2A}$, $c^\phi_{2B}$, $q_{2C}$ and the cutoffs $k_{1A},k_{2A},k_{2B},k_{1B}$.
• Existence of a $D$-subgame equilibrium for every admissible $k$ (§3.1, p. 22).
• Proposition 7: the expected prices under $N$, $P$, and $D$ in closed form.
• Proposition 8: the conditions $k<t\bar c/2$ and $c^\phi\le k/t$ for discretion to be optimal, in the form in which they are true.

Significance

The result says that discretion over disclosure, usually viewed as costly because the market discounts silence, can be the optimal design when a third party reacts to disclosures. The mechanism is that the CEO's ex post wish to inflate valuation lowers the value of silence, and a value of silence below the bargaining threshold $k/t$ disciplines the union. Against a weak union no information is best; against a strong one, committed public disclosure is best because it reveals all low cash flows that deter bargaining.

The result is proved in the paper by explicit computation. To our knowledge none of it is machine-checked. Formalizing it requires solving the Bayes fixed-point equations (1)–(4) for each regime, evaluating the expected prices, and comparing them across the parameter space; it also makes precise a point the paper passes over, namely that the $D$-subgame equilibrium is not unique near $k_{2A}$.

Difficulty

The value of silence is defined by a fixed point: the nondisclosure set depends on the silence price, which depends on the value of silence, which depends on the nondisclosure set. The set is a union of two intervals whose endpoints move with $k$, and the regime changes at four cutoffs, with a mixed-strategy regime in which the union's indifference pins $x=k/t$ and the fixed point is solved for $q$ instead. Each regime yields a quadratic whose relevant root must be shown to satisfy the regime's inequalities, with square roots whose radicands must be shown nonnegative.

The comparison in Proposition 9 then compares piecewise closed forms across these regimes. The first idea, that discretion is optimal exactly when the paper's selected equilibrium has $c^\phi\le k/t$, does not settle the statement for every equilibrium: just below $k_{2A}$ there are mixed equilibria at which discretion beats public disclosure, and at $k=k_{2A}$ there is a pure equilibrium at which it does not.

Formalization scope

• Representation. Everything is in ℝ. The uniform prior is encoded by Lebesgue integrals over subsets of $[0,\bar c]$ divided by $\bar c$; no probability space is introduced. The parameter $t=\lambda t'$ enters only as $t\in(0,1)$. The standing assumptions $0<t<1$, $k>0$, $0<p<1$, $\bar c>k/[t(1-t)]$ are a single predicate Standing carried by every statement. Under it, the weak-union part (a) is vacuous for $t\ge1/2$, as in the paper.
• Ties follow the paper: the informed CEO discloses at indifference (p. 16); the union does not bargain after a disclosed $c=k/t$, nor under $N$ or $P$ silence when $E[c]=k/t$ (Propositions 5–6). The union's mixing probability $q$ after silence under $D$ is part of the equilibrium.
• Multiplicity. The $D$-subgame can have several equilibria near $k_{2A}$. Example: $\bar c=1$, $t=0.4$, $p=0.8$, $k=k_{2A}-0.001$ has a Case 2A equilibrium and two mixed ones; the mixed one with $q\approx0.567$ gives $E_D\approx0.333>E_P\approx0.317$. The goal is therefore stated per equilibrium: universally in (a), in (b) for $k>k_{2A}$, and in (c) for equilibria with $x>k/t$; existentially elsewhere. Likewise Proposition 8's sufficiency is stated for every equilibrium with $c^\phi<k/t$ and for the paper's own mixed equilibrium, and the uniqueness half of the §3.1 remark is not formalized.
• The cutoff $k_{2B}$. Its printed formula is undefined at $t=1/2$ and wherever $(1-p)[1-2t+(1-p)t^2]<0$; the statements that use $k_{2B}$ (Propositions 3, 4, the corresponding cases of 7(c), and part 3 of Proposition 8) assume these conditions. The goal does not use $k_{2B}$.
• Printed slips are not copied: Proposition 4(c) prints $\wp(D,\phi)=k/t$ where the price is $[1-tq_{2C}]k/t$ (the value of silence is $k/t$), and Proposition 7(c) prints $q$ for $q_{2C}$.
• No trivialization. The expected price under $D$ is defined from an equilibrium profile through the best-response integral, never by Proposition 7's closed forms, and the goal quantifies over all pairs satisfying the Bayes fixed-point condition rather than over a given closed-form equilibrium; a statement about a single closed-form solution, or with the fixed-point condition replaced by its solution, is not this theorem.
• Infrastructure. The development needs integrals of piecewise-linear functions over unions of intervals, and the solution of quadratic fixed points with sign control of square-root radicands. Contributions of any of the milestones, of lemmas computing the nondisclosure set and the expected price for a given silence price, and of proofs of the cutoff ordering $k_{1A}\le k_{2A}<t\bar c/2$ are welcome.

Selected references

• A. Arya and R. N. V. Ramanan, Endogenizing Discretion in Disclosures, Management Science (2022/23); authors' manuscript, June 2022. https://ssrn.com/abstract=3935991, doi:10.1287/mnsc.2022.4505
• R. A. Dye, Disclosure of Nonproprietary Information, Journal of Accounting Research 23(1), 1985. https://doi.org/10.2307/2490910
• E. Kamenica and M. Gentzkow, Bayesian Persuasion, American Economic Review 101(6), 2011. https://doi.org/10.1257/aer.101.6.2590