Unique minimizer of the $\ell^1$ programs $(P_1)$ and $(P_1')$

IsUniqueL1Minimizer. This is a predicate (a proposition, not a theorem) with the following data: two natural numbers $p, m \ge 0$ (implicit; both may be $0$), a real matrix $F \in \mathbb{R}^{p \times m}$ with rows indexed by $\{0,\dots,p-1\}$ and columns by $\{0,\dots,m-1\}$, a vector $f \in \mathbb{R}^p$, and a vector $c \in \mathbb{R}^m$. Write $Fc$ for the ordinary matrix–vector product, $(Fc)_i = \sum_{j} F_{ij}\, c_j$, and write $\|x\|_1$ for the quantity l1Norm from the earlier file, which is the finite sum $\|x\|_1 = \sum_{j=0}^{m-1} |x_j|$ (equal to $0$ when $m = 0$). The predicate $\mathrm{IsUniqueL1Minimizer}(F, f, c)$ asserts the conjunction of two things:

That is, $c$ is a solution of the linear system $Fx = f$, and every other solution $d$ of that system has strictly larger $\ell^1$-norm than $c$ (strict inequality, so this expresses that $c$ is the unique $\ell^1$-minimizer among solutions, not merely a minimizer). The predicate is about the specific vector $c$ supplied; it does not assert that such a $c$ exists, and it places no rank, sparsity, or size hypotheses on $F$, $f$, or $c$ (in particular the SupportedOn notion from the earlier file is not used). Edge cases: if $m = 0$, then $\mathbb{R}^m$ is a single point, the universally quantified clause is vacuously true, and the predicate reduces to $Fc = f$, i.e. $f = 0 \in \mathbb{R}^p$; if $p = 0$, then $Fc = f$ holds automatically (both sides are the empty vector), so the predicate says exactly that $c$ is the unique minimizer of $\|\cdot\|_1$ over all of $\mathbb{R}^m$, which is the case precisely when $c = 0$.

IsUniqueResidualL1Minimizer. This is a predicate with the following data: two natural numbers $m, n \ge 0$ (implicit; both may be $0$), a real matrix $A \in \mathbb{R}^{m \times n}$ with rows indexed by $\{0,\dots,m-1\}$ and columns by $\{0,\dots,n-1\}$, a vector $y \in \mathbb{R}^m$, and a vector $f \in \mathbb{R}^n$. As above, $Ax$ is the ordinary matrix–vector product, $y - Ax$ is componentwise subtraction in $\mathbb{R}^m$, and $\|v\|_1 = \sum_{i=0}^{m-1} |v_i|$ is the l1Norm of the earlier file (equal to $0$ when $m = 0$). The predicate $\mathrm{IsUniqueResidualL1Minimizer}(A, y, f)$ asserts

i.e. every vector $g$ other than $f$ produces a residual $y - Ag$ of strictly larger $\ell^1$-norm than the residual $y - Af$. This says $f$ is the unique minimizer of $g \mapsto \|y - Ag\|_1$ over all of $\mathbb{R}^n$ (unconstrained; no support, sparsity, or noise condition is imposed, and l2Norm and SupportedOn from the earlier file are not used). There is no hypothesis on $A$; note that if $A$ has a nonzero vector $h$ in its kernel and $n \ge 1$, then $g = f + h \ne f$ gives $\|y - Ag\|_1 = \|y - Af\|_1$, so the predicate is false — it can only hold when $A$ is injective (or $n = 0$). Edge cases: if $n = 0$, then $\mathbb{R}^n$ is a single point, there is no $g \neq f$, and the predicate holds vacuously; if $m = 0$, then every residual is the empty vector with $\ell^1$-norm $0$, the required strict inequality $0 < 0$ fails, and the predicate holds if and only if $n = 0$.