Run bounded native ring/compact_arith/norm_num/search pilots; record original goal, exact premise allowlist, deterministic strategy, certificate size and fresh HA replay. No external proof or model calls are silently accepted.
Method: native-ring. Induction: none. Risk: routine.
This is a human-readable planning contract, not a parsed kernel formula or accepted proof.