Proof-Carrying Optimality for Finite Identification under Bounded Adversarial Answer Errors

Finite identification asks a learner to determine an unknown behaviour using probes from a fixed alphabet when an adversary may corrupt up to e answers. Exact worst-case query complexity is the value of a large minimax game, so an optimum can be expensive to reproduce. We develop proof-carrying methods for many-valued behaviour tables. Portable certificates combine a noiseless strategy with a small lower witness to prove an affine identity OPT_A(e) = αe + β for every budget, with proof size independent of e. Expanded certificates pair a robust strategy at one budget with an adversary DAG closed by analytic lower bounds. We also provide independently checkable lower bounds and certificates for the non-adaptive optimum. All 30 cells in a 15-instance primary matrix at e ∈ {0, 1} receive two-sided optimality proofs. A 101-instance sweep across e ∈ {0, 1, 2} proves 300 of 303 declared cells, leaving three explicit resource-limit outcomes. At e = 2, adaptivity strictly improves on the exact non-adaptive optimum in 91 completed cells, by as many as 84 probes. Replay is faster than synthesis in 29 of 30 timed primary cells, although the largest accepted lower certificate contains 8.9 million moves. These results make query-complexity claims auditable while exposing proof construction and proof size as bottlenecks.