57. Rational certificates and constructive attainment

The finite optimizer in Section CR.5 enumerates finite correction domains. Rational coefficients do not form such a domain. The appropriate interface is therefore not an enumeration of all rational assignments. A solver proposes finite rational matrices, and a verifier checks their identities in the original target.