All missions

Motivation

Semidefinite programs that arise in coding theory, extremal geometry, crossing-number bounds and polynomial optimization are often too large to solve directly, but they are invariant under a large symmetry group. Restricting the matrix variable to the invariant matrices loses nothing, and the invariant matrices form a matrix ∗-algebra. The survey of Bachoc, Gijswijt, Schrijver and Vallentin (arXiv:1007.2905, published in the Handbook on Semidefinite, Conic and Polynomial Optimization, Springer, 2012) organizes this symmetry reduction into steps. Its Step 2 (§1.2, pp. 5–7) replaces an SDP over such an algebra by an SDP over a few small blocks, and the justification of that step is a single structure theorem: every matrix ∗-algebra is ∗-isomorphic to a direct sum of full matrix algebras (Theorem 1.2, restated as Theorem 2.7 on p. 13).

The theorem is classical. It is the finite-dimensional case of the structure theory of C∗-algebras (Davidson, C∗-Algebras by Example, Chapter I.10), and in the unital, non-star form it is the Wedderburn–Artin theorem for semisimple algebras over ℂ. Its use in SDP symmetry reduction goes back to Gatermann and Parrilo (2004) and de Klerk, Pasechnik and Schrijver (2007). Section 2.5 of the survey gives a short, elementary, self-contained proof using only linear algebra; this mission follows that proof.

Setting

A matrix ∗-algebra (Definition 2.1, p. 10) is a complex linear subspace $\mathcal A \subseteq \mathbb C^{n\times n}$ that is closed under matrix multiplication and under the conjugate transpose $X \mapsto X^*$. It need not contain the identity matrix, and it may be $\{0\}$.

A map $\varphi : \mathcal A \to \mathcal B$ between matrix ∗-algebras is a ∗-homomorphism (Definition 2.6, p. 13) if it is linear, satisfies $\varphi(XY) = \varphi(X)\varphi(Y)$ and $\varphi(X^*) = \varphi(X)^*$; a bijective ∗-homomorphism is a ∗-isomorphism. The direct sum $\bigoplus_{k=1}^d \mathbb C^{m_k\times m_k}$ is the algebra of block-diagonal matrices with diagonal blocks of sizes $m_1, \dots, m_d$ (p. 10).

The proof uses the following vocabulary (p. 13). The center of $\mathcal A$ is $\mathcal C_{\mathcal A} = \{Z \in \mathcal A : ZX = XZ \text{ for all } X \in \mathcal A\}$. The unit of $\mathcal A$ is the unique $E \in \mathcal A$ with $EX = XE = X$ for all $X \in \mathcal A$. $\mathcal A$ is simple if it is non-zero and $\mathcal C_{\mathcal A} = \mathbb C E$. For a partition $[n] = S_0 \cup S_1 \cup \dots \cup S_k$, $I_i$ is the zero-one diagonal matrix with ones in the positions of $S_i$.

Formalization targets

Goal: Theorem 2.7 (= Theorem 1.2), p. 13

For every matrix ∗-algebra $\mathcal A \subseteq \mathbb C^{n\times n}$ there are $d$ and $m_1, \dots, m_d$ and a ∗-isomorphism

The goal fixes no sizes: it asserts only the existence of the block structure, which is the form Step 2 uses.

Milestones, in the order of the paper's proof

1. Theorem 2.2 (p. 11): a commutative matrix ∗-algebra is unitarily similar to $\{\lambda_1 I_1 + \dots + \lambda_k I_k : \lambda_i \in \mathbb C\}$ for a partition with $S_1, \dots, S_k$ nonempty and $S_0$ possibly empty.
2. A maximal commutative ∗-subalgebra $\mathcal B$ of $\mathcal A$ contains every element of $\mathcal A$ that commutes with $\mathcal B$ (p. 14).
3. Observations (i)–(ii) (p. 14): with $\mathcal B$ in diagonal form, for $X \in \mathcal A$ each $I_iXI_i$ is a multiple of $I_i$, and $I_0X = XI_0 = 0$.
4. Observation (iii) (p. 14): each block $I_iXI_j$ is zero or a nonzero multiple of a square unitary matrix.
5. The unit of $\mathcal A$ exists and is unique (p. 13).
6. The relation $i \sim j \iff I_i\mathcal A I_j \neq \{0\}$ is an equivalence relation (p. 14).
7. $\mathcal A = \bigoplus_{i=1}^d E_i\mathcal A$, where $E_1, \dots, E_d$ are the minimal idempotents of $\mathcal C_{\mathcal A}$ and each $E_i\mathcal A$ is simple (p. 14).
8. Every simple matrix ∗-algebra is ∗-isomorphic to a full matrix algebra $\mathbb C^{k\times k}$ (p. 14, proved pp. 14–15).

Milestones 7 and 8 together give the goal.

Significance

The result. A ∗-isomorphism preserves positive semidefiniteness, so Theorem 2.7 turns the constraint "$X \in \mathcal A$, $X \succeq 0$" into $d$ independent constraints on blocks of sizes $m_1, \dots, m_d$, with $\sum_k m_k^2 = \dim \mathcal A$. This is what makes the Lovász ϑ-number of symmetric graphs, the Delsarte and Schrijver bounds for codes, and the crossing-number bound of de Klerk et al. computable at scale (§§4–6 of the survey). Without it, an invariant SDP still has a variable of the original size $n$.

Formalizing it. The theorem is proved and textbook material; it is not open. As far as a search of the platform shows, it is not formalized in this form: Mathlib has Wedderburn–Artin for semisimple unital algebras over an algebraically closed field, which yields an algebra isomorphism but neither the star structure nor the non-unital case, and the platform holds a proved matrix-units statement for unital ∗-subalgebras (HarlowTASI.fdStarAlgebra_exists_matrixUnits, attached to this mission as a reference). The mission adds the non-unital ∗-isomorphism, the simultaneous unitary diagonalization of a commutative matrix ∗-algebra, and the intermediate facts of the elementary proof, each stated in a reusable form.

Difficulty

Two points make the obvious routes insufficient. First, a matrix ∗-algebra need not contain the identity: its unit is a projection onto a subspace, and the coordinates in $S_0$ carry no part of the algebra. Statements and arguments that start from a unital subalgebra do not apply without first cutting the algebra down to the range of its unit. Second, an algebra isomorphism onto a product of matrix algebras is not enough: the isomorphism must commute with the conjugate transpose, since positive semidefiniteness is defined through it. Abstract Wedderburn–Artin provides the first kind of isomorphism, and turning it into a ∗-isomorphism requires choosing the matrix units compatibly with the adjoint, which is where the content of the theorem lies. The elementary proof avoids ring theory entirely but has to control every off-diagonal block $I_iXI_j$, which is the role of observations (i)–(iii).

Formalization scope

• A matrix ∗-algebra is NonUnitalStarSubalgebra ℂ (Matrix (Fin n) (Fin n) ℂ); Mathlib's star on matrices is the conjugate transpose. The index set $[n]$ is Fin n (0-based).
• A ∗-isomorphism is StarAlgEquiv ℂ (≃⋆ₐ[ℂ]) on the subtype of $\mathcal A$: additive, multiplicative, ℂ-linear, star-preserving and bijective, exactly Definition 2.6.
• $\bigoplus_{k=1}^d \mathbb C^{m_k\times m_k}$ is the product type (k : Fin d) → Matrix (Fin (m k)) (Fin (m k)) ℂ with pointwise operations and star; it is ∗-isomorphic to the block-diagonal algebra (Matrix.blockDiagonal'). $d = 0$ is allowed and is needed for $\mathcal A = \{0\}$.
• A partition $[n] = S_0 \cup S_1 \cup \dots \cup S_k$ is a map S : Fin n → Option (Fin k), with none for $S_0$ and some i for $S_{i+1}$; the paper's block $A_{ij}$ is represented by the full-size product $I_iXI_j$.
• The center is the set of elements of $\mathcal A$ commuting with $\mathcal A$, not the commutant in $\mathbb C^{n\times n}$. "Simple" is the paper's definition: non-zero, with center $\mathbb C E$ for the unit $E$.
• Milestones 3, 4 and 6 are stated in the proof's normalized setting: $\mathcal B$ is a maximal commutative ∗-subalgebra of $\mathcal A$ that is already in diagonal form; the unitary change of basis is milestone 1.

The goal is not to be read with a unital StarSubalgebra (that adds the hypothesis $I \in \mathcal A$ and is the case already covered by the reference item), with an AlgEquiv that ignores the star, or with a mere linear equivalence (which exists for dimensional reasons and has no content). Each of these would trivialize or weaken the statement.

Useful infrastructure, reusable beyond this mission: simultaneous unitary diagonalization of commuting normal matrices, the unit and the central decomposition of a non-unital finite-dimensional ∗-algebra, and an explicit ∗-isomorphism from a corner algebra onto $\mathbb C^{k\times k}$. Proofs of any milestone, and alternative routes to the goal (for example through Mathlib's Wedderburn–Artin plus a star-compatibility argument), are welcome.

Selected references

• C. Bachoc, D. C. Gijswijt, A. Schrijver, F. Vallentin, Invariant semidefinite programs, in: Handbook on Semidefinite, Conic and Polynomial Optimization, Springer, 2012. arXiv:1007.2905v2. https://arxiv.org/abs/1007.2905
• K. R. Davidson, C∗-Algebras by Example, Fields Institute Monographs 6, American Mathematical Society, 1996. https://doi.org/10.1090/fim/006
• K. Gatermann, P. A. Parrilo, Symmetry groups, semidefinite programs, and sums of squares, Journal of Pure and Applied Algebra 192 (2004) 95–128. https://doi.org/10.1016/j.jpaa.2003.12.011
• E. de Klerk, D. V. Pasechnik, A. Schrijver, Reduction of symmetric semidefinite programs using the regular ∗-representation, Mathematical Programming 109 (2007) 613–624. https://doi.org/10.1007/s10107-006-0039-7
• R. A. Horn, C. R. Johnson, Matrix Analysis, Cambridge University Press, 1985. https://doi.org/10.1017/CBO9780511810817

Reverse convex sets and intersection cuts

A reverse convex set is the part of a polyhedron that lies outside an open convex set: $P\setminus C$, where $P=\{x\in\mathbb{R}^n_+ : Ax=b\}$ and $C\subseteq\mathbb{R}^n$ is open and convex. Such sets arise whenever a model forbids a convex region: integrality (a lattice-free convex set contains no feasible point in its interior), bilevel programs, where the points with $d^\top y>\Phi(x)$ for a convex value function $\Phi$ are infeasible, and nonconvex quadratic or polynomial constraints. Optimizing over $P\setminus C$ calls for valid inequalities for its closed convex hull.

The classical tool is the intersection cut of Balas (Balas 1971): starting from a basic solution $\bar x$ of the linear relaxation that lies inside $C$, one follows the extreme rays of the basis cone until they leave $C$, and the exit points define a valid inequality. Towle and Luedtke study the opposite case, where the basic solution lies outside the closure of $C$. Then the rays of the basis cone may enter $C$, cross it, or never leave it, and no single inequality captures the structure. They replace the cut by a disjunction: a finite union of simpler sets that contains $P\setminus C$, to which the disjunctive programming machinery of Balas can be applied. The present mission targets their multi-term disjunction (Theorem 5 of the paper), which uses the full recession cone of $C$.

Setting

Let $A\in\mathbb{R}^{m\times n}$ have full row rank and $b\in\mathbb{R}^m$. A basis splits the variables into basic variables $B$ and nonbasic variables $N$, with a tableau $\bar a$ and a basic solution $\bar x$ ($\bar x_j=0$ for $j\in N$) such that $Ax=b$ holds exactly when $x_i=\bar x_i-\sum_{j\in N}\bar a_{ij}x_j$ for all $i\in B$. Dropping the sign constraints on the basic variables gives the basis cone

a translated simplicial cone with apex $\bar x$ and extreme rays $\bar r^j$ ($j\in N$): $\bar r^j_j=1$, $\bar r^j_k=-\bar a_{kj}$ for $k\in B$, and $\bar r^j_k=0$ for the other nonbasic $k$.

The recession cone of $C$ is $\operatorname{recc}(C)=\{d : x+td\in C\text{ for all }x\in C,\ t\ge 0\}$. Along each ray, the halfline $\bar x+\lambda\bar r^j$, $\lambda\ge 0$, meets $C$ in an interval with endpoints

in the extended reals, with $\alpha_j=+\infty$, $\beta_j=-\infty$ when the halfline misses $C$. This sorts the nonbasic indices into $N_0$ (the ray misses $C$), $N_1$ ($\alpha_j$ finite and positive, $\beta_j=+\infty$: the ray enters $C$ and stays) and $N_2$ ($\alpha_j<\beta_j<+\infty$: the ray crosses $C$); write $N_0^{\mathrm c}=N_1\cup N_2$. For extended reals $\alpha<\beta$ and a vector $r$, the segment $(\alpha,\beta)r$ is $\{\lambda r:\lambda\in\mathbb{R},\ \alpha<\lambda<\beta\}$, and $[0,\beta)r$, $(-\infty,0]r$ are defined likewise. The paper builds the inner approximation of $C$

and the sets

Throughout, $\bar x\notin\operatorname{cl}(C)$, and (Assumption 2 of the paper) $\operatorname{recc}(C)\subseteq\operatorname{recc}(P^B)$.

Formalization targets

Goal: Theorem 5

With $N_2^0:=N_2\cup\{0\}$,

The relaxation $P^B\setminus T^C$ of $P^B\setminus C$ is thus a disjunction of $|N_2|+1$ terms.

Milestones

1. (§3, p. 5) $\bar r^j\in\operatorname{recc}(C)$ for every $j\in N_1$.
2. (Proposition 5) For $k\in N_2$, $S^C_k=\{\bar x\}+\operatorname{conv}\big(\bigcup_{j\in N_0^{\mathrm c}}(\alpha_j,\beta_j)\bar r^j\big)+(-\infty,0]\bar r^k+\operatorname{recc}(C)$.
3. (Lemma 2) For $a,c\in\mathbb{R}^s_+$ with $\sum_i a_i>0$ there is $\theta\in\mathbb{R}^{s+1}_+$ with $\sum_{i=0}^s\theta_i=1$ and $a_i\theta_0=c_i\theta_i$ for $i=1,\dots,s$.
4. (Proof of Theorem 5) $T^C\subseteq S^C_k$ for every $k\in N_2^0$.
5. (Proof of Theorem 5) $T^C=\bigcap_{k\in N_2^0}S^C_k$.

Significance

Theorem 5 turns the nonconvex set $P^B\setminus T^C$ into a finite union of sets with explicit generators. By the paper's Theorem 2, $P^B\setminus T^C$ has the same closed convex hull as $P^B\setminus C$, so valid inequalities for the disjunction are valid for the reverse convex set and lose nothing in the limit. The paper then relaxes each term to a polyhedron (§4.4), and a cut-generating linear program over the union separates candidate points; when $C$ is bounded the disjunction collapses to the two-term disjunction of the paper's Theorem 1. The disjunction is therefore the bridge between the geometry of $C$ (its recession cone and the exit parameters along the basis rays) and polyhedral cut generation.

The result is proved in the paper (arXiv:1901.02112v5, pp. 17–18; Mathematics of Operations Research, 2022). It has no machine-checked proof. Formalizing it checks the extended-real conventions for $\alpha_j,\beta_j$, the treatment of empty and unbounded segments, and the role of the recession cone, all of which the paper handles in prose. The definitions of the basis cone, the exit parameters and the recession cone are reusable for other intersection-cut results on the platform.

Difficulty

The inclusion $T^C\subseteq\bigcap_k S^C_k$ is immediate from the definitions. The reverse inclusion is the substance: a point lying in every term $S^C_k$ comes with $|N_2|+1$ unrelated representations, one per term, each using different segment parameters, a different multiple of $-\bar r^k$ and a different recession direction. A point of $T^C$ needs a single representation with all segment parameters inside $(\alpha_j,\beta_j)$ and no negative multiples of the rays. A naive average of the representations keeps the negative components along the rays $\bar r^k$, so it does not land in $T^C$. The rewriting of $S^C_k$ in Proposition 5 also needs care: it replaces $[0,\beta_j)$ by $(\alpha_j,\beta_j)$ inside a convex hull, and absorbs the rays of $N_1$ into the recession cone, which holds only because $C$ is open.

Formalization scope

Vectors are functions $\iota\to\mathbb{R}$ on a finite index type $\iota$ (the paper's $\{1,\dots,n\}$). The basis is the published Disjunctive.GeneralDisjunctions.IsTableau (a genuine tableau of $Ax=b$, with $B,N$ a partition and $\bar x_N=0$) together with $\operatorname{rank}A=m$, and the extreme rays are the published Disjunctive.GeneralDisjunctions.extremeRay. $P^B$ is defined, as on the page, by the tableau equations and $x_N\ge 0$. The exit parameters $\alpha_j,\beta_j$ are EReal-valued infima and suprema over real parameters, so the empty set gives $+\infty$ and $-\infty$ and an unbounded set gives $\beta_j=+\infty$; segments quantify over real $\lambda$ compared with extended-real endpoints. $N_0,N_1,N_2$ are filters of $N$, and $N_0^{\mathrm c}=N_1\cup N_2$. The index $0$ of $N_2^0$ is encoded by stating the term $S^C_0$ separately from the terms $S^C_k$, $k\in N_2$. The recession cone is the universal-quantifier cone, which is the whole space for $C=\emptyset$; in that case every set in the goal is empty or $P^B$ and the identity is $P^B=P^B$.

All hypotheses are the paper's: $C$ open and convex, $A$ of full row rank (§2), $\bar x\notin\operatorname{cl}(C)$ (§3), and Assumption 2 (§4). One generalization: the basic solution need not be feasible ($\bar b\ge 0$ is not imposed); the paper's own Example 2 uses an infeasible basic solution and the proof of Theorem 5 does not use feasibility.

Real-valued $\alpha_j,\beta_j$ (where an empty or unbounded parameter set returns $0$), segments with endpoints converted to reals, or an encoding in which $N_2$ is always empty would trivialize the statement; the extended-real definitions rule these out, and a sorry-free check confirms that the hypotheses are satisfiable with $N_2\neq\emptyset$ (one variable, $C=\{1<x<2\}$).

The development needs Minkowski sums and convex hulls of unions in $\mathbb{R}^n$, recession cones of open convex sets, and a Farkas-type alternative (for Lemma 2); the platform's LinearOptimization.farkas_lemma is available. Proofs of the milestones in any order are welcome; Lemma 2 is self-contained.

Selected references

• E. Towle and J. Luedtke, Intersection disjunctions for reverse convex sets, arXiv:1901.02112v5, 2020; Mathematics of Operations Research, 2022. https://arxiv.org/abs/1901.02112v5
• E. Balas, Intersection cuts — a new type of cutting planes for integer programming, Operations Research 19(1), 1971. https://doi.org/10.1287/opre.19.1.19
• E. Balas, Disjunctive programming, Annals of Discrete Mathematics 5, 1979. https://doi.org/10.1016/S0167-5060(08)70342-X
• M. Conforti, G. Cornuéjols, G. Zambelli, Integer Programming, Springer, 2014. https://doi.org/10.1007/978-3-319-11008-0

Motivation

A creator-side experiment on a short-video platform may assign treatment to individual videos while measuring outcomes over a viewer's whole session. A treated video can alter what the viewer watches next, so its effect may persist beyond the immediate reward. The paper studies this form of interference using a Markov decision process and asks how well data from a per-video experiment estimate the effect of treating every video instead of none. Its motivating application is an experiment at Douyin, where viewer state includes attention and other factors that need not be observed by the estimator. Farias et al., 2023 give an estimator based on reward-to-go and a quantitative bias bound for an absorbing-session model.

The distinction matters for experimental design: the usual inverse-propensity estimate weights only the reward received immediately after an assigned action. In this setting it can omit the effect of that action on later rewards. The paper's Differences-in-Qs (DQ) statistic instead weights the remaining reward in the session after each assignment. The mission focuses on the theorem that quantifies the resulting bias in the finite absorbing model of Sections 3–5.

Setting

Let $S$ be a finite state set and let the actions be control $0$ and treatment $1$. An action $a$ has a stochastic transition matrix $P_a(s,s')$ and conditional mean reward $r(s,a)$. The initial state has probability law $\rho_{\rm init}$. A stationary policy $\pi$ assigns action probabilities at each state; its induced transition matrix is $P_\pi(s,s')=\sum_a\pi(s,a)P_a(s,s')$. Global control $\pi_0$ always selects $0$, global treatment $\pi_1$ always selects $1$, and the experiment $\pi_{1/2}$ independently selects each action with probability one half at each step. Thus $P_{\pi_{1/2}}=(P_0+P_1)/2$.

A path consists of successive state-action pairs $(s_t,a_t)$. Its law begins with $s_0\sim\rho_{\rm init}$, draws each action from $\pi(s_t)$, and then draws $s_{t+1}$ from $P_{a_t}(s_t,\cdot)$. The total expected reward is $J_\pi=\sum_{t\ge0}\mathbb E_\pi[r(s_t,a_t)]$. The target average treatment effect is ${\rm ATE}=J_{\pi_1}-J_{\pi_0}$.

The session has a common absorbing class $S_{\rm abs}$: under each policy of interest, transitions from this class stay in it, and its mean rewards vanish. Assumption 1 bounds the expected number of steps spent outside that class, from every initial state, strictly by $T_{\rm abs}$. These conditions make the infinite total-reward quantities meaningful. The paper writes a stronger absorbing-row equation that does not define a stochastic row when the class contains more than one state; the formalization uses the closed-class interpretation and records the discrepancy for review.

For a path from the half-treatment policy, the DQ estimator assigns weight $2$ or $-2$ to the reward remaining after each treatment or control action, respectively. With the path stopped at $H$, write that statistic as $\widehat{\rm ATE}^{(H)}_{\rm DQ}$. The infinite-horizon expectation is defined through the limit of its finite-path expectations, not through a value-function identity.

Formalization targets

The goal is Theorem 1 of Farias et al., in the absorbing regime. If every row of $P_1-P_0$ has total-variation norm at most $\delta$ and $r_{\max}=\max_{s,a}|r(s,a)|$, then the estimator expectations converge to $L$ and

The milestone targets include the matrix resolvent identities of Lemmas 1–2, Theorem 2's finite-order expansion of the total-reward value functional, and Corollary 1's absorbing-case remainder bound. They also identify trajectory reward with the value functional and connect the trajectory DQ statistic to the first-order expansion. The listed order follows these mathematical dependencies. The mission does not assert Theorem 2's discounted, average-reward, or finite-horizon cases, which the goal does not need.

Significance

The bound distinguishes the DQ estimator from an immediate-reward estimate: its bias is at most quadratic in the row distance $\delta$, with explicit dependence on expected session length and reward magnitude. It gives a criterion for when a per-video experiment can approximate the all-treatment versus all-control effect despite changes to later states. This is a statement about expected estimator bias; it does not by itself give a variance or finite-sample confidence bound.

The formal development separates three objects that are easy to conflate: the statistic computed from a trajectory, its expectation under the experimental policy, and a value-functional expansion used to analyze that expectation. The matrix identity corresponding to Lemma 1 is already machine checked on Prove2Me as MarkovEntanglement.resolvent_identity. The goal and other mission statements are compilation-checked drafts with proof obligations still open. A completed formalization would establish their convergence and equality claims as well as the printed bias constant, and would leave reusable finite-state path and absorbing-value definitions.

Difficulty

The immediate-reward estimate evaluates outcomes under the experimental state distribution, while ATE compares outcomes under two different state distributions. Weighting each current reward cannot generally account for that mismatch. The DQ statistic incorporates reward-to-go, but its infinite double sum must be related to a convergent trajectory expectation before any bias inequality applies. The central quantitative issue is to control how changing a policy perturbs the total-reward functional across repeated transitions, with the exact $T_{\rm abs}^{3}\delta^{2}$ scale. A direct comparison of one-step rewards alone does not yield that order.

Formalization scope

States and actions are finite. Transitions are nonnegative and row-stochastic, the initial law is a probability vector, and policies are stationary probability kernels. The goal's actions are Fin 2, with $1$ treatment and $0$ control. Path expectations are finite sums; infinite expected rewards and Q-functions use real series. The absorption-time condition asserts convergence with HasSum and a strict bound from every state. Its closed-class, zero-reward conditions apply under $\pi_0$, $\pi_1$, and $\pi_{1/2}$. The reward field records conditional means, sufficient for the expectation claims.

Here $D_{\rm TV}$ is the $\ell_1$ row norm $\sum_{s'}|P(s,s')-Q(s,s')|$. The paper does not define its normalization; with the alternative half-$\ell_1$ convention the printed Theorem 1 constant fails. This choice is part of the statement, not a hidden rescaling. The truncated estimator is formed from path rewards exactly as equation (4) prescribes; defining its expectation as the first-order expansion would erase the mission's main identification step. The paper's Section 5.3 display also places the outer value functionals at $\pi_1$ and $\pi_0$, while its claimed identity and Theorem 2 require $\pi_{1/2}$; the milestone states that corrected reading and retains the printed display in its provenance.

Useful contributions include convergence of finite-path expectations, the absorbing total-reward resolvent theory, and the exact finite-order remainder estimate. These definitions and lemmas can also support other finite absorbing policy-evaluation problems.

Selected references

• Vivek F. Farias, Hao Li, Tianyi Peng, Xinyuanyang Ren, Huawei Zhang, and Andrew Zheng, Correcting for Interference in Experiments: A Case Study at Douyin, RecSys, 2023; arXiv:2305.02542v1.

Motivation

Quadratic hedging chooses a self-financing trading strategy that minimizes the expected squared difference between its terminal value and a payoff $H$; with $H$ constant it becomes mean–variance portfolio selection. The classical theory works in discounted prices: one asset is a risk-free numeraire, and optimal strategies are written in terms of the remaining assets (Černý and Kallsen 2007; the paper refers to Schweizer's 2010 encyclopedia entry Mean–variance hedging for an overview). Černý, Czichowsky and Kallsen drop that assumption. In their market no asset need be risk-free, and they want formulas for the optimal strategy that do not depend on which asset is used as the unit of account (arXiv:2110.09416v4, §1).

In their feedback formula (Theorem 4.1, p. 15) the optimal strategy is built from two processes. One is the adjustment process $a$, which corrects the hedging error accumulated so far. The other is the pure hedge $\xi$, which offsets the fluctuations of the claim's value process. At each time both are minimizers of a finite-dimensional quadratic problem with one linear budget constraint. The covariance-type matrix in that problem may be singular, for instance whenever a risk-free asset is present. So the minimizers are not unique and ordinary matrix inversion does not describe them. Theorem 4.3 of the paper (p. 16) gives explicit formulas for the whole solution sets, and Appendix A (pp. 24–28) proves the linear algebra behind them. That linear algebra is a general result on affinely constrained quadratic minimization with singular data, built on the oblique-projector analysis of Černý 2009.

Setting

Fix a time and a state. The data of the pointwise problem are:

• a symmetric positive semidefinite matrix $C=\tilde c^{S\star}\in\mathbb R^{d\times d}$, the modified second characteristic of the price process $S$ under the opportunity-neutral measure;
• vectors $b=b^{S\star}$ (drift), $s=S_-\neq0$ (current prices) and $u=\tilde c^{SV\star}$ (covariation of prices with the claim's value process) in $\mathbb R^d$, and a scalar $v=V_-$.

Portfolios $\vartheta$ are row vectors and price-type quantities are column vectors, as in the paper (§2, p. 6). $R(\cdot)$ is the column space and $N(\cdot)$ the null space of a matrix. Every matrix exponent $^{-1}$ in the paper denotes the Moore–Penrose pseudoinverse: the unique $X$ with $AXA=A$, $XAX=X$, $(AX)^{\mathsf T}=AX$, $(XA)^{\mathsf T}=XA$ (p. 24, (A.2)). The two problems are

where an $\operatorname{arg\,min}$ is the set of all global minimizers over the whole hyperplane (possibly empty). With $m=I-ss^{\mathsf T}/(s^{\mathsf T}s)$ and $p=(mCm)^{-1}$ the paper defines

The general problem of Appendix A is to minimize $q(x)=x^{\mathsf T}Cx-2x^{\mathsf T}F$ over $\{x: Ax=b\}$ with $b\in R(A)$, where $M=I-A^{-1}A$ and $J=(MCM)^{-1}$.

Formalization targets

Goal: Theorem 4.3

1. $\Xi_a\neq\varnothing$ if and only if $b\in R(C)+R(s)$; in that case $\Xi_a=a+N(C)\cap N(s^{\mathsf T})$ and $a$ is its minimum-norm element.
2. $\Xi_\xi=\xi+N(C)\cap N(s^{\mathsf T})$, and $\xi$ is its minimum-norm element.
3. If $s\in R(C)$: $\;a=b^{\mathsf T}C^{-1}-\bigl(1+b^{\mathsf T}C^{-1}s\bigr)\dfrac{s^{\mathsf T}C^{-1}}{s^{\mathsf T}C^{-1}s}$ and $\xi=u^{\mathsf T}C^{-1}+\bigl(v-u^{\mathsf T}C^{-1}s\bigr)\dfrac{s^{\mathsf T}C^{-1}}{s^{\mathsf T}C^{-1}s}$.
4. If $s\notin R(C)$: with $\bar m=I-CC^{-1}$, $\alpha=s^{\mathsf T}\bar m/(s^{\mathsf T}\bar ms)$, $r=\alpha b$,

and $\alpha s=1$, $\alpha C=0$.

Milestones (Appendix A and the proof of Theorem 4.3)

In attack order: existence and uniqueness of the pseudoinverse (published, proved); Proposition A.1 (pseudoinverse rules); Proposition A.3 (affinely constrained least squares); (A.8) and $JCJ=J$; (A.14)–(A.15); the completed square (A.16); Theorem A.4(1) (bounded below iff $F\in R(A^{\mathsf T})+R(C)$); A.4(2) (all minimizers are $\hat x+N(C)\cap N(A)$ with $\hat x=JF+(I-JC)A^{-1}b$ of minimum norm); A.4(3) (value identities); Lemma A.5; A.4(4) (formulas (A.6)–(A.7) through the oblique projector onto $\bar Y$ along $N(A)$); and the range fact $\tilde c^{SV\star}\in R(\tilde c^{S\star})$ used in the proof of Theorem 4.3.

Significance

Theorem 4.3 gives closed forms for both ingredients of the optimal hedge. It covers markets with and without a risk-free asset in one formula, because $s\in R(C)$ and $s\notin R(C)$ are the only two cases. In the second case $\alpha$ is a fully invested portfolio with zero instantaneous variance. The paper uses them in its efficient-frontier analysis (§5) and its examples (§6). Theorem A.4 does not depend on finance. It gives a complete solution of a positive semidefinite quadratic program with linear equality constraints: when it is solvable, the full set of minimizers, and the minimum-norm minimizer. Its proof needs nothing beyond finite-dimensional linear algebra.

The paper proves all of these results. Proposition A.3 is taken from Černý (2009), and v4 (7 July 2025) strengthened Proposition A.3 and Theorem A.4 after the journal version (doi:10.1287/moor.2023.1374). The mission cites only v4. None of the statements has a machine-checked proof. The Penrose predicate and Penrose's existence and uniqueness theorem are already on Prove2Me as proved results. Mathlib at the pinned revision has no Moore–Penrose pseudoinverse, so the pseudoinverse calculus built here can be reused.

Difficulty

With a singular $C$, completing the square with an inverse is not available. On the affine set, the quadratic part can vanish in some directions while the linear part keeps decreasing. The boundedness criterion has to detect exactly these directions. Under that criterion, a formula has to describe every minimizer, not just one stationary point. The constraint brings in the projector $M=I-A^{-1}A$, and $C$ need not commute with it. As a result, the relevant projector $JC$ is oblique, not orthogonal, and the obvious guess $C^{-1}F$ plus a correction fails. Exhibiting one feasible point with zero gradient does not prove the set equality, the minimum-norm property, or the case formulas (A.7). The case $s\notin R(C)$ needs its own treatment through $\bar m$.

Formalization scope

• Vectors are Fin d → ℝ with ⬝ᵥ, and matrices are Matrix (Fin m) (Fin n) ℝ. A row vector times a matrix is written x ᵥ* M and a matrix times a column vector M *ᵥ x, matching the paper's printed order. Column and null spaces are LinearMap.range/LinearMap.ker of Matrix.toLin'.
• Each pseudoinverse is an explicit matrix with the hypothesis LocalDistanceNetwork.IsMoorePenroseInverse (the four equations (A.2)). Because the pseudoinverse exists and is unique, this is the same as "the" pseudoinverse. Lean's ⁻¹ is used only on real scalars, never on a singular matrix.
• Positive semidefinite means Matrix.PosSemidef, which includes symmetry. Argmin sets range over the whole affine set or hyperplane. Minimum norm compares squared Euclidean norms over the whole set.
• Theorem 4.3 is stated pointwise: arbitrary $C\succeq0$, $b$, $s\neq0$, $u\in R(C)$, $v$. The paper's setting gives $s\neq0$ implicitly; without it, part (1) is false. The paper's "in the setting of Theorem 4.1" gives $u\in R(C)$, and the range-fact milestone derives it from positive semidefiniteness of the joint characteristic. The stochastic construction of Theorem 4.1 is out of scope. Of the last sentence of part (4), only its algebraic content $\alpha s=1$, $\alpha C=0$ is formalized.
• Appendix A states Propositions A.1 and A.3 and Lemma A.5 over $\mathbb C$. They are posed over $\mathbb R$, which is the case Theorems A.4 and 4.3 use. The two cases of (A.7) are not exhaustive when there are two or more constraints, and each is stated under its own hypothesis.
• Ruled out: an argmin defined from the advertised answer, a minimizer taken as a free parameter, and Mathlib's matrix inverse (which is $0$ on singular matrices) in place of the pseudoinverse. Each of these would make the statements trivial or change them.
• Needed infrastructure: a Moore–Penrose calculus for real matrices (Proposition A.1), ranges and kernels of products, orthogonal and oblique projectors, and minimization of quadratic forms on affine sets. All of it is reusable outside this mission, and contributions to any milestone are welcome.

Selected references

• A. Černý, C. Czichowsky, J. Kallsen, Numeraire-invariant quadratic hedging and mean–variance portfolio allocation, arXiv:2110.09416v4, 2025 (journal version: Mathematics of Operations Research 49(2), 2024). https://arxiv.org/abs/2110.09416v4
• A. Černý, Characterization of the oblique projector $U(VU)^\dagger V$ with application to constrained least squares, Linear Algebra and its Applications 431(9), 2009, 1564–1570. https://mathscinet.ams.org/mathscinet-getitem?mr=2555057
• A. Černý, J. Kallsen, On the structure of general mean–variance hedging strategies, Annals of Probability 35(4), 2007, 1479–1531. https://mathscinet.ams.org/mathscinet-getitem?mr=2330978
• A. Ben-Israel, T. N. E. Greville, Generalized Inverses: Theory and Applications, 2nd ed., CMS Books in Mathematics, Springer, 2003. https://doi.org/10.1007/b97366

Motivation

An investor can improve a portfolio by adding a zero-cost combination of long and short positions. Ordinary arbitrage asks whether such a combination pays nonnegatively in every outcome and positively in some outcomes. That test is restrictive when payoffs have both gains and losses. Arvanitis and Post instead ask whether one overlay portfolio raises expected utility for every admissible risk preference and every benchmark portfolio in a specified class. This gives an asset-pricing question that acknowledges uncertainty about investors' preferences and starting positions. The authors use the concept to study factor portfolios and transaction costs in their 2022 working paper Ordering Arbitrage Portfolios and Finding Arbitrage Opportunities (AUEB Department of Economics Working Paper 04-2022), published as Generalized Stochastic Arbitrage Opportunities in Management Science in 2024.

The target is the paper's Theorem 2.3.1, an existence condition for a pricing system. The working-paper statement needs a finite-generation condition on the utility class for its converse. The resulting mission records the corrected theorem and the general direction that does hold for arbitrary admissible utility classes.

Setting

There are finitely many base assets, indexed by $i=1,\ldots,N$. Their one-period payoff vector is $x\in\mathbb R^N$ with probability law $F$, supported on $[\mathrm{lo},\mathrm{hi}]^N$ for finite $\mathrm{lo}<\mathrm{hi}$. A benchmark position $\kappa\in K\subseteq\mathbb R^N$ costs $p^\mathsf T\kappa=c>0$. The benchmark set $K$ is closed and bounded; it can contain many portfolios and need not be convex. An overlay $\delta$ is feasible when $A\delta\leq a$, where $A$ has $R$ rows. Thus $\Delta=\{\delta:A\delta\leq a\}$ is the bounded overlay polytope, and $0\in\Delta$ is the passive choice.

The utility class $U$ contains continuously differentiable, strictly increasing, strictly concave functions $u:\mathbb R\to\mathbb R$. It is convex and uniformly bounded on bounded payoff intervals. For an overlay $\delta$, the expected utility increment relative to benchmark $\kappa$ is

A strict stochastic arbitrage opportunity is a single feasible overlay that improves every benchmark for every admissible utility. The set is

The paper's candidate stochastic discount factors are $M_{U,K}=\{x\mapsto d\,u'(x^\mathsf T\kappa):d>0,\ (u,\kappa)\in U\times K\}$. A factor $m$ assigns the present-value vector $E_F[m(x)x]$ to the base assets. The relevant polar cone is written in the paper's constraint coordinates as $\Delta^*=\{A^\mathsf T\sigma:\sigma\geq0,\ a^\mathsf T\sigma\leq0\}$. This representation encodes the overlay inequalities and their shadow prices.

Formalization targets

General pricing implication

For the paper's general convex class $U$, the existence of a mixture of marginal-utility discount factors whose present value lies in $\Delta^*$ rules out every strict stochastic arbitrage opportunity:

Corrected existential condition

If $U$ is the convex hull of a finite set of admissible utility functions, the converse is also claimed:

This is the mission's goal. The benchmark set remains any closed bounded set satisfying the budget restriction. ### Supporting milestones

The milestones follow the proof of Theorem 2.3.1 (pp. 34–35): the first-order (Karush–Kuhn–Tucker) condition for optimality on the segment $\kappa+\theta\delta$, $\theta\in[0,1]$,

the concavity bound $D(u,\kappa,\delta,F)\le E_F[u'(x^\mathsf T\kappa)x]^\mathsf T\delta$; the convexification step (9)–(10) in its pointwise form; the minimax reversal (10)–(11) and the linear-programming duality (11)–(13), both available as proved platform theorems; and the general pricing implication above.

Significance

The condition translates absence of a portfolio improvement shared by all the specified investors into the existence of a discount factor with constrained asset values. In markets with transaction costs, the cone can permit price intervals rather than one exact price vector. This connects an investor-facing arbitrage test to restrictions that can be checked through the market's linear constraints. The working paper (§2.3, p. 11) discusses that interpretation and its factor-investing application.

The result is a published mathematical claim but, in this representation, still a Lean proof obligation. A formal development would produce reusable definitions of strict utility-based arbitrage and marginal-utility pricing, plus machine-checked proofs of the valid pricing implication and the corrected converse. The two general minimax and linear-duality results referenced here already have proved Prove2Me statements; the paper-specific statements in this mission are draft goals and have no machine-checked proofs yet.

Difficulty

The converse has a quantifier problem: no single overlay can improve every utility and benchmark, even though different utilities may reject different overlays. Treating one failed endpoint comparison as a first-order optimality condition does not resolve that problem. In fact, a concave expected-utility function may end below its starting value at $\theta=1$ while initially increasing as $\theta$ leaves zero. The paper's proof makes that invalid identification. Its unrestricted utility class also permits limiting behavior that defeats the asserted converse. The finite-generation condition in the goal prevents that particular failure while retaining a nontrivial family of preferences and a general compact benchmark set.

Formalization scope

Lean uses Fin N → ℝ for payoffs and portfolio positions, a probability measure for $F$, and Bochner integrals for expectations. The almost-sure box-support condition makes the utility and marginal-utility expressions integrable under the stated continuity assumptions. The matrix inequality $A\delta\leq a$ defines $\Delta$ directly; $\Delta^*$ is the paper's $A^\mathsf T\sigma$ representation, rather than an abstract inequality definition. The set of discount factors allows every positive scale $d$ and takes the ordinary finite convex hull. The utility derivative is deriv u, justified by the continuously differentiable assumption. Lean's lo and hi name the support endpoints and aVec names the constraint right-hand side; the paper uses $a$ for both roles.

The corrected goal's finite generation of $U$ is an explicit addition to the printed Theorem 2.3.1. To see the need, take one riskless payoff $x_1=1$, a second payoff $x_2\in\{2,-1\}$ with equal probabilities, one benchmark $(1,0)$, and overlays $(0,t)$ for $0\leq t\leq1$. A convex class generated by increasingly steep, smooth, strictly concave utilities has no strict SAO, yet every candidate marginal-utility discount factor at that benchmark is a positive constant and assigns positive value to the second asset, outside $\Delta^*$.

The SAO predicate remains the actual difference of two expected utilities. Defining it through the derivative inequality would erase the principal economic question. Supporting work may establish bounded-support integration, finite-dimensional compactness, convex-hull behavior, and the relation between the matrix cone and the overlay inequalities; these are reusable for other one-period pricing models. A result that only assumes the pricing restriction, or changes the benchmark set to a singleton, does not settle this goal.

Selected references

• Stelios Arvanitis and Thierry Post, Ordering Arbitrage Portfolios and Finding Arbitrage Opportunities, Athens University of Economics and Business Department of Economics Working Paper 04-2022, March 2022; published as the Management Science article below. Theorem 2.3.1 is on printed p. 11 (PDF 12), with proof on printed pp. 34–35 (PDF 35–36).
• Stelios Arvanitis and Thierry Post, Generalized Stochastic Arbitrage Opportunities, Management Science, 2024, DOI. The mission uses the working-paper numbering and pagination.