Approximate complement certificates and finite tests

A bound on $d_{\diamond }(\mathcal{E},{\mathcal{T}}_{\sigma })$ is a recovery upper certificate. A bound on $d_{\diamond }(\mathcal{N},{\mathcal{T}}_{\omega })$ is a recovery lower certificate. The output factor, the replacement state, the quantifier over code inputs, and the factor of one half in (eq:distances) are part of the statement.