EconCSLib.GameTheory.StrategicGame.ZeroSum.StrongComplementarity

Formalises matrix-game strong complementarity [MFoGT Prop. 2.4.1(c)]: for a finite zero-sum matrix game A : I → J → ℝ, there exists an optimal pair (xx*, yy*) ∈ X(A) × Y(A) such that

• xx*_i > 0 ⟺ A.Ei i yy* = A.value;
• yy*_j > 0 ⟺ A.Ej xx* j = A.value.

The forward direction is support_complementarity_row/column and holds for every optimal pair. The reverse direction comes from LP strong CS (EconCSLib.LinearProgramming.exists_strong_complementary_pair) applied to the shifted matrix-game LP.

Proof outline

1. Shift: define K so A' i j := A.g i j + K > 0 for every i, j. The shifted value is v' := A.value + K > 0.
2. LP setup: the row LP for the shifted game is min ∑ x'_i subject to (A'ᵀ x')_j ≥ 1 and x' ≥ 0. Optimal x' rescales to xx = x' · v' (a mixed strategy).
3. Optimal LP pair: from a matrix-game optimal pair (xx₀, yy₀) (existence via MatrixGame.exists_mixed_nash_equilibrium), set x'₀ := xx₀ / v', u'₀ := yy₀ / v'. Both have LP objective 1/v'.
4. Apply LP strong CS: gives a strong-CS optimal pair (x'*, u'*).
5. Rescale and biconditional: xx* := x'* · v', yy* := u'* · v'. The LP strict CS conditions translate to the matrix-game biconditional via (A'ᵀ xx*)_j = A.Ej xx* j + K and v' = A.value + K. Specifically:
   • (Ax* - b)_j > 0 ⟺ u'*_j = 0 becomes A.Ej xx* j > A.value ⟺ yy*_j = 0, equivalently yy*_j > 0 ⟺ A.Ej xx* j = A.value (with weak duality giving ≤ A.value).
   • Symmetric for rows.

The LP theorem indexes primal variables by Fin n; we bridge to Fintype I via Fintype.equivFin I (a Fintype.sum_equiv adapter). The index types are constrained to Type (= Type 0) so the universe inference for Fintype.sum_equiv matches ℝ : Type 0.

Blueprint

• docs/knowledge/nodes/zero_sum/strong_complementarity.md

theorem MatrixGame.exists_strong_complementary_pair {I J : Type} [Fintype I] [Fintype J] [Nonempty I] [Nonempty J] [DecidableEq I] [DecidableEq J] (A : MatrixGame I J ℝ) : ∃ (xx : ↑(stdSimplex ℝ I)) (yy : ↑(stdSimplex ℝ J)), xx ∈ A.optimalRowStrategies ∧ yy ∈ A.optimalColumnStrategies ∧ (∀ (i : I), 0 < ↑xx i ↔ A.Ei i yy = A.value) ∧ ∀ (j : J), 0 < ↑yy j ↔ A.Ej xx j = A.value

Matrix-game strong complementarity [MFoGT Prop. 2.4.1(c)].

There exists an optimal pair (xx, yy) ∈ X(A) × Y(A) such that for every row i, xx_i > 0 ↔ A.Ei i yy = A.value, and for every column j, yy_j > 0 ↔ A.Ej xx j = A.value.

The forward direction is support_complementarity_row/column. The reverse direction comes from LP strong complementarity (EconCSLib.LinearProgramming.exists_strong_complementary_pair) applied to the shifted matrix-game LP. See module docstring for the detailed proof outline.