Export only whitelisted elaborated obligations with natural-domain guards, exact integer/rational encoding, original target hash and checked-premise hashes. No real pow/log oracle, unproved induction schema or lossy denominator transformation.
Method: structural-check. Induction: none. Risk: critical.
This is a human-readable planning contract, not a parsed kernel formula or accepted proof.