Produce positive polynomial certificates, by a reviewed quantitative approximate-root construction or an implemented checked PA-to-HA transformation. Neither route is assumed available.
Method: native-induction. Induction: explicit certificate construction. Risk: critical.
This is a human-readable planning contract, not a parsed kernel formula or accepted proof.