Read-back — PrimalDualOnline.LP bundle (15 declarations)

Shared binders. Every declaration below lives in the namespace PrimalDualOnline.LP and is stated for two implicit type variables $I$ and $J$, each drawn from an arbitrary universe, together with two implicit instance hypotheses asserting that $I$ is a finite type and that $J$ is a finite type. Finiteness is the only structure assumed of $I$ and $J$: they are not assumed nonempty, not assumed decidably ordered, and not related to one another. Nothing in the bundle is a theorem; all fifteen declarations are definitions, twelve of them producing a proposition (a truth-valued predicate) and two producing a real number, so nothing here asserts that any of these propositions holds. Throughout, a matrix-like datum is a function $A$ taking a first index $i \in I$ and a second index $j \in J$ to a real number, written $A_{i,j}$ below; the orientation is uniform across the whole bundle — the symbol is always applied as (first index in $I$, second index in $J$), and no transpose is ever formed. Vectors indexed by $I$ are $x$ and $c$; vectors indexed by $J$ are $b$ and $y$. Sums are finite sums over the whole index type, justified by the finiteness instances, and are $0$ when the index type is empty.

1. PrimalFeasible

PrimalFeasible is a predicate with two implicit arguments (the finite types $I$, $J$, with their two implicit finiteness instances) and three explicit arguments: a two-index real array $A$ with first index in $I$ and second index in $J$, a real vector $b$ indexed by $J$, and a real vector $x$ indexed by $I$. It asserts the conjunction of two families of conditions:

$$\forall j \in J,\quad b_j \;\le\; \sum_{i \in I} A_{i,j}\, x_i, \qquad\text{and}\qquad \forall i \in I,\quad 0 \le x_i .$$

The index convention is explicit here: for each fixed second index $j$, the sum runs over the first index $i$, i.e. over the $I$-indexed family $i \mapsto A_{i,j}$ paired with $x_i$. Both inequalities are non-strict, and the constraint direction is "$\ge$" in the sense that the $b$-side is the lower bound. There is no assumption that $A$, $b$, or $x$ have any sign beyond the stated $x_i \ge 0$. Degenerate cases: if $I$ is empty, every sum is $0$, the nonnegativity clause is vacuously true, and the predicate reduces to "$b_j \le 0$ for all $j$"; if $J$ is empty, the first clause is vacuously true and the predicate reduces to "$x_i \ge 0$ for all $i$"; if both are empty the predicate is unconditionally true (and is then satisfied by the unique empty vector).

2. DualFeasible

DualFeasible is a predicate with implicit arguments $I$, $J$ and their two implicit finiteness instances, and three explicit arguments: the two-index array $A$ (first index in $I$, second in $J$), a real vector $c$ indexed by $I$, and a real vector $y$ indexed by $J$. It asserts the conjunction

$$\forall i \in I,\quad \sum_{j \in J} A_{i,j}\, y_j \;\le\; c_i, \qquad\text{and}\qquad \forall j \in J,\quad 0 \le y_j .$$

Here the summation convention is the mirror image of the primal one: for each fixed first index $i$, the sum runs over the second index $j$, over the $J$-indexed family $j \mapsto A_{i,j}$ paired with $y_j$. Both inequalities are non-strict and the $c$-side is the upper bound. No sign assumption is placed on $A$ or $c$. Degenerate cases: if $J$ is empty, all sums are $0$, the nonnegativity clause is vacuous, and the predicate reduces to "$0 \le c_i$ for all $i$"; if $I$ is empty, the first clause is vacuous and the predicate reduces to "$y_j \ge 0$ for all $j$"; if both are empty it is unconditionally true.

3. primalObjective

primalObjective is not a proposition but a real-valued function. It takes the implicit type $I$ with its implicit finiteness instance (the type $J$ and its instance are also in scope as implicit arguments of the surrounding variable block, though $J$ plays no role in the body) and two explicit real vectors $c$ and $x$, both indexed by $I$, and returns the finite sum

$$\sum_{i \in I} c_i\, x_i ,$$

that is, the pairing of the coefficient vector $c$ with the vector $x$ in the order "$c$ factor first, $x$ factor second". No feasibility, sign, or normalization condition is imposed on either argument: the value is defined for arbitrary real vectors. If $I$ is empty the value is $0$.

4. dualObjective

dualObjective is likewise a real-valued function, taking the implicit type $J$ with its implicit finiteness instance (and the implicit $I$ and its instance, unused in the body) and two explicit real vectors $b$ and $y$, both indexed by $J$, and returning

$$\sum_{j \in J} b_j\, y_j ,$$

the pairing of $b$ with $y$ in the order "$b$ factor first, $y$ factor second". Again no feasibility or sign condition is imposed on the arguments, and the value is $0$ when $J$ is empty.

5. PrimalOptimal

PrimalOptimal is a predicate on a specific vector. Its implicit arguments are $I$, $J$ and their two finiteness instances; its explicit arguments are $A$ (first index $I$, second index $J$), $b$ indexed by $J$, $c$ indexed by $I$, and $x$ indexed by $I$. It asserts the conjunction of two things: first, that $x$ is primal feasible in the sense of declaration 1, i.e. $b_j \le \sum_{i} A_{i,j} x_i$ for every $j \in J$ and $x_i \ge 0$ for every $i \in I$; and second, that for every real vector $x'$ indexed by $I$ — the quantifier ranges over all functions $I \to \mathbb{R}$, filtered by the hypothesis that $x'$ is itself primal feasible in the same sense — one has

$$\sum_{i \in I} c_i\, x_i \;\le\; \sum_{i \in I} c_i\, x'_i .$$

So the direction of optimality is minimization: the objective at $x$ is a lower bound for the objective at every feasible competitor. The inequality is non-strict, so nothing about uniqueness is claimed and several vectors may simultaneously satisfy this predicate. The statement does not require $c$, $b$, or $A$ to be nonnegative. If $J$ is empty, feasibility of $x$ and of each $x'$ reduces to nonnegativity, so the predicate says $x \ge 0$ and $\sum_i c_i x_i \le \sum_i c_i x'_i$ for all $x' \ge 0$. If $I$ is empty, the predicate reduces to "$b_j \le 0$ for all $j$" (the objective comparison becomes $0 \le 0$).

6. DualOptimal

DualOptimal is the corresponding predicate on a specific $J$-indexed vector, with implicit $I$, $J$ and their two finiteness instances, and explicit arguments $A$, $b$ indexed by $J$, $c$ indexed by $I$, and $y$ indexed by $J$. It asserts, first, that $y$ is dual feasible in the sense of declaration 2, i.e. $\sum_{j} A_{i,j} y_j \le c_i$ for every $i \in I$ and $y_j \ge 0$ for every $j \in J$; and second, that for every real vector $y'$ indexed by $J$ that is dual feasible in the same sense,

$$\sum_{j \in J} b_j\, y'_j \;\le\; \sum_{j \in J} b_j\, y_j .$$

Note the orientation of this second clause: the competitor's objective appears on the left, so the direction of optimality is maximization — the objective at $y$ dominates that at every dual feasible competitor. The inequality is non-strict and no uniqueness is claimed. If $I$ is empty, dual feasibility reduces to $y \ge 0$ and the clause says $\sum_j b_j y'_j \le \sum_j b_j y_j$ for all nonnegative $y'$. If $J$ is empty, the predicate reduces to "$0 \le c_i$ for all $i$" (the objective comparison becomes $0 \le 0$).

7. PrimalHasOptimum

PrimalHasOptimum takes implicit $I$, $J$ with their two finiteness instances and explicit $A$ (first index $I$, second $J$), $b$ indexed by $J$, and $c$ indexed by $I$; it asserts the bare existence statement: there exists a real vector $x$ indexed by $I$ such that $x$ is primal optimal in the sense of declaration 5 — that is, $x$ satisfies $b_j \le \sum_i A_{i,j} x_i$ for all $j$ and $x_i \ge 0$ for all $i$, and $\sum_i c_i x_i \le \sum_i c_i x'_i$ for every primal feasible $x'$. This is an ordinary existential, not a unique existential, so it does not claim that the minimizer is unique. It does assert, as part of the unfolded content, that the primal feasible set is nonempty (the witness lies in it) and that the infimum of the objective over that set is attained. If $I$ is empty it reduces to "$b_j \le 0$ for all $j$"; if $J$ is empty it reduces to the existence of a nonnegative $x$ minimizing $\sum_i c_i x_i$ over all nonnegative vectors.

8. DualHasOptimum

DualHasOptimum takes implicit $I$, $J$ with their two finiteness instances and explicit $A$, $b$ indexed by $J$, and $c$ indexed by $I$; it asserts that there exists a real vector $y$ indexed by $J$ that is dual optimal in the sense of declaration 6 — i.e. $\sum_j A_{i,j} y_j \le c_i$ for all $i \in I$, $y_j \ge 0$ for all $j \in J$, and $\sum_j b_j y'_j \le \sum_j b_j y_j$ for every dual feasible $y'$. Again this is a plain existential with no uniqueness, and it entails both that the dual feasible set is nonempty and that the supremum of the dual objective over it is attained. If $J$ is empty it reduces to "$0 \le c_i$ for all $i$"; if $I$ is empty it reduces to the existence of a nonnegative $y$ maximizing $\sum_j b_j y_j$ over all nonnegative vectors.

9. PrimalFeasibleNonempty

PrimalFeasibleNonempty takes implicit $I$, $J$ with their two finiteness instances and only two explicit arguments — $A$ (first index $I$, second $J$) and $b$ indexed by $J$; the objective vector $c$ does not appear. It asserts that there exists a real vector $x$ indexed by $I$ with $b_j \le \sum_{i \in I} A_{i,j} x_i$ for every $j \in J$ and $x_i \ge 0$ for every $i \in I$. Nothing is said about the value of any objective at this witness or about optimality. If $J$ is empty the statement is true for the zero vector (indeed for any nonnegative vector); if $I$ is empty it is equivalent to "$b_j \le 0$ for all $j$", witnessed by the empty vector.

10. DualFeasibleNonempty

DualFeasibleNonempty takes implicit $I$, $J$ with their two finiteness instances and two explicit arguments — $A$ and $c$ indexed by $I$; the vector $b$ does not appear. It asserts that there exists a real vector $y$ indexed by $J$ with $\sum_{j \in J} A_{i,j} y_j \le c_i$ for every $i \in I$ and $y_j \ge 0$ for every $j \in J$. Nothing is said about the value of the dual objective at this witness or about optimality. If $I$ is empty the statement is true for the zero vector (indeed any nonnegative $y$); if $J$ is empty it is equivalent to "$0 \le c_i$ for all $i$", witnessed by the empty vector.

11. PrimalObjectiveBddBelow

PrimalObjectiveBddBelow takes implicit $I$, $J$ with their two finiteness instances and explicit $A$, $b$ indexed by $J$, and $c$ indexed by $I$. It asserts that there exists a real number $M$ such that for every real vector $x$ indexed by $I$, if $x$ is primal feasible — i.e. $b_j \le \sum_i A_{i,j} x_i$ for all $j \in J$ and $x_i \ge 0$ for all $i \in I$ — then

$$M \;\le\; \sum_{i \in I} c_i\, x_i .$$

The bound $M$ is merely some lower bound: it is not required to be tight, to be the infimum, or to be attained by any feasible point, and the quantifier order is "$\exists M$, $\forall x$", so a single $M$ must work uniformly. Crucially, the implication is vacuous when no $x$ is primal feasible: if the feasible set is empty, the statement holds with any $M$ whatsoever, so this predicate carries no existence content. If $I$ is empty, every feasible $x$ has objective $0$, so the predicate holds (e.g. with $M = 0$) regardless of $b$; if $J$ is empty the predicate says the objective $\sum_i c_i x_i$ is bounded below over the nonnegative orthant.

12. DualObjectiveBddAbove

DualObjectiveBddAbove takes implicit $I$, $J$ with their two finiteness instances and explicit $A$, $b$ indexed by $J$, and $c$ indexed by $I$. It asserts that there exists a real number $M$ such that for every real vector $y$ indexed by $J$, if $y$ is dual feasible — i.e. $\sum_j A_{i,j} y_j \le c_i$ for all $i \in I$ and $y_j \ge 0$ for all $j \in J$ — then

$$\sum_{j \in J} b_j\, y_j \;\le\; M .$$

Again $M$ is only some uniform upper bound, not required to be the supremum or to be attained, with quantifier order "$\exists M$, $\forall y$"; and the implication is vacuous when the dual feasible set is empty, in which case any $M$ works and the predicate asserts nothing about existence. If $J$ is empty the objective of any feasible $y$ is $0$ and the predicate holds (e.g. $M = 0$); if $I$ is empty the predicate says $\sum_j b_j y_j$ is bounded above over the nonnegative orthant.

13. NonnegInstance

NonnegInstance takes implicit $I$, $J$ with their two finiteness instances and explicit $A$ (first index $I$, second $J$), $b$ indexed by $J$, and $c$ indexed by $I$, and asserts a threefold conjunction of non-strict sign conditions:

$$\forall i \in I,\ \forall j \in J,\quad 0 \le A_{i,j}; \qquad \forall j \in J,\quad 0 \le b_j; \qquad \forall i \in I,\quad 0 \le c_i .$$

All three are $\ge 0$, not $> 0$, so zero entries, the zero matrix, and the zero vectors are all permitted; nothing is required about row or column sums, nonzero-ness, or any relation between $A$, $b$, and $c$. If $I$ is empty, the first and third clauses are vacuous and only "$b_j \ge 0$ for all $j$" survives; if $J$ is empty, the first and second are vacuous and only "$c_i \ge 0$ for all $i$" survives; if both are empty the conjunction is vacuously true.

14. PrimalApproxCS

PrimalApproxCS takes implicit $I$, $J$ with their two finiteness instances, and five explicit arguments: a real number $\alpha$ (the first argument), the array $A$ (first index $I$, second $J$), the vector $c$ indexed by $I$, the vector $x$ indexed by $I$, and the vector $y$ indexed by $J$; the vector $b$ does not appear. It asserts that for every $i \in I$, if $x_i$ is strictly positive, then the quantity $S_i := \sum_{j \in J} A_{i,j}\, y_j$ — a sum over the second index of $A$ with the first index fixed at $i$, i.e. exactly the left-hand side of the $i$-th dual constraint — is two-sidedly bounded:

$$\frac{c_i}{\alpha} \;\le\; S_i \qquad\text{and}\qquad S_i \;\le\; c_i .$$

So the bounded quantity is the dual-constraint sum $S_i$, with the lower bound $c_i/\alpha$ and the upper bound $c_i$; both inequalities are non-strict, and they are imposed only at those indices $i$ where $x_i > 0$ (indices with $x_i = 0$, or $x_i < 0$, are entirely unconstrained — the hypothesis is the strict inequality $0 < x_i$, so the predicate is vacuously true whenever $x$ has no strictly positive coordinate, in particular for $x = 0$). Note that the upper bound $S_i \le c_i$ is the $i$-th dual feasibility inequality restated at the support of $x$ only; the predicate does not require it at other indices, nor does it require $y \ge 0$, $x \ge 0$, or any sign condition on $\alpha$, $A$, or $c$. Because division in the reals is a total operation here, $\alpha = 0$ is permitted and yields $c_i/0 = 0$, so at $\alpha = 0$ the predicate degenerates to "for every $i$ with $x_i > 0$: $0 \le S_i \le c_i$" — a nonnegativity requirement on the dual-constraint sum rather than anything involving $c_i$ on the left. For $\alpha < 0$ the quotient $c_i/\alpha$ has the opposite sign pattern from the positive case (e.g. it is negative when $c_i > 0$), and no hypothesis such as $\alpha \ge 1$ or $\alpha > 0$ is present to exclude this. Degenerate index types: if $I$ is empty the predicate is vacuously true; if $J$ is empty then $S_i = 0$ for every $i$ and the predicate says "for every $i$ with $x_i > 0$: $c_i/\alpha \le 0$ and $0 \le c_i$".

15. DualApproxCS

DualApproxCS takes implicit $I$, $J$ with their two finiteness instances, and five explicit arguments: a real number $\beta$ (the first argument), the array $A$ (first index $I$, second $J$), the vector $b$ indexed by $J$, the vector $x$ indexed by $I$, and the vector $y$ indexed by $J$; the vector $c$ does not appear. It asserts that for every $j \in J$, if $y_j$ is strictly positive, then the quantity $T_j := \sum_{i \in I} A_{i,j}\, x_i$ — a sum over the first index of $A$ with the second index fixed at $j$, i.e. exactly the left-hand side of the $j$-th primal constraint — is two-sidedly bounded:

$$b_j \;\le\; T_j \qquad\text{and}\qquad T_j \;\le\; \beta\, b_j .$$

So the bounded quantity is the primal-constraint sum $T_j$, with the lower bound $b_j$ and the upper bound the product $\beta b_j$ (a multiplication, not a division, so no junk-value issue arises); both inequalities are non-strict and are imposed only at indices $j$ with $y_j > 0$, leaving indices with $y_j = 0$ or $y_j < 0$ unconstrained, and making the predicate vacuously true when $y$ has no strictly positive coordinate, in particular for $y = 0$. The lower bound $b_j \le T_j$ is the $j$-th primal feasibility inequality restated at the support of $y$ only; the predicate does not require it elsewhere, nor does it require $x \ge 0$, $y \ge 0$, or any sign condition on $\beta$, $A$, or $b$. At $\beta = 0$ the upper bound becomes $T_j \le 0$, so the predicate then requires, for each $j$ with $y_j > 0$, that $b_j \le T_j \le 0$ — which in particular forces $b_j \le 0$ at every such $j$; for $\beta < 0$ the two bounds read $b_j \le T_j \le \beta b_j$, which is unsatisfiable whenever $b_j > 0$ and $\beta < 1$, and no hypothesis such as $\beta \ge 1$ or $\beta > 0$ is present. Degenerate index types: if $J$ is empty the predicate is vacuously true; if $I$ is empty then $T_j = 0$ for every $j$ and the predicate says "for every $j$ with $y_j > 0$: $b_j \le 0$ and $0 \le \beta b_j$".

The four primal notions, as literally written

PrimalOptimal A b c x is a predicate about a named vector $x$: it says $x$ is feasible and its objective is $\le$ that of every feasible competitor. Unfolding it, it contains a feasible witness ($x$ itself) and a uniform lower bound for the objective over the feasible set (namely $\sum_i c_i x_i$), so as written it entails both PrimalFeasibleNonempty A b and PrimalObjectiveBddBelow A b c, and it entails PrimalHasOptimum A b c by taking $x$ as witness. It does not claim $x$ is the only such vector.

PrimalHasOptimum A b c asserts only that some such $x$ exists; it therefore entails feasible-nonemptiness and bounded-belowness and attainment of the minimum, but, having discarded the witness, it names no particular vector and asserts no uniqueness.

PrimalFeasibleNonempty A b mentions only $A$ and $b$ and asserts only that the constraint system has at least one solution with $x \ge 0$. As written it says nothing whatsoever about $c$ or the objective: it does not imply PrimalObjectiveBddBelow, does not imply PrimalHasOptimum, and does not imply that any particular vector is optimal.

PrimalObjectiveBddBelow A b c asserts only the existence of one real number $M$ bounding the objective from below across all feasible points. It does not imply that a feasible point exists (an empty feasible set makes the inner implication vacuous, so every $M$ works and the predicate holds), it does not imply that the bound is tight or attained, and it does not imply PrimalHasOptimum or PrimalOptimal for any vector. Nor is any implication from the conjunction of feasible-nonemptiness and bounded-belowness to the existence of an optimum asserted anywhere in this bundle: these are four separate definitions, and no theorem connecting them is stated here.

The dual side is the exact mirror in every respect, with the direction of the objective comparison reversed: DualOptimal is maximality of $\sum_j b_j y_j$ among dual feasible vectors, DualHasOptimum its existential form, DualFeasibleNonempty (which mentions $A$ and $c$ but not $b$) the bare solvability of the dual constraint system, and DualObjectiveBddAbove the existence of one uniform upper bound $M$, vacuously true when the dual feasible set is empty. No relation between the primal and dual notions — no weak- or strong-duality inequality, no complementary-slackness implication — is stated in this bundle.