Strong duality adapter: a primal optimum yields a dual optimum of equal value (Fin-indexed)

Read-back — strong_duality_adapter

Setting and binders. The statement is quantified over two natural numbers $n$ and $m$ (both implicit, with no positivity or nondegeneracy assumption: $n = 0$ and $m = 0$ are included), and over four arbitrary data items:

• a real matrix $A$ presented as a function $A : \{0,\dots,n-1\} \times \{0,\dots,m-1\} \to \mathbb{R}$, written $A_{i,j}$, whose first index $i$ ranges over the concretely-chosen index type $\mathrm{Fin}\,n$ (the canonical type of naturals below $n$) and whose second index $j$ ranges over $\mathrm{Fin}\,m$ — these are the literal index types, not arbitrary finite or fintype-instantiated index types;
• a vector $b : \mathrm{Fin}\,m \to \mathbb{R}$, written $b_j$;
• a vector $c : \mathrm{Fin}\,n \to \mathbb{R}$, written $c_i$;
• a vector $x : \mathrm{Fin}\,n \to \mathbb{R}$, written $x_i$.

No sign, boundedness, rank, or nonzero assumption is imposed on $A$, $b$, or $c$; all entries are arbitrary reals.

The hypothesis, fully expanded. The single hypothesis is that $x$ is primal optimal, which unfolds to the conjunction of:

1. Primal feasibility of $x$:

$$\forall j \in \mathrm{Fin}\,m,\quad b_j \le \sum_{i \in \mathrm{Fin}\,n} A_{i,j}\, x_i \qquad\text{and}\qquad \forall i \in \mathrm{Fin}\,n,\quad 0 \le x_i .$$

(Note the inequality direction: the weighted column sums are bounded below by $b$, with a non-strict $\le$, and $x$ is componentwise nonnegative.)

2. Minimality of $x$ among all primal-feasible points: for every function $x' : \mathrm{Fin}\,n \to \mathbb{R}$ — the inner quantifier ranges over all real-valued functions on $\mathrm{Fin}\,n$, restricted only by feasibility, with no locality, boundedness, or proximity restriction — if $x'$ satisfies the same two feasibility conditions ($b_j \le \sum_i A_{i,j} x'_i$ for all $j$, and $0 \le x'_i$ for all $i$), then

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

So $x$ minimizes $\sum_i c_i x_i$ over the primal-feasible set. Since $x$ is itself feasible, $x$ is one of the admissible $x'$, so this clause is reflexively satisfied at $x' = x$.

The conclusion, fully expanded. There exists a vector $y : \mathrm{Fin}\,m \to \mathbb{R}$ (mere existence, not unique existence, and no formula or construction for $y$ is asserted) such that both:

1. $y$ is dual optimal, i.e.
   • dual feasibility: $\forall i \in \mathrm{Fin}\,n,\ \sum_{j \in \mathrm{Fin}\,m} A_{i,j}\, y_j \le c_i$ (row sums bounded above by $c$, non-strict) and $\forall j \in \mathrm{Fin}\,m,\ 0 \le y_j$;
   • maximality: for every function $y' : \mathrm{Fin}\,m \to \mathbb{R}$ satisfying those same two dual-feasibility conditions,

$$\sum_{j \in \mathrm{Fin}\,m} b_j\, y'_j \;\le\; \sum_{j \in \mathrm{Fin}\,m} b_j\, y_j ,$$

 i.e. $y$ *maximizes* $\sum_j b_j y_j$ over the dual-feasible set (note the reversed direction relative to the primal clause: primal optimality is minimization, dual optimality is maximization);

2. the two objective values coincide exactly:

$$\sum_{i \in \mathrm{Fin}\,n} c_i\, x_i \;=\; \sum_{j \in \mathrm{Fin}\,m} b_j\, y_j .$$

Existence vs. assumption. This statement assumes existence of a primal optimum (it is handed a specific optimal $x$) and asserts existence of a dual optimum. It is therefore a conditional existence claim, not an unconditional one.

Degenerate cases.

• $n = 0$ (no primal variables): $\mathrm{Fin}\,0$ is empty, $x$ is the unique empty function, and every sum over $i$ is the empty sum $0$. The hypothesis then forces $b_j \le 0$ for all $j$; the componentwise-nonnegativity clause and the minimality clause are vacuous/trivial (the only feasible $x'$ is $x$ itself, and $0 \le 0$). The primal objective is $0$, so the conclusion demands a $y$ with $0 \le y_j$ for all $j$ (the dual constraint clause, quantified over $i \in \mathrm{Fin}\,0$, is vacuous), maximal $\sum_j b_j y_j$ over all such $y$, and $\sum_j b_j y_j = 0$. If instead some $b_j > 0$ while $n = 0$, the hypothesis is unsatisfiable and the statement is vacuous for that data.
• $m = 0$ (no constraints): the first feasibility clause (quantified over $j \in \mathrm{Fin}\,0$) is vacuous, so primal feasibility reduces to $x_i \ge 0$ for all $i$, and the hypothesis says $x \ge 0$ minimizes $\sum_i c_i x_i$ over the nonnegative orthant. The witness $y$ is the unique empty function, its dual-feasibility reduces to $0 \le c_i$ for all $i$ (empty row sums) with the nonnegativity clause vacuous, its maximality is $0 \le 0$, and the value equality reduces to $\sum_i c_i x_i = 0$.
• $n = m = 0$: all feasibility and optimality clauses are vacuous or trivial, and the value equality reduces to $0 = 0$.

Relation to the other two statements. As written, this statement implies the left-to-right direction of strong_duality_iff_fin (from a primal optimum it produces a dual optimum). It also implies strong_duality_value_fin: given any primal optimum $x$ and any dual optimum $y$, this statement yields some dual optimum $y_0$ with $\sum_i c_i x_i = \sum_j b_j y_{0,j}$, and applying the maximality clause of dual optimality in both directions (once with $y' = y_0$ against $y$, once with $y' = y$ against $y_0$) forces $\sum_j b_j y_j = \sum_j b_j y_{0,j}$. It does not imply the right-to-left direction of the biconditional.

Not asserted. No claim that $y$ is unique; no construction, formula, sign pattern, or complementary-slackness relation for $y$; no claim that a primal optimum exists for any given $A, b, c$; no claim that the primal-feasible or dual-feasible sets are nonempty, closed, or bounded; no claim about the case where $x$ is merely feasible but not optimal; no claim about unbounded or infeasible instances; no weak-duality statement in its own right; no statement about arbitrary finite index types other than $\mathrm{Fin}\,n$ and $\mathrm{Fin}\,m$; and no assertion that the constructed $y$ is related to $x$ in any way beyond the stated equality of objective values.

---