Certified Behavioral Maxmin: Semidefinite Certification Separates Abstraction Loss from Solver Loss in Imperfect-Recall Games

A player who forgets, facing an adversary who does not, is the normal case in deployed game solving: a poker abstraction merges information sets, and a team that cannot communicate knows less than its members do. Her best guaranteed payoff, the behavioral maxmin, is a polynomial optimization problem that is $\exists \mathbb{R}$-hard even when the adversary has perfect recall, and first-order methods return a strategy without saying how far it is from that value. We add a certificate that runs once after the solver and changes nothing about it: a sum-of-squares feasibility program in which the adversary appears as a polynomial response map, so it contributes only linear variables and the semidefinite blocks carry only the player's variables. The degree of the response map defines a ladder: at degree zero the certificate bounds the minmax value, and raising the degree closes the behavioral duality gap. A posterior step makes the floating-point solution rigorous by evaluation alone, and that bound splits the deployment loss of the solver's point into an abstraction part and a solver part, which exploitability cannot distinguish: on Kuhn poker two abstractions, one with perfect recall and one without, lose the same $0.167$ against the full game, and the certificate assigns the first loss to the abstraction and the second to CFR stalling. On Leduc abstractions up to $126$ variables it bounds CFR's gap by $10^{-4}$ in minutes where the global solver SCIP leaves $10^{-3}$ to $10^{-2}$ after an hour, and on three-player Kuhn teams it certifies a team-maxmin value and an interval for the value of coordination. One certificate thus separates two failures that the standard diagnostic reports as one number.