forall ap am b. b>0 -> exists n up um ud e trace. IrrCert(ap,am,b,n,up,um,ud,e,trace). Split rational competitors inside/outside [1,2]; no classical rule, oracle, missing premise or degree/height restriction.
Method: native-search. Induction: none. Risk: critical.
This is a human-readable planning contract, not a parsed kernel formula or accepted proof.