forall integer polynomial codes P. Nonzero(P) -> exists n,w. TransCert(P,n,w). Establish the fixed constant interpretation by IR027; no bounded-degree substitute.
Method: native-search. Induction: none. Risk: critical.
This is a human-readable planning contract, not a parsed kernel formula or accepted proof.