All missions

Why sparsity limits accuracy

The Frank–Wolfe algorithm minimizes a smooth convex objective over a compact convex domain by choosing an atom through a linear optimization problem and moving toward it. On a domain that is the convex hull of atoms, each ordinary iteration introduces at most one new atom. That makes the method useful when a solution represented with few atoms is valuable, but it raises a basic question: how much accuracy can a solution with only a few atoms attain? Jaggi's 2013 analysis gives upper bounds on primal error and duality gap for four Frank–Wolfe variants. Its sparsity section supplies a matching obstruction on the unit simplex. This mission isolates that obstruction so the claimed dependence on sparsity can be checked independently of any particular implementation of the algorithm.

The paper calls the number of used atoms the sparsity of an iterate. It proves two lower bounds for one quadratic objective: a sparse point cannot have arbitrarily small objective value, and, with fewer active coordinates than the simplex dimension, it cannot have arbitrarily small duality gap. These are worst-case statements about feasible points themselves. Consequently, any method whose iterates retain the stated sparsity is subject to them, regardless of how it selects its next atom. The source statements and constants are Lemma 3 and Lemma 4, PDF p. 5.

The quadratic simplex problem

Let $n$ be a positive integer and let the unit simplex be

$$\Delta_n=\left\{x\in\mathbb R^n:x_i\ge0\text{ for every }i,\ \sum_{i=1}^n x_i=1\right\}.$$

For a vector $x$, let $\operatorname{card}(x)$ be the number of nonzero coordinates. The objective is the squared Euclidean norm $f(x)=\|x\|_2^2=\sum_i x_i^2$. Its minimum on the full simplex is $1/n$, reached at the uniform point. The paper compares that optimum with the best value permitted by a bound on $\operatorname{card}(x)$. The dimension $n$ and sparsity budget $k$ are separate: the goal assumes $k<n$, so at least one coordinate must be zero at every eligible point.

The duality gap at a feasible $x$ is

$$g_{f,\Delta_n}(x)=\max_{s\in\Delta_n}\langle x-s,\nabla f(x)\rangle.$$

For a convex objective, this gap bounds the difference between the current objective value and the optimum; the paper introduces that certificate in display (2), PDF p. 2. Here the maximum exists because the simplex is nonempty and compact and the expression is continuous in $s$. It is the same certificate computed by minimizing a linear function over the domain in a Frank–Wolfe step. The paper's Table 1, PDF p. 6 identifies the simplex linear subproblem with choosing a coordinate having the largest coefficient.

Formalization targets

Sparse objective minimum

For $1\le k\le n$, Lemma 3 asserts an attained minimum:

$$\min_{x\in\Delta_n,\ \operatorname{card}(x)\le k} f(x)=\frac1k.$$

The associated primal-error statement says that a point with exactly $k$ nonzero coordinates has $f(x)-f(x^*)\ge1/k-1/n$, where $x^*$ is an optimizer on the full simplex. The minimum and the primal-error reading are both included as draft theorems.

Duality-gap lower bound

For every natural number $k<n$, Lemma 4 states the mission goal:

$$\forall x\in\Delta_n,\quad \operatorname{card}(x)\le k\ \Longrightarrow\ g_{f,\Delta_n}(x)\ge\frac2k.$$

The threshold $k<n$ is essential to this exact value. If all coordinates may be active, the uniform optimizer has zero gap. The case $k=0$ is formally allowed by the paper's natural-number wording, but has no eligible simplex point. The formal statement keeps the paper's quantifier order and does not add a positive-$k$ hypothesis.

Three milestones accompany the goal. The first records that an atomic set and its convex hull have the same support function. The second records the simplex support value $\max_i y_i$ from Table 1. The third is Lemma 3's attained sparse minimum. They are stated as mathematical claims independent of any algorithmic running-time assertion.

What the bound establishes

The source's convergence analysis gives error guarantees that decrease with the number of iterations, while its simplex example shows that using only $k$ atoms leaves primal error at least $1/k-1/n$ and, for $k<n$, gap at least $2/k$. Together they delimit what the paper's sparsity guarantees can achieve. The duality-gap claim concerns a certificate of approximation quality, so it applies even when the optimal value is unavailable to an algorithm. The result is already proved in the 2013 paper; the open work here is its Lean formalization and the finite-dimensional facts needed to connect sparse coordinates, linear optimization, and the gap.

The formalization also produces reusable interfaces for sparse simplex optimization: a coordinate-count notion of sparsity, an attained minimum formulation, and a support-function statement that avoids making a real supremum silently return a default value on an empty or unbounded set. These can serve later work on atomic methods without tying that work to one choice of Frank–Wolfe steps.

Where the argument is delicate

Bounding the quadratic objective alone does not establish the duality-gap statement. The gap also involves the best linear comparison point $s$ in the simplex. The unrestricted simplex optimum, the optimum under a sparsity budget, and the best linear comparison are different objects and must retain their respective domains. An encoding that replaces the gap's domain with the sparse feasible set would change the theorem. Another easy mistake is to use the ambient norm of a function $\mathrm{Fin}(n)\to\mathbb R$ as the objective: that norm is the supremum norm, whereas the paper uses the Euclidean squared norm.

The paper's displayed curvature value $C_f=4$ is included as a companion statement. It uses the Euclidean diameter of the simplex, which is $\sqrt2$ for $n\ge2$. The one-dimensional simplex is a single point, so extending that equality to $n=1$ would be false. The formalized companion makes the dimension condition explicit.

Formalization scope

Vectors are functions $\mathrm{Fin}(n)\to\mathbb R$. The domain is Mathlib's $\mathrm{stdSimplex}\ \mathbb R\ (\mathrm{Fin}(n))$; the objective is an explicit sum of coordinate squares, and sparsity counts nonzero coordinates. The gradient pairing in the source is represented by the Fréchet derivative applied to a direction. For this quadratic, the two agree coordinate by coordinate. The duality gap is a real supremum of those derivative values over the simplex. Its use in the goal is guarded by $k<n$, which implies $n>0$ and makes the simplex nonempty; compactness makes the supremum a maximum. The support-function milestone states equality through all upper bounds, so it also has a meaningful reading for empty or unbounded atomic sets.

The curvature set follows display (3), PDF p. 3, with step size $0<\gamma\le1$ because the printed quotient has no value at zero. The $C_f=4$ companion assumes $n\ge2$, a necessary dimension pin beyond the paper's sentence. Other standing conditions of the general problem are discharged by the chosen quadratic and simplex, rather than added as free hypotheses. No theorem assumes the quadratic minimum, a gap maximizer, or a zero coordinate as a premise; those are consequences to be established from feasibility and sparsity. The source PDF contains the statements but not its cited appendix proofs, so formal proof contributions may use other valid arguments. The simplex support, sparse minimum, and curvature interfaces are reusable beyond this mission.

Selected references

• Martin Jaggi, Revisiting Frank-Wolfe: Projection-Free Sparse Convex Optimization, Proceedings of the 30th International Conference on Machine Learning, JMLR Workshop and Conference Proceedings 28, 2013. Proceedings page.

Motivation

An assortment planner chooses which products to offer to arriving customers. When products are grouped into nests, a customer's choice of nest depends on all the assortments offered at once. A planner may nevertheless be able to generate only a short list of promising assortments for each nest. The remaining task is to choose one assortment from each list so that their combined expected revenue is as large as possible. Testing every combination requires a number of evaluations equal to the product of the list sizes. Gallego and Topaloglu show that the choice can instead be described through a linear program whose number of constraints grows with the sum of those sizes; this is Theorem 2 of their 2014 paper, in the authors' September 11, 2013 manuscript, pp. 10–12.

This mission isolates that selection result. Later parts of the paper address how to construct useful candidate lists under cardinality, space, and pricing constraints. Here the candidates are already given, and the question is which combination earns the most. The result matters whenever the candidate lists are much smaller than the space of all assortments: it makes the last step of those algorithms an exact optimization over the candidates, without enumerating their Cartesian product.

Setting

Let $M$ be a finite set of nests and $N$ a finite set of products available in each nest. An assortment $S_i\subseteq N$ is the set offered in nest $i$. Product $j$ in nest $i$ has preference weight $v_{ij}>0$ and revenue $r_{ij}\in\mathbb R$. The empty assortment is allowed. The main model has no within-nest no-purchase option, so its total offered weight is $V_i(S_i)=\sum_{j\in S_i}v_{ij}$. The conditional revenue in nest $i$ is $R_i(S_i)=\sum_{j\in S_i}v_{ij}r_{ij}/V_i(S_i)$, with $R_i(\varnothing)=0$ under the paper's $0/0=0$ convention.

The weight of no purchase outside the nests is $v_0>0$. Each nest has a dissimilarity parameter $\gamma_i\in(0,1]$. Its attraction weight is $V_i(S_i)^{\gamma_i}$. The expected revenue of a combined assortment $S=(S_i)_{i\in M}$ is

$$\Pi(S)=\frac{\sum_{i\in M}V_i(S_i)^{\gamma_i}R_i(S_i)} {v_0+\sum_{i\in M}V_i(S_i)^{\gamma_i}}.$$

For each nest, $A_i$ is a finite nonempty collection of candidate assortments. The paper obtains these from a feasible set $C_i$, which may impose a cardinality or space constraint; Theorem 2 compares only combinations drawn from the supplied candidates. Equation (2) defines a real scalar $\widehat z$ through the maximum, over $A_i$ separately, of $V_i(S_i)^{\gamma_i}(R_i(S_i)-z)$. Problem (3) selects a maximizing candidate $\widehat S_i$ in each nest at that scalar. Linear program (4) has decision variables $(z,y_i)_{i\in M}$, minimizes $z$, and imposes $v_0z\ge\sum_i y_i$ and $y_i\ge V_i(S_i)^{\gamma_i}(R_i(S_i)-z)$ for every $i$ and every $S_i\in A_i$.

Formalization targets

The goal is the exact candidate-selection claim of Theorem 2. If $(\widehat z,\widehat y)$ minimizes $z$ among all feasible pairs of program (4), and every $\widehat S_i$ solves problem (3) at $\widehat z$, then

$$\Pi(S_1,\ldots,S_m)\le\Pi(\widehat S_1,\ldots,\widehat S_m) \qquad\text{for every }S_i\in A_i.$$

The milestones record three statements from pp. 11–12: equation (2) has a unique real root; the balance equation and its inequality form characterize the expected revenue of a fixed assortment; and Lemma 1 identifies the root as the best revenue attainable from candidate combinations while showing that local maximizers attain it. They separate the paper's numerical characterization of the best candidate revenue from its LP formulation. The target does not prescribe how the candidate lists were generated or claim that the selected combination is best among assortments outside those lists.

Significance

The theorem gives an exact, compact choice rule for assembling nestwise candidates. If the lists contain useful assortments under the original constraints, their best combination can be selected through program (4). The rest of the paper establishes candidate-generation and approximation results under particular constraint families; the stitching theorem supplies the common final selection step for those results. A larger candidate list may improve the obtainable revenue, but its Cartesian product need not be searched explicitly. The authors' manuscript, p. 12, states that program (4) has $1+m$ variables and $1+\sum_i|T_i|$ constraints when the candidates are indexed by $T_i$.

Formalizing the theorem yields a reusable statement about the interaction of a fractional revenue objective, independent nestwise candidate families, and a shared scalar LP. The published Prove2Me definition NestedLogitVariants.LP.Model already supplies the instance, $V_i$, $R_i$, $\Pi$, and the feasibility and optimality predicates for program (4). Its previously proved lp4_opt_binding concerns an equality at an LP optimum under ordered, nonnegative revenues; it does not contain Theorem 2's maximality claim under this paper's revenue assumptions. The four statements in this mission are draft targets awaiting machine-checked proofs.

Difficulty

Optimizing a candidate independently in every nest at an arbitrary value of $z$ does not generally optimize the combined revenue: the revenue denominator couples all nests. Likewise, an LP-feasible value need not be its minimum, and using such a value in problem (3) does not establish the theorem. The substantive assertion is that choosing the local maximizers at the optimal LP value solves the combined selection problem. The unique-root statement also needs care at empty assortments, where a nest contributes zero attraction and the conditional revenue uses the paper's $0/0$ convention.

Formalization scope

Nests are represented by any finite type, and products by Fin n, indexed $0,\ldots,n-1$ rather than the paper's $1,\ldots,n$. A Boolean offer vector is represented by Finset (Fin n); $\overline 0$ is the empty finset. Each $A_i$ is a finite set of such assortments. There is no single-nest or $\gamma_i=1$ specialization, and no substitution of all possible assortments for the supplied candidates. The LP assumption is its full minimum objective property, not merely feasibility. The imported LP4Optimal predicate uses a set of candidates, supplied by coercing each finite $A_i$ to a set.

The source's main model is selected from the imported general instance by setting $v_{i0}=0$. In the paper's later extension, $V_i(S_i)=v_{i0}\mathbf1(S_i\ne\overline0)+\sum_jv_{ij}S_{ij}$; this is different from the imported unmodified $v_{i0}+\sum_jv_{ij}S_{ij}$ when $S_i=\overline0$, so the extension is outside this mission. Positive $v_0$ and product weights are stated explicitly to keep the probability denominator positive and to match the model's preference interpretation. Revenues remain arbitrary real numbers: neither an order nor nonnegativity is assumed. The dissimilarities satisfy the paper's $(0,1]$ range. The paper states candidate feasibility $A_i^t\in C_i$; this mission's claim holds for arbitrary candidate collections because no step compares against $C_i$. The definitions of revenue and LP feasibility are imported, so useful contributions include proofs of the balance characterization, the root result, Lemma 1, and the final LP statement.

Selected references

• Guillermo Gallego and Huseyin Topaloglu, Constrained Assortment Optimization for the Nested Logit Model, Management Science, 2014. DOI: 10.1287/mnsc.2014.1931; authors' manuscript, September 11, 2013, pp. 7–12.
• James Davis, Guillermo Gallego, and Huseyin Topaloglu, Assortment Optimization under Variants of the Nested Logit Model, Operations Research, 2014. DOI: 10.1287/opre.2014.1256. The published Prove2Me model definition used here comes from this line of work.

Motivation

A retailer that sells through a choice model decides two things at once: which products to put on the shelf and at what price. Under the nested logit model of discrete choice, products are grouped into nests (brands, categories, store sections); a customer first picks a nest, or leaves without buying, and then picks a product inside the nest. The price of a product changes its attractiveness, and the attractiveness of every product changes the purchase probabilities of all the others, so assortment and price interact.

Gallego and Topaloglu (Management Science, 2014) study assortment optimization under the nested logit model with constraints on what may be offered in each nest. Their §6 treats joint assortment and pricing when each product can be sold at one of finitely many price levels. Earlier work on nested logit pricing, by Li and Huh (2011) and Gallego and Wang (2011), assumes that a product priced at $p_{ik}$ has preference weight $e^{\alpha_{ik}-\beta_{ik}p_{ik}}$. With a finite menu of price levels, no parametric link between price and preference weight is required, and the prices can be restricted to a range or a grid (for example $49.99, $59.99, …), as retail practice often demands.

Setting

There are $m$ nests $M$. In each nest $i$ there are $p$ products $P=\{1,\dots,p\}$, and each product can be offered at one of $b$ price levels $B=\{1,\dots,b\}$. Offering product $k$ at level $l$ in nest $i$ earns the price $\rho_{ik}^l$ and gives the product the preference weight $\nu_{ik}^l>0$. The relation between $\rho_{ik}^l$ and $\nu_{ik}^l$ is arbitrary.

Each pair (product, price level) is a virtual product. Nest $i$ has $n=pb$ virtual products $N=\{1,\dots,n\}$; $N_k\subseteq N$ is the set of the $b$ virtual products of product $k$, and the sets $N_k$ are disjoint. Virtual product $j\in N_k$ at level $l$ has revenue $r_{ij}=\rho_{ik}^l$ and preference weight $v_{ij}=\nu_{ik}^l$. An assortment of nest $i$ is a set $S_i\subseteq N$, and the feasible assortments are

$$\mathcal C_i=\Big\{S_i\in\{0,1\}^n:\ \sum_{j\in N_k}S_{ij}\le 1\ \ \forall k\in P\Big\},$$

so each product is offered at no more than one price, or not at all.

For an assortment $S_i$ write $V_i(S_i)=\sum_{j\in S_i}v_{ij}$ and $R_i(S_i)=\sum_{j\in S_i}r_{ij}v_{ij}/V_i(S_i)$, with $R_i(\emptyset)=0$. For a number $u\ge 0$, problem (7) of the paper is

$$\max_{S_i\in\mathcal C_i}\ V_i(S_i)\,\big(R_i(S_i)-u\big).$$

Its objective equals $\sum_{j\in S_i}f_{ij}(u)$ with $f_{ij}(u)=v_{ij}(r_{ij}-u)$; under $\mathcal C_i$ this is problem (12) of the paper.

Formalization targets

Goal: a small candidate collection per nest

For every nest $i$ there is a collection $\{A_i^t:t\in\mathcal T_i\}\subseteq\mathcal C_i$, fixed independently of $u$, with

$$|\mathcal T_i|\le p\,(b+1)^2+1,$$

such that for every $u\ge 0$ some $A_i^t$ is an optimal solution of problem (7). The page states $|\mathcal T_i|=O(pb^2)$; the explicit bound is the count of intervals left by the intersection points of the lines $f_{ij}$, $j\in N_k\cup\{0\}$, with $f_{i0}=0$.

Milestones

1. Selection rule (p. 24). For fixed $u$, the assortment that in each $N_k$ offers one virtual product with the largest coefficient $f_{ij}(u)$ when that coefficient is positive, and nothing otherwise, solves problem (7) over $\mathcal C_i$.
2. Order and signs (p. 24). If at $u$ and $u'$ the values $\{f_{ij}:j\in N_k\cup\{0\}\}$ are in the same weak order for every $k$, then the optimal solutions of (7) at $u$ and at $u'$ coincide.

Significance

The paper's Theorem 4 shows that a collection containing an optimal solution of (7) for every $u\ge 0$ yields an optimal solution of the full nested logit problem, and its Theorem 2 that the best combination of candidates solves a linear program with $1+m$ variables and $1+\sum_i|\mathcal T_i|$ constraints. With the goal above, the joint assortment and pricing problem is solved exactly by a linear program of polynomial size, $O(mpb^2)$ constraints, for arbitrary price–weight relations. This is one of the paper's three headline results.

The result is proved in the paper in prose, without a numbered statement. No machine-checked proof of it is known. The mission fixes the constant hidden in $O(pb^2)$, states the feasible set exactly, and isolates the two steps of the argument as separate statements.

Difficulty

The naive candidate set is all of $\mathcal C_i$, which has $(b+1)^p$ members; the content of the goal is the polynomial bound with the collection fixed before $u$. The argument must handle ties between coefficients, lines that coincide or never cross, intersection points at negative $u$, and the boundary points between intervals, where several assortments are optimal at once. The count must be made per product: a count over all pairs of virtual products gives $O(n^2)=O(p^2b^2)$ and misses the stated bound.

Formalization scope

• Nests are a type ι; virtual products are Fin n and products Fin p, both 0-based. $N_k$ is the fiber of a map prod : Fin n → Fin p; the hypothesis that every fiber has exactly $b$ elements is IsVirtualProductMap prod b. The price level of a virtual product is left implicit.
• Prices and weights are the published NestedLogitVariants.LP.Instance fields r i j and v i j; there is no parametric price–weight relation and no ordering of prices.
• Assortments are Finset (Fin n); the empty assortment is allowed and has objective $0$.
• The published $V$ is $v_{i0}+\sum_{j\in S}v_{ij}$. Every statement assumes $v_{i0}=0$, so it equals the paper's $V_i(S_i)$. The paper's extension $V_i(S_i)=v_{i0}\mathbf 1(S_i\neq\emptyset)+\sum_jv_{ij}S_{ij}$ (p. 15) is not formalized.
• Positive weights $v_{ij}>0$ are an explicit hypothesis; the paper takes them for granted.
• Optimality in problem (7) is over $\mathcal C_i$ only, for $u\ge 0$ (0 ≤ u).
• The bound $p(b+1)^2+1$ is in terms of $p$ and $b$, not $n$, and the collection is chosen before $u$. Statements with $b=1$ (pure assortment), a logit price–weight relation, no bound, or a collection chosen after $u$ are trivial or different theorems and are ruled out.

A complete development needs the reduction of (7) to the linear objective (identity (8)), the per-product optimality of problem (12), and a counting argument for the intersection points of finitely many lines on $[0,\infty)$. The last one is reusable beyond this mission: the paper's cardinality-constrained result uses the same kind of argument. Proofs of the milestones, and lemmas such as (8) for the published V and R, are welcome.

Selected references

• G. Gallego and H. Topaloglu, Constrained Assortment Optimization for the Nested Logit Model, Management Science 60(10), 2014. https://doi.org/10.1287/mnsc.2014.1931 (authors' manuscript of Sept. 11, 2013, §6, pp. 23–25).
• H. Li and W. T. Huh, Pricing Multiple Products with the Multinomial Logit and Nested Logit Models: Concavity and Implications, Manufacturing & Service Operations Management 13(4), 2011. https://doi.org/10.1287/msom.1110.0342
• G. Gallego and R. Wang, Multi-Product Price Optimization and Competition under the Nested Logit Model with Product-Differentiated Price Sensitivities, Operations Research 62(2), 2014 (working paper 2011). https://doi.org/10.1287/opre.2013.1249
• J. M. Davis, G. Gallego and H. Topaloglu, Assortment Optimization Under Variants of the Nested Logit Model, Operations Research 62(2), 2014. https://doi.org/10.1287/opre.2014.1256

Motivation

The rank of a matrix does not depend on the field in which its entries are read: a rational matrix has the same rank over $\mathbb Q$, $\mathbb R$ and $\mathbb C$, because rank is computed by Gaussian elimination, which never leaves the field of the entries. For 3-tensors, arrays $\mathcal A = [\![a_{ijk}]\!]$ with three indices, this fails. Tensor rank governs the complexity of bilinear maps (the exponent of matrix multiplication is a statement about the rank of one tensor), the uniqueness of the CANDECOMP/PARAFAC decompositions used in psychometrics and signal processing, and the identifiability of latent-variable models. In each application the field matters: algorithms are run over $\mathbb R$ or $\mathbb C$, while complexity results are often proved over $\mathbb Q$ or finite fields.

Håstad (1990) proved that deciding $\operatorname{rank}(\mathcal A) \le r$ is NP-complete over finite fields and NP-hard over $\mathbb Q$. De Silva and Lim (2008) gave real tensors whose rank over $\mathbb C$ is strictly smaller than their rank over $\mathbb R$. Hillar and Lim (2013, Theorem 1.14) showed that the same phenomenon already occurs between $\mathbb Q$ and $\mathbb R$, for a $2\times2\times2$ tensor with integer entries, so that Håstad's result over $\mathbb Q$ does not by itself say anything about rank over $\mathbb R$.

Setting

Let $E$ be a field. The outer product of $\mathbf x \in E^l$, $\mathbf y \in E^m$, $\mathbf z \in E^n$ is the tensor $\mathbf x\otimes\mathbf y\otimes\mathbf z \in E^{l\times m\times n}$ with entries $x_iy_jz_k$. The rank of $\mathcal A$ over $E$ is

$$\operatorname{rank}_E(\mathcal A) = \min\Big\{ r : \mathcal A = \sum_{s=1}^{r} \lambda_s\,\mathbf x_s\otimes\mathbf y_s\otimes\mathbf z_s,\ \ \lambda_s\in E,\ \mathbf x_s\in E^l,\ \mathbf y_s\in E^m,\ \mathbf z_s\in E^n\Big\}.$$

If $\mathcal A$ has entries in a subfield $F \subseteq E$, both $\operatorname{rank}_F(\mathcal A)$ and $\operatorname{rank}_E(\mathcal A)$ are defined, and $\operatorname{rank}_E(\mathcal A) \le \operatorname{rank}_F(\mathcal A)$.

The paper's example uses $\mathbf x = [1,0]^\top$, $\mathbf y = [0,1]^\top$ and

$$\mathcal A = 2\,\mathbf x\otimes\mathbf x\otimes\mathbf x - 4\,\mathbf y\otimes\mathbf y\otimes\mathbf x + 4\,\mathbf y\otimes\mathbf x\otimes\mathbf y - 4\,\mathbf x\otimes\mathbf y\otimes\mathbf y \in \mathbb Q^{2\times2\times2}.$$

A decomposition $\mathcal A = \mathbf u_1\otimes\mathbf u_2\otimes\mathbf u_3 + \mathbf v_1\otimes\mathbf v_2\otimes\mathbf v_3$ with $\mathbf u_i = [a_i,b_i]^\top$, $\mathbf v_i = [c_i,d_i]^\top$ is equivalent to the eight cubic equations (30) in the twelve unknowns $a_1,\dots,d_3$, one for each entry of $\mathcal A$.

In Lean, outer x y z and rankOver E A implement the two definitions, tensorA is $\mathcal A$, and System30 is (30).

Formalization targets

Goal: Theorem 1.14

$$\exists\, \mathcal A \in \mathbb Q^{2\times2\times2}:\quad \operatorname{rank}_{\mathbb R}(\mathcal A) < \operatorname{rank}_{\mathbb Q}(\mathcal A).$$

Milestones (proof of Theorem 1.14, p. 0:26)

1. With $\mathbf z = \mathbf x + \sqrt2\,\mathbf y$ and $\bar{\mathbf z} = \mathbf x - \sqrt2\,\mathbf y$:

$$\bar{\mathbf z}\otimes\mathbf z\otimes\bar{\mathbf z} + \mathbf z\otimes\bar{\mathbf z}\otimes\mathbf z = \mathcal A,\qquad\text{so } \operatorname{rank}_{\mathbb R}(\mathcal A)\le 2.$$

2. A tensor of rank at most 2 over a field is a sum of two outer products, and for $\mathcal A$ the identity (29) $\mathcal A = \mathbf u_1\otimes\mathbf u_2\otimes\mathbf u_3 + \mathbf v_1\otimes\mathbf v_2\otimes\mathbf v_3$ holds exactly when the coordinates of $\mathbf u_i, \mathbf v_i$ satisfy (30).
3. Every solution of (30) in a field of characteristic zero satisfies $2c_2^2 - d_2^2 = 0$ and $c_1d_2d_3 + 2 = 0$.
4. Lemma 8.1: (30) has no rational solution.
5. $\operatorname{rank}_{\mathbb Q}(\mathcal A) > 2$.

Significance

The theorem shows that tensor rank, unlike matrix rank, is not invariant under field extension even between $\mathbb Q$ and $\mathbb R$, and even for the smallest nontrivial format $2\times2\times2$. Its consequence for complexity is that a hardness result for rank over $\mathbb Q$ cannot be transferred to $\mathbb R$ by reading the same instance in a larger field; the paper accordingly re-examines Håstad's construction to obtain hardness over $\mathbb R$ and $\mathbb C$ (Theorem 8.2), which is outside this mission.

The result is proved in the paper, with the decisive algebraic step delegated to a computer-algebra computation (Appendix). A machine-checked proof replaces that computation by a certificate verified in Lean, and it settles a printed error: one of the two consequences of (30) in the proof of Lemma 8.1 is printed with the wrong sign (see Formalization scope). No formalization of array tensor rank over a field, or of its field dependence, is known to exist in Mathlib or on this platform.

Difficulty

The upper bound is an identity among explicit $2\times2\times2$ arrays. The lower bound is the substance: one must show that the cubic system (30), which has real solutions, has no rational one. Since (30) is solvable over $\mathbb R$, no argument by signs, inequalities or real geometry can work; the obstruction is arithmetic, coming from the irrationality of $\sqrt2$. The step that fails in a naive attempt is the elimination: eliminating ten of the twelve unknowns from eight cubic equations by hand is impractical. A second, smaller difficulty is the reduction from "$\operatorname{rank}_{\mathbb Q}(\mathcal A) \le 2$" to two terms of the special form (29), which requires absorbing the scalars and padding a decomposition with fewer than two terms.

Formalization scope

• Tensors are functions Fin l → Fin m → Fin n → E, with 0-based indices: the paper's $a_{ijk}$ is A (i-1) (j-1) (k-1). Vectors are Fin n → E.
• rankOver E A is the sInf over $\mathbb N$ of the lengths $r$ of decompositions $\sum_s \lambda_s\, \mathbf x_s\otimes\mathbf y_s\otimes\mathbf z_s$. The set is nonempty (one term per entry), so this is the paper's minimum. Zero summands are allowed; this gives the same minimum as the paper's sum of nonzero rank-1 tensors.
• $\operatorname{rank}_{\mathbb R}$ of a rational tensor is rankOver ℝ of its entrywise cast to $\mathbb R$; $\operatorname{rank}_{\mathbb Q}$ is rankOver ℚ, whose witnesses are rational. A formalization in which both ranks range over real witnesses would make the theorem false.
• The goal is the printed existential. It is not a loophole: the milestones concern the paper's explicit tensor.
• Readings of loose phrases: "Suppose not and that there exist $\mathbf u_i, \mathbf v_i$ with (29). Identity (29) gives eight equations found in (30)" is split into a general statement (rank at most 2 over any field means a sum of two outer products) and the equivalence of (29) with (30) over every field of characteristic zero (milestone 2); both are stated in a generality in which their hypotheses can hold, because for $\mathcal A$ over $\mathbb Q$ they cannot. "Polynomial consequences of (30)" is read as "holds at every solution of (30) in every field of characteristic zero" (milestone 3); over $\mathbb Q$ alone the statement would be vacuous, since (30) has no rational solution.
• Corrected error. The paper prints the second consequence as $c_1d_2d_3 - 2 = 0$. It is false: the real solution from milestone 1 has $c_1d_2d_3 = -2$. The milestone states $c_1d_2d_3 + 2 = 0$ (checked by a Gröbner basis computation over $\mathbb Q$), which serves the paper's argument equally. The Appendix certificates $G_k$, $H_k$ (p. 0:34) are not used in any statement.
• Out of scope: Theorem 1.15/8.2 (Håstad's construction over $\mathbb R$ and $\mathbb C$) and the conjectures of §13.

Needed infrastructure: finite sums of arrays, Real.sqrt and irrational_sqrt_two, and an ideal-membership certificate for milestone 3. The array rank rankOver is reusable for any statement about tensor rank over a field. The platform's mme_tensor_rank (restriction-based rank of a TensorObj over a single field, from the matrix-multiplication exponent series) is a different object and is not reused. Proofs of any milestone, and alternative certificates for Lemma 8.1, are welcome.

Selected references

• C. J. Hillar and L.-H. Lim, Most tensor problems are NP-hard, J. ACM 60(6), Art. 45, 2013. https://doi.org/10.1145/2512329 (arXiv: https://arxiv.org/abs/0911.1393)
• J. Håstad, Tensor rank is NP-complete, J. Algorithms 11(4), 644–654, 1990. https://doi.org/10.1016/0196-6774(90)90014-6
• V. de Silva and L.-H. Lim, Tensor rank and the ill-posedness of the best low-rank approximation problem, SIAM J. Matrix Anal. Appl. 30(3), 1084–1127, 2008. https://doi.org/10.1137/06066518X
• F. L. Hitchcock, The expression of a tensor or a polyadic as a sum of products, J. Math. Phys. 6, 164–189, 1927. https://doi.org/10.1002/sapm192761164

Motivation

A snark is an uncolourable, cyclically 4-edge-connected cubic graph of girth at least 5: a cubic graph whose edges cannot be properly coloured with three colours, and which is not reducible to a smaller such graph by an elementary operation. Snarks are the critical cases for several of the central conjectures of graph theory, among them the cycle double cover conjecture, Tutte's 5-flow conjecture and the Berge–Fulkerson conjecture: a minimal counterexample to any of them, if one exists, is a snark. Lists of all small snarks are therefore used to test such conjectures by computer.

Brinkmann, Goedgebeur, Hägglund and Markström (arXiv:1206.6690v3, 2013) generated all snarks on up to 36 vertices. Testing 3-edge-colourability is NP-complete, and only a vanishing fraction of cubic graphs are snarks (0.00044% of the cubic graphs of girth at least 5 on 28 vertices, p. 4), so the generation algorithm needs cheap criteria that recognise, before a graph is built, that it will be colourable and can be skipped. Section 3.1 of the paper supplies such a criterion for the last construction step, and this mission formalizes it.

Setting

All graphs are finite and simple. A graph is cubic if every vertex has degree 3. A 3-colouring of a graph $G=(V,E)$ is a map $C:E\to\{0,1,2\}$ that gives different colours to any two distinct edges sharing an end-vertex; $G$ is colourable if it has one, i.e. its chromatic index satisfies $\chi'(G)\le 3$ (p. 2, Isaacs' terminology).

A 2-factor of $G$ is a spanning 2-regular subgraph $F$ (p. 4); each connected component of $F$ is a cycle. $F$ is an even 2-factor if all its cycles have even length (p. 5). For a 3-colouring $C$ and colours $i\ne j$, write $G_{ij}$ for the spanning subgraph whose edges are those coloured $i$ or $j$.

The edge insertion operation (Figure 1(d), p. 5) takes two distinct edges $e=ab$ and $e'=cd$ of $G$, which may share an end-vertex, subdivides $e$ by a new vertex $x$ and $e'$ by a new vertex $y$, and adds the edge $xy$. The resulting graph $G'$ has vertex set $V\cup\{x,y\}$ and edge set

$$E(G')=\bigl(E\setminus\{e,e'\}\bigr)\cup\{ax,xb,cy,yd,xy\}.$$

If $G$ is cubic, so is $G'$. In the generation algorithm every graph of girth at least 4 is produced from a graph with two fewer vertices by this operation.

Formalization targets

Goal: Theorem 3.3 (p. 5)

Let $G$ be a cubic graph with a 3-colouring $C$, let $i\ne j$ be colours, and let $e=ab$, $e'=cd$ be distinct edges of $G_{ij}$ lying on the same cycle of $G_{ij}$. Then

$$\chi'(G')\le 3,\qquad G' = G \text{ with an edge inserted between } e \text{ and } e'.$$

Milestones

1. Lemma 3.1 (p. 5). For a cubic graph $G$,

$$\chi'(G)\le 3 \iff G \text{ has an even 2-factor.}$$

2. The two-colour observation (§3.1, p. 5). If $G$ is cubic, $C$ is a 3-colouring and $i\ne j$, then $G_{ij}$ is an even 2-factor of $G$.
3. Lemma 3.2 (p. 5). If $F$ is an even 2-factor of a cubic graph $G$ and $e\ne e'$ are edges of $F$ on the same cycle of $F$, then the graph obtained by inserting an edge between $e$ and $e'$ is colourable.

Supporting statement (not on the goal's path)

Theorem 3.4 (p. 6, stated as folklore without proof). If $G$ is a colourable cubic graph and the inserted edge $xy$ lies on a 4-cycle of $G'$, then $G'$ is colourable.

Significance

The result. Theorem 3.3 is the look-ahead of the snark generator: one 3-colouring of a graph on $n-2$ vertices excludes, at once, every pair of edges lying on a common cycle of one of its three bicoloured 2-factors. For 28 vertices the first colouring alone discards on average 85% of the candidate edge pairs (p. 6), and the overall ratio of weak snarks among generated graphs on the last level improves by a factor of 85 (p. 4). The enumeration of all snarks up to 36 vertices, on which the paper's counterexamples and statistics rest, depends on this pruning being sound: a wrong pruning rule would silently delete snarks from the lists. Theorem 3.4 is a second pruning rule of the same kind.

Formalizing it. The results are proved (Lemma 3.1 is classical; the paper gives the argument for Lemma 3.2 in one sentence and for Theorem 3.3 by combination). None of them, and no statement about 3-edge-colourings of cubic graphs and their 2-factors, is formalized on the platform. The mission produces a machine-checked soundness proof of the pruning criterion and, along the way, a reusable development of the equivalence between 3-edge-colourings and even 2-factors in Lean's SimpleGraph library. Theorem 3.4 has no proof in the paper.

Difficulty

The combinatorial content is short; the difficulty lies in graph-theoretic infrastructure that Mathlib does not have. Lemma 3.1 relates a global object (a proper colouring of all edges) to the cycle structure of a spanning 2-regular subgraph, and either direction needs the description of a finite 2-regular graph as a disjoint union of cycles together with parity information along each cycle. Mathlib has walks, cycles and connected components, but no decomposition of a 2-regular graph into cycles and no notion of the length of a component as a cycle.

Lemma 3.2 and Theorem 3.3 change the vertex type: $G'$ lives on $V\sqcup\{x,y\}$, so 2-factors, connected components and cycle lengths must be transported from $G$ to $G'$, and the case where $e$ and $e'$ share an end-vertex (allowed by Figure 1(d)) has to be handled alongside the generic one. A first idea, to extend a given 3-colouring of $G$ directly to $G'$, does not work in general: the colours forced on the edges at $x$ and $y$ by the old colours of $e$ and $e'$ can conflict, and the hypothesis "same cycle" is what has to be used to avoid the conflict.

Formalization scope

Vertices form a type V with [Fintype V] [DecidableEq V]; graphs are SimpleGraph V with decidable adjacency, and "cubic" is Mathlib's G.IsRegularOfDegree 3. Colourability is G.lineGraph.Colorable 3 (an edge colouring, not a vertex colouring), and a 3-colouring is G.lineGraph.Coloring (Fin 3). A 2-factor is a graph F on the same vertex type with F ≤ G and F.IsRegularOfDegree 2; it is even if every connected component has an even number of vertices (Nat.card). The edge insertion operation produces a graph on V ⊕ Fin 2, with Sum.inr 0 subdividing $e$ and Sum.inr 1 subdividing $e'$; edges are unordered pairs Sym2 V. "On the same cycle" is encoded as membership of both edges in the 2-factor plus reachability of their end-vertices inside the 2-factor. Oddness is not defined as a number; Lemma 3.1 is stated in its second form.

Dropping "on the same cycle" would make Theorem 3.3 and Lemma 3.2 false (inserting edges between different cycles of a bicoloured 2-factor is exactly how snarks are produced), and both statements require the two edges to be distinct; a formalization without either hypothesis is ruled out. Every statement assumes cubicity, without which Lemma 3.1 fails.

Out of scope: the algorithmic content of §3 (isomorphism rejection, the look-ahead implementation, recolouring along non-hamiltonian cycles, the 85% / 11% / 3.4% statistics), the generation counts, and every exhaustive-search claim of the paper. The remaining results of the paper are covered by three sibling missions of this series.

Reusable beyond this mission: the 2-factor and even-2-factor definitions, the two-colour 2-factor of an edge colouring, and Lemma 3.1 itself. Contributions welcome: the cycle decomposition of finite 2-regular graphs, alternating colourings of even cycles, and a proof of Theorem 3.4.

Selected references

• G. Brinkmann, J. Goedgebeur, J. Hägglund, K. Markström, Generation and properties of snarks, J. Combin. Theory Ser. B 103 (2013); arXiv:1206.6690v3. https://arxiv.org/abs/1206.6690
• R. Isaacs, Infinite families of nontrivial trivalent graphs which are not Tait colorable, Amer. Math. Monthly 82 (1975) 221–239. https://doi.org/10.2307/2319844

Motivation

Quasi-Newton methods replace the Hessian of an objective by a matrix $H \succ 0$ that is updated from observed pairs of steps and gradient changes. The secant equation $HS = Y$ asks the new matrix to map the observed steps $S$ to the observed changes $Y$. The best-known update is BFGS, which for $p$ simultaneous pairs $S, Y \in \mathbb{R}^{n\times p}$ reads

$$H_{\mathrm{BFGS}} := Y(Y^TS)^{-1}Y^T + H - HS(S^THS)^{-1}S^TH .$$

Schnabel (Quasi-Newton methods using multiple secant equations, technical report, University of Colorado at Boulder, 1983, reference [25] of the paper) studied such multiple-secant updates; one of his results is that a positive definite $H$ with $HS = Y$ exists exactly when $Y^TS \succ 0$.

Dahl and Andersen (Math. Program. 194:341–370, 2022) use multiple-secant BFGS updates to build primal-dual scaling matrices for an interior-point algorithm on the nonsymmetric exponential cone, following Tunçel (Found. Comput. Math. 1:229–254, 2001) and Myklebust and Tunçel (arXiv:1411.2129). In their setting $p = 2$, and they need the update in factored, low-rank form. Their Theorem 2 supplies it: the term $Y(Y^TS)^{-1}Y^T$, and its counterpart $S(Y^TS)^{-1}S^T$ for the inverse update, are computed by $p$ rank-one steps. These steps resemble single-secant quasi-Newton updates, and no inverse is formed. This mission formalizes Theorem 2 and the steps of its proof.

Setting

Let $n, p \ge 0$ and $Y_0, S_0 \in \mathbb{R}^{n\times p}$. Write $e_k$ for the $k$-th unit vector of $\mathbb{R}^p$ and $\langle a, b\rangle = a^Tb$ for the inner product of $\mathbb{R}^n$, so that $\langle Ye_k, Se_k\rangle = (Y^TS)_{kk}$. The hypothesis of the theorem is

$$Y_0^TS_0 \succ 0,$$

meaning that the $p\times p$ matrix $Y_0^TS_0$ is symmetric and positive definite.

For $k = 1, \dots, p$ the recursions (25)–(26) are

$$v_k := \frac{Y_{k-1}e_k}{\langle Y_{k-1}e_k, S_{k-1}e_k\rangle^{1/2}}, \qquad Y_k := Y_{k-1} - v_kv_k^TS_{k-1},$$ $$u_k := \frac{S_{k-1}e_k}{\langle Y_{k-1}e_k, S_{k-1}e_k\rangle^{1/2}}, \qquad S_k := S_{k-1} - u_ku_k^TY_{k-1}.$$

Both updates of step $k$ use the previous pair $(Y_{k-1}, S_{k-1})$. Collect the vectors into $V := (v_1 \cdots v_p)$ and $U := (u_1 \cdots u_p) \in \mathbb{R}^{n\times p}$.

The proof uses two more objects. The first is the $p\times p$ matrix

$$L := \left(\frac{Y_0^TS_0e_1}{\langle Y_0e_1, S_0e_1\rangle^{1/2}}, \cdots, \frac{Y_{p-1}^TS_{p-1}e_p}{\langle Y_{p-1}e_p, S_{p-1}e_p\rangle^{1/2}}\right).$$

The second is $\Psi_k$, the principal submatrix formed by the last $p-k$ rows and columns of $Y_k^TS_k$. In Lean these are ExpConeIPM.Secant.Ys, Ss, d, V, U, L and Ψ, all in one definition item.

Formalization targets

Goal: Theorem 2 (pp. 357–358)

$$Y_0(Y_0^TS_0)^{-1}Y_0^T = VV^T, \qquad S_0(Y_0^TS_0)^{-1}S_0^T = UU^T .$$

Milestones (the steps of the proof, pp. 358–359)

1. (27). For $k = 1, \dots, p$,

$$Y_k^TS_k = Y_{k-1}^TS_{k-1} - \frac{(Y_{k-1}^TS_{k-1}e_k)(Y_{k-1}^TS_{k-1}e_k)^T}{\langle Y_{k-1}e_k, S_{k-1}e_k\rangle}.$$

2. Well-definedness. For $k = 0, \dots, p-1$, $\Psi_k \succ 0$, and in particular $\langle Y_ke_{k+1}, S_ke_{k+1}\rangle > 0$.
3. Sparsity. $Y_je_k = S_je_k = 0$ for $1 \le k \le j \le p$.
4. Cholesky factorization (28). $LL^T = Y_0^TS_0$.
5. The $V$-identity. $LV^T = Y_0^T$.

The first identity of the goal follows from milestones 4 and 5. The paper says the second "follows similarly". The analogous identity $LU^T = S_0^T$ is not displayed in the paper, so it is not a milestone.

Significance

The result. Theorem 2 expresses the multiple-secant part of the BFGS update (23), and of its inverse, as a sum of $p$ rank-one terms $v_kv_k^T$ and $u_ku_k^T$. Each term comes from a recursion that touches one column at a time. On pp. 359–360 Dahl and Andersen apply it twice with $p = 2$. This gives the BFGS scaling of their exponential-cone algorithm as an explicit rank-3 update of $\mu F''(x)$, which is how the algorithm implemented in MOSEK computes its scaling matrices (§6, p. 361 of the paper). The argument is a Cholesky factorization of $Y_0^TS_0$ carried out implicitly on the factors $Y_0$ and $S_0$.

Formalizing it. The theorem is proved in the paper, in under a page. Its proof leaves two steps implicit. The first is that the symmetry of every $Y_k^TS_k$, which (27) and the step to $LV^T = Y_0^T$ use, propagates from $Y_0^TS_0$. The second is the second identity, which the paper does not prove. A machine-checked proof records both. To our knowledge no proof assistant has a formal treatment of multiple-secant updates. The recursion also gives a reusable statement: a column-by-column Schur-complement process on a product $Y^TS$ produces its Cholesky factor.

Difficulty

The obvious route expands $VV^T$ directly and compares it with $Y_0(Y_0^TS_0)^{-1}Y_0^T$. This leads nowhere, because $v_k$ depends on all earlier steps through $Y_{k-1}$ and $S_{k-1}$. The step that carries the proof is an invariant over the recursion. The trailing blocks $\Psi_k$ of $Y_k^TS_k$ must stay symmetric positive definite, and the leading columns of $Y_k$ and $S_k$ must stay zero. Both must be maintained together through a pair of coupled updates, in which $S_k$ is updated with the old $Y_{k-1}$. A second difficulty is bookkeeping: the paper's 1-based columns, the step count $k$, and the trailing block of size $p-k$ shift relative to each other.

The hypothesis needs care. If $Y_0^TS_0$ is only assumed to satisfy $x^TY_0^TS_0x > 0$ for $x \ne 0$, without symmetry, the identities are false in general. A $5\times 3$ instance whose symmetric part is positive definite, with a small antisymmetric part, violates the first identity by $0.44$ in the largest entry.

Formalization scope

Everything is real matrix algebra over Matrix (Fin n) (Fin p) ℝ, with arbitrary $n, p$ (including $p = 0$, where both sides are zero). The formalization commits to the following conventions.

• $Y_0^TS_0 \succ 0$ is Matrix.PosDef, which includes symmetry. The inverse is Matrix.inv. It is a genuine inverse under this hypothesis.
• Columns are 0-based. Column j : Fin p is the paper's $e_{j+1}$. Ys Y₀ S₀ k and Ss Y₀ S₀ k are $Y_k$ and $S_k$ after $k$ steps, and they are left unchanged after step $p$. d Y₀ S₀ j is $\langle Y_je_{j+1}, S_je_{j+1}\rangle$.
• The square root is Real.sqrt. The division by it is multiplication by an inverse. Both return junk values on non-positive arguments, which never occur under the hypothesis; milestone 2 states this.
• $V$, $U$ and $L$ are computed from the recursion (25)–(26). They are never chosen as some factorization satisfying the conclusion. The trivializing formalization, which defines $V$ as any factor of $Y_0(Y_0^TS_0)^{-1}Y_0^T$, is ruled out by construction.
• Each milestone carries the theorem's hypothesis $Y_0^TS_0 \succ 0$. No hypothesis on the intermediate $Y_k^TS_k$ is assumed, since its symmetry is part of what must be proved.

No repair of the printed statements was needed. On p. 359 two misprints are not copied: $\langle Y_{p-1}^Te_p, S_{p-1}e_p\rangle$ for $\langle Y_{p-1}e_p, S_{p-1}e_p\rangle$, and $S_i^TY_i$ for $Y_i^TS_i$. The definition of $L$ uses $Y_i^TS_i$.

A complete development needs rank-one updates of products, Schur complements of a positive definite matrix in its leading entry, and inverses of $LL^T$ for an invertible $L$. Schnabel's existence theorem (Theorem 1 of the paper) and the applications on pp. 359–360 are outside the mission. A general lemma on Schur-complement recursions producing Cholesky factors would be reusable on its own. Contributions on the U-side identity $LU^T = S_0^T$ are welcome.

Selected references

• J. Dahl, E. D. Andersen, A primal-dual interior-point algorithm for nonsymmetric exponential-cone optimization, Math. Program. 194:341–370, 2022. https://doi.org/10.1007/s10107-021-01631-4
• R. B. Schnabel, Quasi-Newton methods using multiple secant equations, Technical Report, University of Colorado at Boulder, 1983 (no stable online link known; cited as [25] in Dahl–Andersen).
• L. Tunçel, Generalization of primal-dual interior-point methods to convex optimization problems in conic form, Found. Comput. Math. 1:229–254, 2001. https://doi.org/10.1007/s102080010008
• T. Myklebust, L. Tunçel, Interior-point algorithms for convex optimization based on primal-dual metrics, arXiv:1411.2129, 2014. https://arxiv.org/abs/1411.2129

Motivation

Nonnegative matrix factorization (NMF) approximates a data matrix $A\in\mathbb R^{m\times n}$ by a product $XY$ of two nonnegative factors. Adding a cap on the number of nonzero entries of each factor gives sparse NMF, used in signal separation, text mining and image analysis because sparse nonnegative factors are easier to interpret. Bolte, Sabach and Teboulle (Math. Program. 146 (2014)) introduced the algorithm PALM (proximal alternating linearized minimization) for problems of the form $f(x)+g(y)+H(x,y)$ with nonconvex, nonsmooth $f$ and $g$, and proved that its bounded runs converge to critical points when the objective has the Kurdyka–Łojasiewicz property. Sparse NMF is the paper's main application (§4).

PALM is only implementable when the proximal map of each nonsmooth term can be computed. For sparse NMF the nonsmooth term is the indicator of the nonconvex set of nonnegative matrices with at most $s$ nonzero entries. Proposition 4.1 of the paper computes that proximal map in closed form. This mission formalizes Proposition 4.1 and the steps of its proof. The convergence theory of PALM is a separate mission of the same series.

Setting

Matrices are real $m\times n$ arrays $X=(X_{ij})$. The squared Frobenius norm is $\|X\|_F^2=\sum_{i,j}X_{ij}^2=\langle X,X\rangle$. The sparsity count $\|X\|_0$ is the number of nonzero entries of $X$, and $X\ge0$ means $X_{ij}\ge0$ for every $(i,j)$.

For a set $C$, the indicator $\delta_C$ is $0$ on $C$ and $+\infty$ off $C$. For a natural number $s$, set

$$f:=\delta_{X\ge0}+\delta_{\|X\|_0\le s},$$

the function that is $0$ on nonnegative matrices with at most $s$ nonzero entries and $+\infty$ elsewhere.

For $\sigma:\mathbb R^{m\times n}\to(-\infty,+\infty]$ and $t>0$, the proximal map (2.2) of the paper is the set

$$\operatorname{prox}^\sigma_t(U)=\operatorname{argmin}\Big\{\sigma(X)+\frac t2\|X-U\|_F^2\Big\}.$$

Throughout, $\operatorname{argmin}\{\varphi(X):X\in C\}$ is the set of all points of $C$ where $\varphi$ attains its smallest value on $C$.

The hard-thresholding operator of Definition 4.1 is

$$T_s(U)=\operatorname{argmin}_V\big\{\|U-V\|_F^2:\|V\|_0\le s\big\},$$

which is multi-valued when the $s$ largest entries of $U$ in absolute value are not uniquely determined. The projection onto the nonnegative orthant is $P_+(U)=\max\{0,U\}$, componentwise.

In the proof, $U$ is fixed and $\mathcal I^+=\{(i,j):U_{ij}\ge0\}$, $\mathcal I^-=\{(i,j):U_{ij}<0\}$, with partial squared norms $\|X\|_\pm^2=\sum_{(i,j)\in\mathcal I^\pm}X_{ij}^2$.

Formalization targets

Goal: Proposition 4.1 (Proximal map formula), p. 28

For every $U\in\mathbb R^{m\times n}$ and every $s\in\mathbb N$,

$$\operatorname{prox}^f_1(U)=\operatorname{argmin}\Big\{\tfrac12\|X-U\|_F^2 : X\ge0,\ \|X\|_0\le s\Big\}=T_s\big(P_+(U)\big).$$

Both equalities are equalities of sets, and both are part of the goal.

Milestones (in the order the proof uses them)

1. Relations (i)–(iii) in the proof (pp. 28–29): $\|X\|_F^2=\|X\|_+^2+\|X\|_-^2$; $\|X-U\|_+^2+\|X\|_-^2=\|X-P_+(U)\|_F^2$; and $\|X\|_-^2=0$ iff $X$ vanishes on $\mathcal I^-$.
2. The equality of the minimizer sets (4.1) and (4.2) (p. 29):

$$\operatorname{argmin}\Big\{\|X-U\|_+^2+\|X\|_-^2-2\!\!\sum_{(i,j)\in\mathcal I^-}\!\!X_{ij}U_{ij}:X\ge0,\|X\|_0\le s\Big\}=\operatorname{argmin}\big\{\|X-U\|_+^2:X|_{\mathcal I^-}=0,\ X\ge0,\ \|X\|_0\le s\big\}.$$

3. The constraint $X\ge0$ in (4.2) can be removed without changing its set of solutions (p. 29).

Significance

The result. Proposition 4.1 says that the proximal step for the nonnegative sparsity constraint is computed by clipping the negative entries of $U$ to zero and then hard-thresholding: keeping $s$ entries of largest magnitude and zeroing the rest. The paper remarks that this costs $O(mn)$ operations. It is what turns PALM into the explicit algorithm PALM-Sparse NMF, and the same formula applies to any method that needs a projection onto nonnegative sparse matrices (projected gradient methods, iterative hard thresholding with sign constraints).

Formalizing it. The result is proved in the paper; to our knowledge no machine-checked proof exists. The platform has a projection-onto-sparse-vectors statement without nonnegativity and stated as a single inclusion, which is a different theorem. The mission produces a set-level statement that handles ties, the degenerate cases $s=0$ and $s\ge mn$, and the interaction of the sign and the sparsity constraints, all of which the informal proof passes over quickly.

Difficulty

The obvious argument is: "project onto the nonnegative orthant, then onto the sparse matrices". Composing two projections onto nonconvex sets is not in general the projection onto their intersection, so this argument is not valid as it stands; the equality holds here because of the specific coordinate structure, and the proof must show it. The second obstacle is that everything is set-valued: when several entries of $P_+(U)$ tie for the $s$-th largest magnitude, $T_s(P_+(U))$ has several elements, and the equality must account for every one of them, in both directions. The step "(4.1) = (4.2)" and the removal of $X\ge0$ are dismissed in the paper as "a simple contradiction argument" and "arguing in a similar way"; each needs an explicit modification of a feasible point that preserves sparsity and does not increase the objective.

Formalization scope

Matrices are Matrix (Fin m) (Fin n) ℝ, with 0-based indices (harmless relabelling of $\{1,\dots,m\}\times\{1,\dots,n\}$). $\|M\|_F^2$ is the Frobenius inner product $\langle M,M\rangle$ of the published definition CaiCandesShen.ProximalLimit.Basic. The indicators and $f$ take values in EReal, with $+\infty=\top$; membership in $\operatorname{prox}^f_1(U)$ is the inequality $f(X)+\frac12\|X-U\|_F^2\le f(W)+\frac12\|W-U\|_F^2$ in EReal for every $W$. The proximal map carries the weight $t/2$ of (2.2), not $1/(2t)$. $P_+$ is defined by the componentwise formula. No restriction is placed on $s$.

Every operator in the statement is a set of minimizers. A formalization that selects one element (for instance "keep the $s$ largest entries with a fixed tie-break") proves only one inclusion of a weaker statement and does not count.

The development needs only finite sums and the argmin-set definition shared by all items; no further library is required. Lemmas about hard thresholding on matrices (the description of $T_s(U)$ by $s$ largest entries, nonnegativity of $T_s$ of a nonnegative matrix) are reusable well beyond this mission, and contributions of such lemmas are welcome.

Theorem numbers and page numbers refer to the author version of the paper (36 pages, printed page = PDF page), not to the Springer typesetting.

Selected references

• J. Bolte, S. Sabach, M. Teboulle, Proximal alternating linearized minimization for nonconvex and nonsmooth problems, Mathematical Programming 146 (2014), 459–494. https://doi.org/10.1007/s10107-013-0701-9
• D. D. Lee, H. S. Seung, Learning the parts of objects by non-negative matrix factorization, Nature 401 (1999), 788–791. https://doi.org/10.1038/44565
• J.-F. Cai, E. J. Candès, Z. Shen, A singular value thresholding algorithm for matrix completion, SIAM J. Optim. 20 (2010), 1956–1982. https://doi.org/10.1137/080738970 (source of the Frobenius inner product definition reused here)

Motivation

Differential privacy (Dwork, McSherry, Nissim, Smith 2006) asks that a randomized algorithm run on a database behave almost identically whether or not any single record is changed. A central question for data curators is non-interactive release: publish, once, a sanitized object (ideally a synthetic database) from which analysts can answer many statistical queries accurately. Blum, Ligett and Roth (arXiv:1109.2229, JACM 2013) showed that over a discrete data universe this is possible for every class of counting queries of bounded VC-dimension, with accuracy governed by the VC-dimension and the logarithm of the universe size.

That dependence on the universe size raises an obvious question: can the discretization be removed? For real-valued data the class of interval queries ("what fraction of the records lies in $[a,b]$?") has VC-dimension 2, so a learning-theoretic intuition suggests that releasing a database accurate for all intervals should be easy. Section 5 of the paper shows that it is impossible under differential privacy. This mission formalizes that impossibility.

The phenomenon was later quantified: Bun, Nissim, Stemmer and Vadhan (FOCS 2015) showed that for approximate differential privacy, releasing threshold queries over a finite ordered domain of size $N$ requires sample size growing with $\log^* N$, so that the infinite case is impossible for approximate privacy as well. The present result is the pure-privacy statement for the real line.

Setting

A real-valued database of size $n \ge 1$ is a tuple $z = (z_1,\dots,z_n) \in \mathbb R^n$. Two databases are neighbours if they differ in exactly one coordinate. A mechanism maps each database $z$ to a probability distribution $A(z)$ on a measurable output space $O$. It is $\varepsilon$-differentially private if for all neighbours $z, z'$ and all measurable $S \subseteq O$,

$$\Pr[A(z) \in S] \le e^{\varepsilon}\,\Pr[A(z') \in S].$$

For real $a \le b$ the interval query is $Q_{[a,b]}(z) = \#\{i : a \le z_i \le b\}/n$. A mechanism with a readout $\mathrm{ans}(o,a,b)$ (the answer that output $o$ gives to $Q_{[a,b]}$; for synthetic data $\hat D$, $\mathrm{ans}(\hat D,a,b) = Q_{[a,b]}(\hat D)$) is $(\alpha,\delta)$-useful for interval queries if for every database $z$,

$$\Pr_{o\sim A(z)}\big[\forall a \le b:\ |\mathrm{ans}(o,a,b) - Q_{[a,b]}(z)| \le \alpha\big] \ge 1-\delta .$$

A real number $r$ is a $\theta$-percentile point of $z$ (the paper's "$50-\delta, 50+\delta$ percentile" with $\theta = \delta/100$) if at least $(1/2-\theta)n$ entries satisfy $z_i \le r$ and at least $(1/2-\theta)n$ entries satisfy $z_i \ge r$. A mechanism with real outputs answers median queries usefully with positive probability if on every database its output is a $\theta$-percentile point with positive probability.

In Lean, databases are Fin n → ℝ; neighbours and differential privacy are the published PrivLearn.Generic.Neighbors and PrivLearn.Generic.IsDP; the new objects are intervalQuery, IsPercentile, AnswersMedianUsefully and UsefulIntervals in PrivateRelease.Continuous.

Formalization targets

Goal: Corollary 5.2 (p. 15)

For every $n \ge 1$, $\varepsilon \ge 0$ and $\alpha, \delta < 1/2$, no $\varepsilon$-differentially private mechanism with a measurable readout is $(\alpha,\delta)$-useful for interval queries on $\mathbb R^n$:

$$\mathrm{IsDP}(A,\varepsilon) \;\Longrightarrow\; \neg\,\mathrm{UsefulIntervals}(A,\mathrm{ans},\alpha,\delta).$$

No constant is hard-coded; the thresholds $1/2$ are the paper's.

Milestone: Theorem 5.1 (p. 14)

For every $n \ge 1$, $0 \le \theta < 1/2$ and real $\varepsilon$, no $\varepsilon$-differentially private mechanism $A : \mathbb R^n \to \mathcal P(\mathbb R)$ answers median queries usefully with positive probability on every database:

$$\mathrm{IsDP}(A,\varepsilon) \;\Longrightarrow\; \exists z,\ \Pr_{r\sim A(z)}[r \text{ is a } \theta\text{-percentile point of } z] = 0 .$$

Significance

The result. Corollary 5.2 is the reason the paper's general release mechanism needs a discretized data universe and why its halfspace mechanism (§6) relaxes usefulness to large-margin queries. More broadly it separates private release from non-private learning: the class of intervals is learnable from $O(1/\alpha^2)$ samples without privacy, yet no pure-private mechanism can release it at all over $\mathbb R$. It anticipates the line of work on private learning of thresholds and the role of the domain size in private query release.

Formalizing it. Both statements are proved in the paper; neither is, to our knowledge, machine-checked. A formal proof needs the countability of the atoms of a finite measure on $\mathbb R$, the stability of differential privacy under measurable post-processing, and a measurable selection of a percentile point from approximate interval answers. These pieces (especially post-processing for general measurable outputs) are reusable across formalized differential privacy.

Difficulty

The obvious argument for Theorem 5.1, a direct comparison of two neighbouring databases, gives nothing: changing one record moves the percentile set only slightly, and differential privacy allows each probability to change by a factor $e^{\varepsilon}$, so no single pair of neighbours yields a contradiction. A naive appeal to "the median reveals a record" also fails, since the statement must exclude even mechanisms that are correct with tiny positive probability.

For Corollary 5.2 the difficulty is measure-theoretic: the usefulness event intersects uncountably many conditions, the release must be converted into a single real output measurably, and the converted output must be a percentile point on the useful event for every real database, not only those in $[0,1]$.

Formalization scope

Conventions committed to in Lean:

• Databases are ordered tuples Fin n → ℝ with $n \ge 1$; the paper's neighbour relation "$|D\Delta D'| \le 1$" is read as replace-one-entry.
• Mechanisms are families of probability measures (IsProbabilityMeasure (A z) is a hypothesis). Theorem 5.1's outputs live in $\mathbb R$ with its Borel σ-algebra.
• Interval queries use closed intervals $[a,b]$ with $a \le b$, as in the paper's indicator $I_{a_1,a_2}$ (p. 12).
• Usefulness is required on every database in $\mathbb R^n$ (Definition 2.10 with $X = \mathbb R$). The usefulness event need not be measurable; its probability is the outer measure.
• The goal is stated for an arbitrary measurable output space with a readout $\mathrm{ans}$ measurable in the output for each fixed query. Synthetic data is a special case, so the formal goal is at least as strong as the paper's. The readout's measurability is necessary for the statement to be true with outer measures.
• The percentile set counts entries equal to $r$ on both sides. A one-sided reading ($\#\{z_i \le r\}/n \in [1/2-\theta, 1/2+\theta]$) makes the set empty for constant databases, so that Theorem 5.1 would hold vacuously; the chosen definition always contains a sample median and equals $\{c\}$ on a constant database $(c,\dots,c)$ (both facts were checked locally in Lean).
• Trivializing readings are ruled out: the percentile set is never empty, the mechanism is a probability measure (the zero measure is differentially private), and $n = 0$ (no neighbours, $Q = 0/0 = 0$ in Lean) is excluded.
• There is no O(·)/Ω(·) in this section, so no constant was instantiated.
• Not formalized: the clause of Corollary 5.2 "nor for any class $C$ that generalizes interval queries to higher dimensions (for example, halfspaces, axis-aligned rectangles, or spheres)", because the paper does not define "generalizes".

Contributions welcome: a proof of Theorem 5.1; a general post-processing lemma for IsDP; the reduction from interval usefulness to median answers.

Selected references

• A. Blum, K. Ligett, A. Roth, A Learning Theory Approach to Non-Interactive Database Privacy, arXiv:1109.2229v1, 2011; J. ACM 60(2), 2013. https://arxiv.org/abs/1109.2229, https://doi.org/10.1145/2450142.2450148
• C. Dwork, F. McSherry, K. Nissim, A. Smith, Calibrating Noise to Sensitivity in Private Data Analysis, TCC 2006. https://doi.org/10.1007/11681878_14
• M. Bun, K. Nissim, U. Stemmer, S. Vadhan, Differentially Private Release and Learning of Threshold Functions, FOCS 2015. https://arxiv.org/abs/1504.07553