For every finite signed/rational polynomial P, construct U,V,Q with P(X)=U+V*X+(X²-2)*Q(X). Emit an identity certificate; substitution at approximate sqrt2 has an explicit residual (x²-2)*Q(x).
Method: native-induction. Induction: polynomial degree. Risk: high.
This is a human-readable planning contract, not a parsed kernel formula or accepted proof.