The doubly-weighted sum is at most the primal objective

Read-back 1 — weighted_le_primal

Data and binders. The statement quantifies over two types $I$ and $J$ (implicit arguments, living in arbitrary universes), each equipped with a finiteness structure (Fintype), i.e. each is a finite index set with a fixed enumeration. No further structure is assumed on $I$ or $J$: no order, no nonemptiness, no decidable equality beyond what finiteness supplies. It then quantifies over four explicit pieces of real-valued data:

• $A : I \to J \to \mathbb{R}$, a real matrix whose rows are indexed by $I$ and whose columns are indexed by $J$; write $A_{i,j}$ for its entry;
• $c : I \to \mathbb{R}$, one real number $c_i$ per row 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 hypotheses are assumed, both universally quantified over their whole index type:

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

Conclusion. Unfolding the bundle's definition $\texttt{primalObjective}(c,x) = \sum_{i \in I} c_i\, x_i$, the asserted conclusion is

On the left, the inner sum runs over $j$, the second index of $A$ (a row of $A$ paired against $y$), and the outer sum runs over $i$, the first index of $A$; the row-sum is multiplied on the right by $x_i$. The inequality is non-strict and points in the direction: weighted quantity $\le$ primal objective.

Sign conditions present and absent. Nonnegativity is assumed only for $x$. There is no sign condition anywhere on $y$, on the entries of $A$, or on $c$; $y_j$ and $A_{i,j}$ may be negative, and $c_i$ may be negative provided hypothesis 2 still holds. Both stated hypotheses appear in the conclusion's data ($x$ in hypothesis 1, and the row-sums and $c$ in hypothesis 2); neither is left dangling on data absent from the conclusion.

Degenerate cases. If $I$ is empty, both hypotheses are vacuously true and both sides of the conclusion are the empty sum $0$, so the claim is $0 \le 0$. If $J$ is empty, every inner sum $\sum_{j} A_{i,j} y_j$ is $0$, hypothesis 2 degenerates to $0 \le c_i$ for every $i$, the left-hand side of the conclusion is $\sum_{i} 0 \cdot x_i = 0$, and the assertion becomes $0 \le \sum_i c_i x_i$. If both are empty, the whole statement reduces to $0 \le 0$. Nothing rules out $x = 0$, $y = 0$, or $A = 0$.

Not asserted. The statement does not assert equality, nor a strict inequality. It does not assert that either side is nonnegative. It says nothing about any vector $b$, about any dual objective, about feasibility of $x$ for constraints of the form $Ax \ge b$ or $Ax \le b$ (no such hypothesis appears), or about optimality of $x$ or $y$. It does not assert the converse inequality, nor that the left-hand side may be rewritten with the summation order reversed, nor any relation to the other two statements in this bundle. It is a single inequality between two finite sums, and nothing more. The declaration's body is a placeholder, so no proof is supplied by the code.