A Deterministic Polynomial-Time Approximation Below One Third for Bimatrix Games

This paper proves a strict deterministic polynomial-time approximation guarantee below the one-third frontier for general two-player rational bimatrix games with payoffs normalized to [0,1]. Its central result is an explicit universal algorithm that returns a rational approximate Nash equilibrium with worst-case regret at most 1/3 − 7.5 × 10⁻⁴⁵ < 1/3. The contribution is therefore a qualitative separation of the deterministic polynomial-time approximation threshold from one third, rather than another guarantee that approaches 1/3 only from above. The proof builds on the Tsaknakis–Spirakis stationary descent and the Deligkas–Fasoulakis–Markakis (DFM) post-processing framework, but substantially strengthens the interface between stationarity and post-processing. Crucially, the algorithm retains throughout the enlarged d-near-best-response sets on which the polynomial-convergence argument is actually established. It does not replace the resulting certificate by a re-solved exact-best-response dual. Instead, the normalized enlarged-dual mixtures are treated as d-best responses, their explicit row and column deficits are propagated through the entire argument, and all subsequent candidates are constructed from the same retained enlarged certificate. A deficit-aware pointwise bridge converts the enlarged stationary dual into pure-action inequalities suitable for fixed-anchor regret control. This yields a complete near-set stationary ledger, including the harmonic bound, the third DFM inequality, and the one-dimensional minimax eliminations required in the difficult asymmetric branches. The proof separately establishes persistence of DFM Case 4.1 and gives a dependency-explicit reconstruction of Case 4.2, thereby eliminating hidden reliance on exact-best-response support. The Case 4.2 equality-set analysis is made quantitatively robust by threshold-perturbed residual functions and a unified tolerance parameter. Exact separation margins away from the critical zero sets dominate the perturbation error by several orders of magnitude. The remaining endpoint, high-face, and near-one configurations are then excluded by explicit feasibility, derivative, denominator, and stationary estimates rather than by qualitative continuity arguments. This produces an exhaustive treatment of the parameter space under the enlarged-set certificate. The central regime is closed by a fixed-anchor contradiction argument with an explicit boundary optimization. Once the direct-mixing branch fails, the relevant completion value W(a_s,a_w) is shown to be monotone in the admissible slack directions. The supremum over the strict deficit budget can therefore be transferred to its closed boundary, where the derivative has constant sign, and the maximization reduces to two endpoints. Exact evaluation gives W(E_s) = 0.2777901226… and W(E_w) = 0.3077215004… < 0.30773. Hence, any putative central obstruction would generate a feasible completion below 0.30773, contradicting the assumed obstruction. Importantly, 0.30773 is used only as a contradiction witness in the central branch; it is not asserted as a uniform approximation guarantee for arbitrary games. At the structural level, every enlarged-set terminal certificate satisfying the stated stopping condition contains either an enriched fixed-side-hull candidate or a finite DFM candidate of regret at most 1/3 − 10⁻⁴⁴. The algorithmic theorem then converts this structural separation into a fully specified rational polynomial-time procedure. The implementation consists of rational regret equalization, enlarged primal-dual linear programs, retention of the terminal enlarged dual, deterministic finite candidate generation, a fixed rational descent step with O(d⁻²) nonterminal iterations, exact regret evaluation, and constant-resolution three-anchor fixed-side discretization. With d₀ = 10⁻⁵⁰, γ₀ = 10⁻⁴⁴, and discretization loss η₀ = γ₀/4 = 2.5 × 10⁻⁴⁵, the final returned profile satisfies ρ_G(x,y) ≤ 1/3 − γ₀ + η₀ = 1/3 − 7.5 × 10⁻⁴⁵ < 1/3. A separate exact-set theorem is retained only as a secondary structural special case. The unconditional polynomial-time result does not depend on an exact-stationarity certificate and does not infer one from near-best-response convergence. This distinction is essential to the final proof architecture: the unconditional conclusion rests directly on the same enlarged certificate type for which polynomial convergence is available. The paper also provides a reproducibility-oriented verification layer. The decisive endpoint values, central mass-control inequalities, boundary monotonicity, fixed-step descent identity, Case 4.2 separation hierarchy, and related algebraic margins are accompanied by exact-rational and symbolic audit checks. These computations serve as algebraic stress tests and reproducibility aids rather than as substitutes for the mathematical proof. The significance of the result is qualitative rather than numerical. The explicit gap below one third is deliberately nonoptimized, but its positivity establishes that the one-third benchmark is not a terminal deterministic polynomial-time upper-bound frontier for normalized rational bimatrix games. Beyond the final approximation constant, the paper develops a reusable methodological framework combining enlarged stationary certificates, deficit-aware primal-dual analysis, enriched strategy hulls, robust equality-set localization, fixed-anchor completion, finite candidate extraction, rational linear programming, controlled discretization, and exact algebraic auditing. These mechanisms provide concrete directions for sharper approximation constants, automated theorem search, symbolic verification, computational benchmarking, and further investigation of the true approximation threshold for bimatrix Nash equilibria. The result does not determine the exact approximation threshold, establish optimality of the displayed gap, provide a matching hardness lower bound, or place exact Nash equilibrium computation in polynomial time. Its precise contribution is a fully explicit deterministic polynomial-time strict crossing of the one-third approximation frontier for general normalized rational bimatrix games.