The dual objective is at most the doubly-weighted sum

Read-back 3 — dual_le_weighted

Data and binders. Two implicitly quantified types $I$ and $J$ in arbitrary universes, each with a finiteness structure, and four explicit pieces of real-valued data:

• $A : I \to J \to \mathbb{R}$, a real matrix with rows indexed by $I$, columns by $J$, entries $A_{i,j}$;
• $b : J \to \mathbb{R}$, one real number $b_j$ per column index;
• $x : I \to \mathbb{R}$, one real number $x_i$ per row index;
• $y : J \to \mathbb{R}$, one real number $y_j$ per column index.

Hypotheses. Two, each universally quantified over the column index type $J$:

1. $\forall j \in J,\; 0 \le y_j$ — every component of $y$ is nonnegative.
2. $\forall j \in J,\; b_j \;\le\; \displaystyle\sum_{i \in I} A_{i,j}\, x_i$ — for each column index $j$, $b_j$ is at most the sum over all row indices $i$ of $A_{i,j} x_i$. Note the direction: $b_j$ is the smaller side.

Conclusion. Unfolding the bundle's definition $\texttt{dualObjective}(b,y) = \sum_{j \in J} b_j\, y_j$, the assertion is

Here the inner sum runs over $i$, the first index of $A$ (a column of $A$ contracted against $x$), and the outer sum runs over $j$, the second index of $A$; the column value is multiplied on the right by $y_j$. The inequality is non-strict and points in the direction: dual objective $\le$ weighted quantity.

Sign conditions present and absent. Nonnegativity is assumed only for $y$. There is no sign condition on $x$ — its components may be negative — nor on the entries of $A$, nor on $b$. Both stated hypotheses bear on data occurring in the conclusion ($y$ in hypothesis 1; $b$ and the column sums in hypothesis 2); neither is left unused in the sense of constraining data absent from the conclusion.

Degenerate cases. If $J$ is empty, both hypotheses are vacuously true and both sides are the empty sum $0$, giving $0 \le 0$. If $I$ is empty, each inner sum $\sum_i A_{i,j} x_i$ is $0$, hypothesis 2 degenerates to $b_j \le 0$ for every $j$, the right-hand side is $\sum_j 0 \cdot y_j = 0$, and the assertion becomes $\sum_j b_j y_j \le 0$. If both are empty, the statement reduces to $0 \le 0$. Nothing excludes $y = 0$, $x = 0$, $b = 0$, or $A = 0$.

Not asserted. The statement does not assert equality, nor strict inequality, nor nonnegativity of either side. It says nothing about $c$, about $\texttt{primalObjective}$, or about any comparison between the dual objective and a primal objective; no weak-duality chain is claimed. It assumes and asserts nothing about the sign of $x$, about $x$ being a feasible or optimal primal point, or about $y$ being feasible for constraints of the form $A^{\top} y \le c$ (no such hypothesis appears). It does not assert that the right-hand side may be rewritten with the summation order reversed, and it states no connection to the other two statements in this bundle. The declaration's body is a placeholder, so no proof is supplied by the code.