Start with a valid rational certificate. Clear all input denominators with one positive multiplier, preserving certificate validity. Encode each outcome as a nonnegative integer inequality system, normalizing strict separation or improvement to magnitude at least one. Minimal-support conic representations have independent columns; Cramer's rule on their Gram matrix bounds all reduced coordinates. The actual input encoding bounds both the dimension and the sum of denominator sizes. The resulting certificate encoding is at most 512 times the cube of input size plus one. No solver theorem is assumed.